[improvement] Essentially the same query is much slower if cut into two

[msooseth]

Hi,

This SMT2:

(set-logic ALL)
(declare-const txdata (Array (_ BitVec 256) (_ BitVec 8)))
(declare-const txdata_length (_ BitVec 256))
(declare-const arg1 (_ BitVec 256))
(declare-const callvalue_0 (_ BitVec 256))
(define-fun max ((a (_ BitVec 256)) (b (_ BitVec 256))) (_ BitVec 256) (ite (bvult a b) b a))
(assert (and (bvuge (max (_ bv36 256) txdata_length) (_ bv36 256)) (bvult (max (_ bv36 256) txdata_length) (_ bv18446744073709551616 256))))
(assert (and (bvuge arg1 (_ bv0 256)) (bvule arg1 (_ bv115792089237316195423570985008687907853269984665640564039457584007913129639935 256))))
(declare-const mystuff (_ BitVec 256))
(assert (= (ite (= (_ bv0 256) (ite (= arg1 (_ bv0 256)) (_ bv0 256) mystuff)) (_ bv1 256) (_ bv0 256)) (_ bv0 256)))
(assert (not (= (_ bv1 256) (_ bv0 256))))
(assert (= (_ bv0 256) (_ bv0 256)))
(assert (not (= (ite (= callvalue_0 (_ bv0 256)) (_ bv1 256) (_ bv0 256)) (_ bv0 256))))
(check-sat)
(assert (= mystuff (bvsdiv (_ bv0 256) arg1)))
(check-sat)

Has two check-sat-s, the first time mystuff is not defined, later it is defined to be (bvsdiv (_ bv0 256) arg1)). This gives sat immediately and then runs for 500+ seconds without a result for the second check-sat. If however I replace mystuff in the original query with (bvsdiv (_ bv0 256) arg1)), and remove the definition & the 2nd check-sat, then it returns unsat in about 20 seconds. This is odd.

To be clear, the second query is:

(reset)
(set-logic ALL)
(declare-const txdata (Array (_ BitVec 256) (_ BitVec 8)))
(declare-const txdata_length (_ BitVec 256))
(declare-const arg1 (_ BitVec 256))
(declare-const callvalue_0 (_ BitVec 256))
(define-fun max ((a (_ BitVec 256)) (b (_ BitVec 256))) (_ BitVec 256) (ite (bvult a b) b a))
(assert (and (bvuge (max (_ bv36 256) txdata_length) (_ bv36 256)) (bvult (max (_ bv36 256) txdata_length) (_ bv18446744073709551616 256))))
(assert (and (bvuge arg1 (_ bv0 256)) (bvule arg1 (_ bv115792089237316195423570985008687907853269984665640564039457584007913129639935 256))))
; (evm_bvsdiv (_ bv0 256) arg1)
(assert (= (ite (= (_ bv0 256) (ite (= arg1 (_ bv0 256)) (_ bv0 256) (bvsdiv (_ bv0 256) arg1))) (_ bv1 256) (_ bv0 256)) (_ bv0 256)))
(assert (not (= (_ bv1 256) (_ bv0 256))))
(assert (= (_ bv0 256) (_ bv0 256)))
(assert (not (= (ite (= callvalue_0 (_ bv0 256)) (_ bv1 256) (_ bv0 256)) (_ bv0 256))))
(check-sat)

My expectation was that it shouldn't be such a radical performance difference?

Not a bug, just a performance bug. Running Z3 version 4.12.2

[NikolajBjorner]

It is because pre-processing in the main mode of Z3 does not work well with incrementality. So far Z3 used tactics that are one-shot pre-processing hammes to simplify goals. Your problem cannot be solved if you keep bsdiv because bv reasoning is dead with 256 let alone 32 bits for bsdiv, bvudiv, bvsrem, ..

I am working on incremental pre-processing that is transparent for push/pop. It happens not to solve your problem (it is enabled by passing sat.smt=true from the command line) either. It is not directly fixable within the current implementation because mystuff gets bit-blasted for the first solver call and the simplified version of the formula that uses mystuff is not going to be re-created. I end up not substituting in solutions for variables in previous constraints. The alternative is to substitute mystuff into the formulas where they occur, simplify them, and reassert the simplified formulas. I don't think this stratetegy always works well. So some users would suffer from this behavior. Therefore, you are more likely much better off using z3 with separate queries in one-shot modes for this methdology.

[msooseth]

Oh wow, thank you for the detailed explanation. That makes a lot of sense. Thank you!