CODEWITHSUNDEEP
z3smt
Philippe
Philippe

Reputation: 9742

Bug with check-sat when passed assumptions

We ran into this seemingly severe bug today.

Consider this Z3 script. (Reproduced below for completeness.)

The formula is unsat. We first check the formula with an additional assumption, and get unsat as expected. However, when we check it a second time, without any assumption, Z3 now reports sat. When we ask for a model, we get an obviously wrong one (essentially contradicting (distinct 1 1)).

If we surround the first (check-sat ...) with (push) and (pop), the result is as expected. This suggests that when check-sat is passed additional assumptions, it applies unsound simplifications to the context.

Are we perhaps using check-sat in an incorrect way?

(set-option :produce-unsat-cores true)
(set-option :produce-models true)

(declare-const start25 Bool)
(declare-const bf07 Bool)
(declare-const bf19 Bool)
(declare-const lt06 Int)
(declare-const ef08 Int)
(declare-const ef110 Int)

(declare-fun whileM4 (Int) Int)

(assert start25)
(assert (=> start25 (distinct lt06 1)))
(assert (=> start25 (= lt06 (whileM4 0))))
(assert (=> (not bf07) (= ef08 0)))
(assert (=> bf07 (= ef08 (whileM4 (+ 0 1)))))
(assert (=> start25 (not (< (whileM4 0) 1))))
(assert (=> start25 (= (whileM4 0) ef08)))
(assert (=> start25 (and (=> bf07 (< 0 1)) (=> (< 0 1) bf07))))
(assert (=> (not bf19) (= ef110 (+ 0 1))))
(assert (=> bf19 (= ef110 (whileM4 (+ (+ 0 1) 1)))))
(assert (=> bf07 (not (< (whileM4 (+ 0 1)) 1))))
(assert (=> bf07 (= (whileM4 (+ 0 1)) ef110)))
(assert (=> bf07 (and (=> bf19 (< (+ 0 1) 1)) (=> (< (+ 0 1) 1) bf19))))

(push) ; comment out to produce bug
(check-sat (not bf19))
(pop)  ; comment out to produce bug

(check-sat)

Upvotes: 3

Views: 256

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

Thanks for reporting the bug. The bug affects all Z3 <= v4.3.1. I fixed this bug, and the fix is already available at codeplex.

http://z3.codeplex.com/SourceControl/changeset/8c211dd4fcd3

To get the work-in-progress branch, we use

git clone https://git01.codeplex.com/z3 -b unstable

Using the "work-in-progress" branch may be inconvenient since you also get other updates and modifications. So, another option is to manually apply the fix to the version you are using. Note that, the fix is a very small modification.

Upvotes: 4

Related Questions