During a program synthesis task I hit the following equivalence, which is based on mixed-boolean-arithmetic logic and that I can't seem to be able to prove with Z3 in a reasonable amount of time (some seconds or minutes). I'm following a counter-example driven approach (CEGIS), feeding the original expression and the synthesis candidate to a distinct query: if no counter-examples are found the synthesis is correct.
(set-logic QF_BV)
(declare-fun y () (_ BitVec 64))
(declare-fun x () (_ BitVec 64))
(assert (let ((a!1 (bvsub (bvsub (bvsub x #x0000000000000002) y)
(bvshl (bvor x (bvnot y)) #x0000000000000001))))
(let ((a!2 (bvmul (bvand (bvxor a!1 x) (bvnot y))
(bvand y (bvnot (bvxor a!1 x))))))
(let ((a!3 (bvadd (bvmul (bvor (bvxor a!1 x) y) (bvand (bvxor a!1 x) y)) a!2)))
(distinct a!3 (bvmul y y))))))
(check-sat)
I know the equivalence to hold just fine for reduced bit-width bit-vectors (e.g. 8 or 16), so I was wondering if Z3 is employing any technique to first prove the bit-width reduced version of the query and then extend the result to the full-width version.
I tried the Z3 bv-size-reduction tactic, but it doesn't seem to fit my requirements because it's meant to reduce the size of the constants and not of the symbolic bit-vectors. Moreover, the implementation of the Speeding-up Quantified Bit-Vector Solving Bit-Width Reductions and Extensions paper doesn't seem to work out for this specific case, because no useful counter-model is generated, keeping the size of the problem unaltered.
I'm not a SAT/SMT person, as I barely use tools like Z3 as black boxes to play around with synthesis problems, so I was wondering:
- Is there anything I can do to reduce the bit-width of the bit-vectors, prove the reduced query and extend the results to the full-width query?
- Is there any other viable way to prove the unsatisfiability of the aforementioned query?