Z3 Bug Report: sat.smt=true returns invalid model for BV comparator assertions

Component: smt.elim_unconstrained + sat.smt=true witness reconstruction
Affected versions: Z3 4.16.0, Z3 main HEAD (4.17.0-dev)
Regression: Z3 4.13.0 is not affected
Option: sat.smt=true (non-default, opt-in)
Type: invalid_model — verdict SAT is correct, but the returned model violates the asserted formula
Workaround: add smt.elim_unconstrained=false

Summary

When sat.smt=true is enabled, Z3 can return a model that falsifies the asserted formula. The verdict (sat) is correct — satisfying assignments exist — but the witness reconstruction assigns a value that violates one or more constraints.

The bug affects boolean structures of bitvector comparator predicates (bvuge, bvult, bvugt, bvule) and their boolean combinations (and, or, xor, not). It is triggered by smt.elim_unconstrained, which abstracts comparator sub-formulas to fresh Boolean variables; the subsequent witness reconstruction independently satisfies each predicate without ensuring joint consistency.

Minimal Reproducer

Pattern 1 — AND scalar inclusion (simplest)

(set-logic QF_BV)
(declare-const k (_ BitVec 4))
(assert (and (bvuge k (_ bv1 4)) (bvult k (_ bv3 4))))
(check-sat)
(get-model)

Expected: sat with k ∈ {1, 2} (any value satisfying 1 ≤ k < 3)
Actual (z3 sat.smt=true): sat, k = #x0 (= 0)
Verification: bvuge(0, 1) = false → returned model violates bvuge k 1

Pattern 2 — OR range rejection

(set-logic QF_BV)
(declare-const x (_ BitVec 4))
(assert (or (bvult x (_ bv1 4)) (bvuge x (_ bv7 4))))
(check-sat)
(get-model)

Expected: sat with x ∈ {0} ∪ {7, 8, …, 15}
Actual (z3 sat.smt=true): sat, x = #x6 (= 6)
Verification: bvult(6,1) = false, bvuge(6,7) = false → or(false, false) = false → invalid model

Pattern 3 — XOR of two comparators

(set-logic QF_BV)
(declare-const v1 (_ BitVec 3))
(declare-const v2 (_ BitVec 3))
(assert (xor (bvult v2 (_ bv6 3)) (bvult (_ bv4 3) v1)))
(check-sat)
(get-model)

Expected: sat with e.g. v1 = 7, v2 = 0 (where exactly one predicate holds)
Actual (z3 sat.smt=true): sat, v1 = #b101 (5), v2 = #b101 (5)
Verification: bvult(5,6) = true, bvult(4,5) = true → xor(true, true) = false → invalid model

Pattern 4 — Double negation (NOT NOT)

(set-logic QF_BV)
(declare-const x (_ BitVec 3))
(assert (not (not (and (bvuge x (_ bv1 3)) (bvult x (_ bv3 3))))))
(check-sat)
(get-model)

Expected: sat with x ∈ {1, 2}
Actual (z3 sat.smt=true): sat, x = #b000 (= 0)
Verification: bvuge(0, 1) = false → invalid model
Note: Double negation does not protect against the bug; the inner AND form is still abstracted.

Pattern 5 — Multi-assertion (variable appears in two assertions)

(set-logic QF_BV)
(declare-const x (_ BitVec 4))
(assert (= (bvand x (_ bv3 4)) x))
(assert (and (bvuge x (_ bv1 4)) (bvult x (_ bv3 4))))
(check-sat)
(get-model)

Expected: sat with x ∈ {1, 2} (satisfies both assertions)
Actual (z3 sat.smt=true): sat, x = #x0 (= 0)
Verification: bvuge(0, 1) = false → second assertion violated
Note: x appears in both assertions. The bug fires despite the variable not being "single-occurrence". smt.elim_unconstrained abstracts x from the comparator predicates in the second assertion even though x appears in the first assertion as well.

Metamorphic Confirmation (no external oracle required)

The following two formulas are semantically equivalent by De Morgan's law:

v1: (or  (bvult x 1) (bvuge x 7))
v2: (not (and (bvuge x 1) (bvult x 7)))

Both express x ∉ [1, 6]. Any sound solver must return consistent models for both.

v1 (z3 sat.smt=true):

; v1-or-range.smt2
(set-logic QF_BV)
(declare-const x (_ BitVec 4))
(assert (or (bvult x (_ bv1 4)) (bvuge x (_ bv7 4))))
(check-sat)
(get-model)

Expected: sat with x ∈ {0} ∪ {7..15}
Actual: sat, x = #x6 (= 6) — violates v1

v2 (z3 sat.smt=true):

; v2-not-and-range.smt2
(set-logic QF_BV)
(declare-const x (_ BitVec 4))
(assert (not (and (bvuge x (_ bv1 4)) (bvult x (_ bv7 4)))))
(check-sat)
(get-model)

Expected: same satisfying set as v1
Actual: sat, x = #x0 (= 0) — satisfies v2, but inconsistent with v1's model

Result: v1 and v2 are equivalent yet produce different models (6 vs 0). Cross-validating v1's model (x=6) against v2: not(and(bvuge(6,1), bvult(6,7))) = not(and(T,T)) = false → v1's model falsifies v2. This proves the bug without any external oracle.

Root Cause

The interaction between smt.elim_unconstrained and sat.smt=true:

1. smt.elim_unconstrained identifies variables that appear (at least once) only in comparator predicates and abstracts each predicate to a fresh Boolean variable:
   b1 ← (bvuge k 1), b2 ← (bvult k 3)

2. The SAT layer satisfies the resulting Boolean formula (e.g., and(b1, b2) → b1=T, b2=T).

3. Witness reconstruction maps each Boolean back to a BV value independently:

   • b1=T → pick k such that bvuge k 1 → selects k = 0 (off-by-one error: picks lo − 1)
   • b2=T → pick k such that bvult k 3 → k = 0 happens to satisfy this too

4. The independently chosen values are combined into a single model, but their joint consistency is not checked. Result: k = 0 which falsifies b1.

Workaround: smt.elim_unconstrained=false disables the abstraction step and eliminates all observed instances of the bug.

Z3 Self-Diagnosis

With model_validate=true, Z3 confirms the bug itself on all 5 patterns:

$ z3 sat.smt=true model_validate=true minimal/01-and-scalar.smt2
sat
(error "line 10 column 10: an invalid model was generated")
(
  (define-fun k () (_ BitVec 4)
    #x0)
)

The same an invalid model was generated error appears for patterns 1–5.

Regression Window

Cross-Solver Verification

All reference solvers return correct models on the same formula:

Files

report_bug/
├── REPORT.md                    ← this file
├── repro.sh                     ← automated reproducer (run with: bash repro.sh)
├── minimal/
│   ├── 01-and-scalar.smt2       ← Pattern 1: AND scalar inclusion
│   ├── 02-or-range.smt2         ← Pattern 2: OR range rejection
│   ├── 03-xor-cmp.smt2          ← Pattern 3: XOR comparators
│   ├── 04-double-neg.smt2       ← Pattern 4: double negation wrapper
│   └── 05-multi-assert.smt2     ← Pattern 5: multi-assertion trigger
└── metamorphic/
    ├── v1-or-range.smt2         ← DeMorgan pair v1
    └── v2-not-and-range.smt2    ← DeMorgan pair v2 (equivalent to v1)

Run bash repro.sh to verify all patterns in one shot. Set Z3=/path/to/z3 if needed.

repro.zip

@yoonsh