There is an unsaved comment in progress. You will lose your changes if you continue. Are you sure you want to reopen the work item?
unknown/invalid extract application error
I ran z3 on the attached file, and I got "unknown" when I used 4.3.2 version (z3-220.127.116.11d2a7f922c82-x64-ubuntu-12.04) and "invalid extract application" when I used 4.1 version. Surprisingly, if I added 2 extra assertions:
(assert (= (_ bv0 9) mem_13_v1))
(assert (= (_ bv0 9) mem_24_v0))
z3 will return SAT.
Is this a bug in z3? If yes, can this bug be fixed soon? My project is heavily rely on z3.
If not, can anyone point me out what I did wrong? Is it the case that these extra assertions guide the solver to prune out some space that leads to error? That's why it doesn't fail when having these assertions. If that's the case, what does that error corresponding