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)