Skip to content

Fix setup_relevancy for relevancy-dependent case split strategies#7662

Merged
NikolajBjorner merged 1 commit intoZ3Prover:masterfrom
CanCebeci:master
May 27, 2025
Merged

Fix setup_relevancy for relevancy-dependent case split strategies#7662
NikolajBjorner merged 1 commit intoZ3Prover:masterfrom
CanCebeci:master

Conversation

@CanCebeci
Copy link
Contributor

Quantifier-free bitvector problems break with auto_config=false smt.case_split=3, 4 and 5. This is because setup_relevancy silently disables relevancy, and does so after the sanity checks in mk_case_split_queue.

Below is a short unsat example that is fixed by the commit.

Before the fix, relevancy-dependent strategies returned sat with most random random seeds, unsat with some. Also, moving the first assertion to the end made the query consistently unsat.

(declare-const x (_ BitVec 32))
(declare-const y Int)
(declare-const z Bool)

(assert (or  (= #x00000000 x) (= 0 y)))

(assert (bvslt #x00000000 x))    
(assert (< 0 y))

(check-sat)

@NikolajBjorner NikolajBjorner merged commit b44c897 into Z3Prover:master May 27, 2025
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants