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)
