Support for multiple (check-sat)

[AndreaCallia]

Dear all,

Using the following code, Z3 first replies sat and then it replies unsat.

(set-logic QF_NRA)
(declare-fun x () Real)
(assert (> x 0.0))
(assert (< x 2.0))
(check-sat)
(assert (> x 5.0))
(check-sat)
(exit)

According to my understanding, the first check-sat is based on just the first two assertions, and the second check-sat also considers the third assertion. In the first case there is a solution (e.g. x == 1), but in the second case it becomes unsat.

You can also verify this online at: http://rise4fun.com/z3

If I run the same code on dReal, it just says: delta-sat with delta = 0.00100000000000000

One first thing I did not understand is: why is dReal giving just one reply, considering I asked to check satisfiability twice? (using two different check-sat commands)

If I try to run it using the --model option, it still says delta-sat just once, but it provides two solutions. The output is below.

Solution:
x : [ ENTIRE ] = [0, 2]
Solution:
x : [ ENTIRE ] = [5, inf]
delta-sat with delta = 0.00100000000000000

You can also verify this online at: http://dreal.github.io/try/

I also do not understand this reply. The first provided solution seems correct (it is compatible with the solution provided by Z3), but I think the second one is incorrect, and I think that after the first check-sat is executed, the solver forgets about the two assertions before it, then when the second check-sat is executed, the solver only considers the third assertion.

Am I wrong? May this be a bug? Probably multiple check-sat commands are not supported? Is there a way to simulate the Z3 behavior, maybe using push and pop mechanisms?

Would the output be different if I use the dReal APIs instead? About this, how should I write the above problem using the dReal C++ APIs instead of writing it in SMT2 format?

My OS is Ubuntu 14.04 64bit and I installed the precompiled dReal binaries using apt-get with the dReal repository.

Many thanks for all your work and support.

[soonho-tri]

Hi @AndreaCallia, thanks for the report. The delta-sat from the second check-sat is a bug and I'm working on a fix. I'll also change it to have an output for each check-sat command.

[soonho-tri]

Closed by 0e900251fd26d2ae55705ea85af51871200ec069 and 0e900251fd26d2ae55705ea85af51871200ec069.

Now it outputs (without --model option):

delta-sat with delta = 0.00100000000000000
unsat

With --model option, we have:

Solution:
x : [ ENTIRE ] = [0.0009765625, 0.001953125]
delta-sat with delta = 0.00100000000000000
unsat

[AndreaCallia]

Many thanks for this fix @soonho-tri ...