1

Closed

z3 returns unsat for a sat query

description

We ran into the following SMTLIBv2 query:
(set-logic QF_BV)
(declare-fun x () (_ BitVec 16))
(assert (and (bvsle x (_ bv65472 16) ) (bvsgt x (_ bv65416 16) ) ) )
(check-sat)
(exit)
This query is sat, i.e., there is an x in the interval (65416, 65472]. I double-checked it with stp/cvc4/boolector.

z3 returns unsat (unstable branch, commit 4c5753f32).

comments

nunolopes wrote Nov 24, 2014 at 6:06 PM

Bug confirmed.
It's a bug in the bv size reduction tactic.

wintersteiger wrote Nov 24, 2014 at 6:12 PM

Thanks for reporting this issue! This has now been fixed in the unstable branch (as of [this](https://z3.codeplex.com/SourceControl/changeset/213d816c0a418bafc8fe57acb4b10aeea5b1f5b2 commit)).

wintersteiger wrote Nov 24, 2014 at 6:12 PM

Problem has been fixed

** Closed by wintersteiger 11/24/2014 10:12AM

nunolopes wrote Nov 24, 2014 at 6:36 PM

Still not enough bits in the party.
Will still be unsat if we add a second constraint:
(assert (not (= x #xffc0)))