Bit-vector regression

[LeventErkok]

The following benchmark was solved in about 36 seconds (it is sat), using z3 compiled on September 23; about 3 days ago.

A fresh compile of z3 returns unknown for it.

I'm noticing that, if I remove:

(set-option :smt.auto_config false)
(set-option :smt.relevancy 0)

then, latest z3 also solves it as well, but in 3m36s; about 6 times slower than before. These settings were obtained after the discussion in https://github.com/Z3Prover/z3/issues/2075

I'd be curious to know if there's a new set of settings I can use to recover the performance.

(set-option :global-declarations true)
(set-option :diagnostic-output-channel "stdout")
(set-option :smt.auto_config false)
(set-option :smt.relevancy 0)
(set-option :produce-models true)
(set-logic BV)
(define-fun s4 () (_ BitVec 1) #b0)
(declare-fun s0 () (_ BitVec 64)) ; tracks user variable "mask"
(declare-fun s1 () (_ BitVec 64)) ; tracks user variable "mult"
(assert (forall ((s2 (_ BitVec 64)))
            (let ((s3 ((_ extract 7 7) s2)))
            (let ((s5 (distinct s3 s4)))
            (let ((s6 (bvand s0 s2)))
            (let ((s7 (bvmul s1 s6)))
            (let ((s8 ((_ extract 56 56) s7)))
            (let ((s9 (distinct s4 s8)))
            (let ((s10 (= s5 s9)))
            (let ((s11 ((_ extract 15 15) s2)))
            (let ((s12 (distinct s4 s11)))
            (let ((s13 ((_ extract 57 57) s7)))
            (let ((s14 (distinct s4 s13)))
            (let ((s15 (= s12 s14)))
            (let ((s16 ((_ extract 23 23) s2)))
            (let ((s17 (distinct s4 s16)))
            (let ((s18 ((_ extract 58 58) s7)))
            (let ((s19 (distinct s4 s18)))
            (let ((s20 (= s17 s19)))
            (let ((s21 ((_ extract 31 31) s2)))
            (let ((s22 (distinct s4 s21)))
            (let ((s23 ((_ extract 59 59) s7)))
            (let ((s24 (distinct s4 s23)))
            (let ((s25 (= s22 s24)))
            (let ((s26 ((_ extract 39 39) s2)))
            (let ((s27 (distinct s4 s26)))
            (let ((s28 ((_ extract 60 60) s7)))
            (let ((s29 (distinct s4 s28)))
            (let ((s30 (= s27 s29)))
            (let ((s31 ((_ extract 47 47) s2)))
            (let ((s32 (distinct s4 s31)))
            (let ((s33 ((_ extract 61 61) s7)))
            (let ((s34 (distinct s4 s33)))
            (let ((s35 (= s32 s34)))
            (let ((s36 ((_ extract 55 55) s2)))
            (let ((s37 (distinct s4 s36)))
            (let ((s38 ((_ extract 62 62) s7)))
            (let ((s39 (distinct s4 s38)))
            (let ((s40 (= s37 s39)))
            (let ((s41 ((_ extract 63 63) s2)))
            (let ((s42 (distinct s4 s41)))
            (let ((s43 ((_ extract 63 63) s7)))
            (let ((s44 (distinct s4 s43)))
            (let ((s45 (= s42 s44)))
            (let ((s46 (and s40 s45)))
            (let ((s47 (and s35 s46)))
            (let ((s48 (and s30 s47)))
            (let ((s49 (and s25 s48)))
            (let ((s50 (and s20 s49)))
            (let ((s51 (and s15 s50)))
            (let ((s52 (and s10 s51)))
            s52)))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)

[NikolajBjorner]

Appreciated and suggesting the mbqi loop in the smt core has regressed or so. Possibly going forward we can try

 (check-sat-using (and-then simplify smtfd))

smtfd currently behaves comparatively poorly on the domain it is supposed to be good at, but for this particular example it is amazing.

[LeventErkok]

Wow; smtfd instantly solves it! I hope it stays that way!

Thanks..