C API vs. Command line disagree on satisfiability

[Lukas-Dresel]

Hey!

I'm using my own fork of the rust Z3 binding to implement a concolic execution tool. However, I am running into an issue using the z3 optimizer to implement a constraint sampling approach (SMTSampler).

I set up my hard and soft constraints and then print out the optimizer using Z3_optimize_to_string to get a smtlib representation of the solver. The resulting constraints can be found in this pastebin. However, the excerpt that I would think to be relevant is:

(declare-fun x () (_ BitVec 32))
(declare-fun original_0 () Bool)
(declare-fun __guard_hard_BV__x_0__is_1 () Bool)
(assert (=> original_0 (bvult x #x0000000a)))
(assert (=> (not __guard_hard_BV__x_0__is_1) (= ((_ extract 0 0) x) #b0)))
(assert (=> __guard_hard_BV__x_0__is_1 (= ((_ extract 0 0) x) #b1)))
(check-sat)

This contains the only real constraint (guarded by original_0), as well as the two opposing constraints according to the unsat core.

The problem is then that the optimizer check call using those assumptions in the C API (Z3_optimize_check) returns unsat and produces an unsat core of Unsat result for x#0: [__guard_hard_BV__x_0__is_1, (not __guard_hard_BV__x_0__is_1)], whereas when running the z3 command and providing it with the corresponding smt commands below returns SAT and a model.

Any ideas on how to debug this issue? I haven't worked with z3 internals much before and would appreciate any pointers. To be clear, I am operating squarely under the assumption that this is an issue with my implementation of the z3 bindings, however the unsat core containing guard variables to constraints that aren't mutually exclusive does not make much sense to me, so I figured I'd ask :).

[Lukas-Dresel]

P.S. I think I figured out the issue, namely that assert_and_track constraints are being pretty-printed out like an implication, but the solver internally forces the implication guard variable to be true, whereas the implication in text form does not contain this information and can have the variable be true or false.

I would really appreciate any tips on how to debug issues like this in the future, and if someone could confirm my intuition here that would be great as well :)

[NikolajBjorner]

We have Z3_open_log("z3.log"); that you can invoke before any z3 call. It tracks calls into z3. It works only if you have a single thread that uses z3. After the program has finished with its use of z3 you can run "z3 z3.log" - it recognizes the log suffix as a replay log. To debug internals of what goes on we have to do a little more, such as instrument z3 with some tracing (-tr:tag) that is mostly for developers unless you can read source code and find the appropriate tags. Tracing is only enabled on trace enabled builds, not the released binaries, so as a user you have to start with something more basic (run in verbose mode -v:10) to get some idea of what is going on. The replay log feature is good for scenarios where you have a specialized setup (Rust->Z3) that is impossible to install or take time recreating on my end. The replay log represents the boundary to z3.

For solvers we have an option to trace interactions as smtlib2 commands. We don't have this for the optimizer context. This feature allows replaying interaction as commands. I guess a takeaway is that such a feature would expose the missing assumptions portion. You need to use check-sat with assumptions to get unsat.