Incorrect UNSAT in Z3 4.4.1 (incremental mode)

[mschwerhoff]

Updating from Z3 4.4.0 (x64, Windows) to 4.4.1, I noticed that several of our tests (Smallfoot-style software verification) fail because Z3 reports UNSAT were it previously didn't and shouldn't.

Here is a minimal example:

(set-option :auto_config false)
(set-option :smt.mbqi false)

(push) ; Comment --> SAT

(declare-const k Real)
(assert (and
  (<= 0.0 k)
  (not (= k 0.0))
  (< k 1.0)))

; (push) ; No observable effect
(check-sat) ; UNSAT (or SAT, see above)

Z3 4.4.0 reported SAT (and so does CVC4), but Z3 4.4.1 reports

• UNSAT for the above example
• SAT if the first push is commented
• SAT if the first push is commented and the second one is uncommented

At first glance, issue #240 looks related.

[mschwerhoff]

Z3 4.4.2 2d2ec38 show the same behaviour.