[QF_BV] How to create an expression alias instead of a variable definition

[ghost]

Consider the following formula:

Formula 1

(set-logic QF_BV)
(declare-const a0 Bool)
(declare-const a1 Bool)
(declare-const a2 Bool)
(declare-const a3 Bool)
(declare-const a4 Bool)
(declare-const a5 Bool)
(declare-const a6 Bool)
(declare-const a7 Bool)
(declare-const a8 Bool)
(declare-const a9 Bool)
(declare-const a10 Bool)
(declare-const a11 Bool)
(declare-const a12 Bool)
(declare-const a13 Bool)
(declare-const a14 Bool)
(declare-const a15 Bool)
(declare-const a16 Bool)
(declare-const a17 Bool)
(declare-const a18 Bool)
(declare-const a19 Bool)
(declare-const a20 Bool)
(declare-const a21 Bool)
(declare-const a22 Bool)
(declare-const a23 Bool)
(declare-const a24 Bool)
(declare-const a25 Bool)
(declare-const a26 Bool)
(declare-const a27 Bool)
(declare-const a28 Bool)
(declare-const a29 Bool)
(declare-const a30 Bool)
(declare-const a31 Bool)
(declare-const a32 Bool)
(declare-const a33 Bool)
(declare-const a34 Bool)
(declare-const a35 Bool)
(declare-const a36 Bool)
(declare-const a37 Bool)
(declare-const a38 Bool)
(declare-const a39 Bool)
(declare-const a40 Bool)
(declare-const a41 Bool)
(declare-const a42 Bool)
(declare-const a43 Bool)
(declare-const a44 Bool)
(declare-const a45 Bool)
(declare-const a46 Bool)
(declare-const a47 Bool)
(declare-const a48 Bool)
(declare-const a49 Bool)
(declare-const a50 Bool)
(declare-const a51 Bool)
(declare-const a52 Bool)
(declare-const a53 Bool)
(declare-const a54 Bool)
(declare-const a55 Bool)
(declare-const a56 Bool)
(declare-const a57 Bool)
(declare-const a58 Bool)
(declare-const a59 Bool)
(declare-const a60 Bool)
(declare-const a61 Bool)
(declare-const a62 Bool)
(declare-const a63 Bool)
(declare-const a64 Bool)
(declare-const a65 Bool)
(declare-const a66 Bool)
(declare-const a67 Bool)
(declare-const a68 Bool)
(declare-const a69 Bool)
(declare-const a70 Bool)
(declare-const a71 Bool)
(declare-const a72 Bool)
(declare-const a73 Bool)
(declare-const a74 Bool)
(declare-const a75 Bool)
(declare-const a76 Bool)
(declare-const a77 Bool)
(declare-const a78 Bool)
(declare-const a79 Bool)
(declare-const a80 Bool)
(declare-const a81 Bool)
(declare-const a82 Bool)
(declare-const a83 Bool)
(declare-const a84 Bool)
(declare-const a85 Bool)
(declare-const a86 Bool)
(declare-const a87 Bool)
(declare-const a88 Bool)
(declare-const a89 Bool)
(declare-const a90 Bool)
(declare-const a91 Bool)
(declare-const a92 Bool)
(declare-const a93 Bool)
(declare-const a94 Bool)
(declare-const a95 Bool)
(declare-const a96 Bool)
(declare-const a97 Bool)
(declare-const a98 Bool)
(declare-const a99 Bool)
(assert (and
(= (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd (_ bv0 8) (ite a0 (_ bv1 8) (_ bv0 8))) (ite a1 (_ bv1 8) (_ bv0 8))) (ite a2 (_ bv1 8) (_ bv0 8))) (ite a3 (_ bv1 8) (_ bv0 8))) (ite a4 (_ bv1 8) (_ bv0 8))) (ite a5 (_ bv1 8) (_ bv0 8))) (ite a6 (_ bv1 8) (_ bv0 8))) (ite a7 (_ bv1 8) (_ bv0 8))) (ite a8 (_ bv1 8) (_ bv0 8))) (ite a9 (_ bv1 8) (_ bv0 8))) (ite a10 (_ bv1 8) (_ bv0 8))) (ite a11 (_ bv1 8) (_ bv0 8))) (ite a12 (_ bv1 8) (_ bv0 8))) (ite a13 (_ bv1 8) (_ bv0 8))) (ite a14 (_ bv1 8) (_ bv0 8))) (ite a15 (_ bv1 8) (_ bv0 8))) (ite a16 (_ bv1 8) (_ bv0 8))) (ite a17 (_ bv1 8) (_ bv0 8))) (ite a18 (_ bv1 8) (_ bv0 8))) (ite a19 (_ bv1 8) (_ bv0 8))) (ite a20 (_ bv1 8) (_ bv0 8))) (ite a21 (_ bv1 8) (_ bv0 8))) (ite a22 (_ bv1 8) (_ bv0 8))) (ite a23 (_ bv1 8) (_ bv0 8))) (ite a24 (_ bv1 8) (_ bv0 8))) (ite a25 (_ bv1 8) (_ bv0 8))) (ite a26 (_ bv1 8) (_ bv0 8))) (ite a27 (_ bv1 8) (_ bv0 8))) (ite a28 (_ bv1 8) (_ bv0 8))) (ite a29 (_ bv1 8) (_ bv0 8))) (ite a30 (_ bv1 8) (_ bv0 8))) (ite a31 (_ bv1 8) (_ bv0 8))) (ite a32 (_ bv1 8) (_ bv0 8))) (ite a33 (_ bv1 8) (_ bv0 8))) (ite a34 (_ bv1 8) (_ bv0 8))) (ite a35 (_ bv1 8) (_ bv0 8))) (ite a36 (_ bv1 8) (_ bv0 8))) (ite a37 (_ bv1 8) (_ bv0 8))) (ite a38 (_ bv1 8) (_ bv0 8))) (ite a39 (_ bv1 8) (_ bv0 8))) (ite a40 (_ bv1 8) (_ bv0 8))) (ite a41 (_ bv1 8) (_ bv0 8))) (ite a42 (_ bv1 8) (_ bv0 8))) (ite a43 (_ bv1 8) (_ bv0 8))) (ite a44 (_ bv1 8) (_ bv0 8))) (ite a45 (_ bv1 8) (_ bv0 8))) (ite a46 (_ bv1 8) (_ bv0 8))) (ite a47 (_ bv1 8) (_ bv0 8))) (ite a48 (_ bv1 8) (_ bv0 8))) (ite a49 (_ bv1 8) (_ bv0 8))) (ite a50 (_ bv1 8) (_ bv0 8))) (ite a51 (_ bv1 8) (_ bv0 8))) (ite a52 (_ bv1 8) (_ bv0 8))) (ite a53 (_ bv1 8) (_ bv0 8))) (ite a54 (_ bv1 8) (_ bv0 8))) (ite a55 (_ bv1 8) (_ bv0 8))) (ite a56 (_ bv1 8) (_ bv0 8))) (ite a57 (_ bv1 8) (_ bv0 8))) (ite a58 (_ bv1 8) (_ bv0 8))) (ite a59 (_ bv1 8) (_ bv0 8))) (ite a60 (_ bv1 8) (_ bv0 8))) (ite a61 (_ bv1 8) (_ bv0 8))) (ite a62 (_ bv1 8) (_ bv0 8))) (ite a63 (_ bv1 8) (_ bv0 8))) (ite a64 (_ bv1 8) (_ bv0 8))) (ite a65 (_ bv1 8) (_ bv0 8))) (ite a66 (_ bv1 8) (_ bv0 8))) (ite a67 (_ bv1 8) (_ bv0 8))) (ite a68 (_ bv1 8) (_ bv0 8))) (ite a69 (_ bv1 8) (_ bv0 8))) (ite a70 (_ bv1 8) (_ bv0 8))) (ite a71 (_ bv1 8) (_ bv0 8))) (ite a72 (_ bv1 8) (_ bv0 8))) (ite a73 (_ bv1 8) (_ bv0 8))) (ite a74 (_ bv1 8) (_ bv0 8))) (ite a75 (_ bv1 8) (_ bv0 8))) (ite a76 (_ bv1 8) (_ bv0 8))) (ite a77 (_ bv1 8) (_ bv0 8))) (ite a78 (_ bv1 8) (_ bv0 8))) (ite a79 (_ bv1 8) (_ bv0 8))) (ite a80 (_ bv1 8) (_ bv0 8))) (ite a81 (_ bv1 8) (_ bv0 8))) (ite a82 (_ bv1 8) (_ bv0 8))) (ite a83 (_ bv1 8) (_ bv0 8))) (ite a84 (_ bv1 8) (_ bv0 8))) (ite a85 (_ bv1 8) (_ bv0 8))) (ite a86 (_ bv1 8) (_ bv0 8))) (ite a87 (_ bv1 8) (_ bv0 8))) (ite a88 (_ bv1 8) (_ bv0 8))) (ite a89 (_ bv1 8) (_ bv0 8))) (ite a90 (_ bv1 8) (_ bv0 8))) (ite a91 (_ bv1 8) (_ bv0 8))) (ite a92 (_ bv1 8) (_ bv0 8))) (ite a93 (_ bv1 8) (_ bv0 8))) (ite a94 (_ bv1 8) (_ bv0 8))) (ite a95 (_ bv1 8) (_ bv0 8))) (ite a96 (_ bv1 8) (_ bv0 8))) (ite a97 (_ bv1 8) (_ bv0 8))) (ite a98 (_ bv1 8) (_ bv0 8))) (ite a99 (_ bv1 8) (_ bv0 8))) (_ bv5 8))
))
(check-sat)

It takes few milliseconds to output sat. However, if I want to rewrite the formula by introducing aliases for expressions as following:

Formula 2

(set-logic QF_BV)
(declare-const a0 Bool)
(declare-const a1 Bool)
(declare-const a2 Bool)
(declare-const a3 Bool)
(declare-const a4 Bool)
(declare-const a5 Bool)
(declare-const a6 Bool)
(declare-const a7 Bool)
(declare-const a8 Bool)
(declare-const a9 Bool)
(declare-const a10 Bool)
(declare-const a11 Bool)
(declare-const a12 Bool)
(declare-const a13 Bool)
(declare-const a14 Bool)
(declare-const a15 Bool)
(declare-const a16 (_ BitVec 8))
(declare-const a17 (_ BitVec 8))
(declare-const a18 (_ BitVec 8))
(declare-const a19 (_ BitVec 8))
(declare-const a20 (_ BitVec 8))
(declare-const a21 (_ BitVec 8))
(declare-const a22 (_ BitVec 8))
(declare-const a23 (_ BitVec 8))
(declare-const a24 (_ BitVec 8))
(declare-const a25 (_ BitVec 8))
(declare-const a26 (_ BitVec 8))
(declare-const a27 (_ BitVec 8))
(declare-const a28 (_ BitVec 8))
(declare-const a29 (_ BitVec 8))
(declare-const a30 (_ BitVec 8))
(declare-const a31 (_ BitVec 8))
(assert (and
(= (ite a15 (bvadd a31 (_ bv1 8)) a31) (_ bv5 8))
(= a16 (_ bv0 8))
(= a17 (ite a0 (bvadd a16 (_ bv1 8)) a16))
(= a18 (ite a1 (bvadd a17 (_ bv1 8)) a17))
(= a19 (ite a2 (bvadd a18 (_ bv1 8)) a18))
(= a20 (ite a3 (bvadd a19 (_ bv1 8)) a19))
(= a21 (ite a4 (bvadd a20 (_ bv1 8)) a20))
(= a22 (ite a5 (bvadd a21 (_ bv1 8)) a21))
(= a23 (ite a6 (bvadd a22 (_ bv1 8)) a22))
(= a24 (ite a7 (bvadd a23 (_ bv1 8)) a23))
(= a25 (ite a8 (bvadd a24 (_ bv1 8)) a24))
(= a26 (ite a9 (bvadd a25 (_ bv1 8)) a25))
(= a27 (ite a10 (bvadd a26 (_ bv1 8)) a26))
(= a28 (ite a11 (bvadd a27 (_ bv1 8)) a27))
(= a29 (ite a12 (bvadd a28 (_ bv1 8)) a28))
(= a30 (ite a13 (bvadd a29 (_ bv1 8)) a29))
(= a31 (ite a14 (bvadd a30 (_ bv1 8)) a30))
))
(check-sat)

See how much shorter it is. But for some reason Z3 is x100 times slower on this example. Why? I guess in the first example Z3 is using all the values as intermediate results and discard them after they are no longer needed, but in the second example Z3 keeps track of all auxiliary variables in case get-model is invoked.

How can I instruct Z3 to consider all of the auxiliary variables as aliases for expressions and exclude them from the final model? I don't even want to call get-model at all, so Z3 can discard all variables, all I want is to know the satisfiability. Basically, what is the optimal way to define an alias for an expression that may occur multiple times in the formula?

Thanks.

[NikolajBjorner]

Use "define-const" and "define-fun"