Assertion violation for QF_BV instance at ../src/sat/sat_integrity_checker.cpp:91

[rainoftime]

Hi,
For this formula:

satintegritycheck91.txt

-----a smaller instance----------

(set-logic QF_BV)
(set-option :model_validate true)
(set-option :model true)
(set-option :sat.unit_walk true)
(declare-const v0 Bool)
(declare-const v4 Bool)
(declare-const v6 Bool)
(declare-const v15 Bool)
(declare-const bv_4-0 (_ BitVec 4))
(assert (xor (= (bvurem bv_4-0 bv_4-0) (bvurem bv_4-0 bv_4-0) (bvurem bv_4-0 bv_4-0) bv_4-0 (bvurem bv_4-0 bv_4-0)) v4 v15 v0 (bvult #x243 #x243) v6))
(check-sat-using (then simplify bit-blast sat))

Z3 (compiled with debug mode) throws out an assertion violation:

verifying solution
unsat
Failed to verify: s.value(c[i]) == l_false
ASSERTION VIOLATION
File: ../src/sat/sat_integrity_checker.cpp
Line: 91
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 16.04
Commit: fcbf660 (master branch)

[rainoftime]

I guess this issue is caused by the unit walk algorithm for SAT solving.
Since the unit walk implementation may not be actively maintained, this issue might be closed.

[rainoftime]

Here is a much smaller instance

(set-logic QF_BV)
(set-option :model_validate true)
(set-option :model true)
(set-option :sat.unit_walk true)
(declare-const v0 Bool)
(declare-const v4 Bool)
(declare-const v6 Bool)
(declare-const v15 Bool)
(declare-const bv_4-0 (_ BitVec 4))
(assert (xor (= (bvurem bv_4-0 bv_4-0) (bvurem bv_4-0 bv_4-0) (bvurem bv_4-0 bv_4-0) bv_4-0 (bvurem bv_4-0 bv_4-0)) v4 v15 v0 (bvult #x243 #x243) v6))
(check-sat-using (then simplify bit-blast sat))

[NikolajBjorner]

thanks