Print nested let-abbreviations in ExprSMTLIBPrinter

This patch introduces nested let-abbreviations in the ExprSMTLIBPrinter
to reduce the size of the SMTLIBv2 queries and the corresponding processing
time (bugfix for #170).

The current implementation of the let abbreviation mode does not consider
expression intra-dependencies and prints all abbreviations in the same
let scope. For a (simplified) example, it prints

(assert (let ( (?B1 (A + B)) (?B2 (A + B + C)) ) (= ?B1 ?B2) ) ).

This is extremely inefficient if the expressions (and there many of these!)
extensively reuse their subexpressions. Therefore, it's better to print
the query with nested let-expressions by reusing existing expression bindings
in the new let scope:

(assert (let ( (?B1 (A + B)) ) (let ( (?B2 (?B1 + C)) ) (= ?B1 ?B2) ) ) ).

This patch adds a new function ExprSMTLIBPrinter::scanBindingExprDeps() that
scans bindings for expression dependencies. The result is a vector of
new bindings (orderedBindings) that represents the expression dependency tree.

When printing in the let-abbreviation mode, the new code starts with
abbreviating expressions that have no dependencies and then gradually makes
these new bindings available in the upcoming let-scopes where expressions
with dependencies reuse them.

The effect of nested let-abbreviations is comparable to :named abbreviations.
However, the latter mode is not supported by the majority of the solvers.

1 files changed, 7 insertions, 7 deletions

diff --git a/test/Expr/print-smt-let.smt2.good b/test/Expr/print-smt-let.smt2.good
index 3fb9b35c..cb387fef 100644
--- a/test/Expr/print-smt-let.smt2.good
+++ b/test/Expr/print-smt-let.smt2.good
@@ -866,7 +866,7 @@
 (assert (=  (select const_arr2 (_ bv1 32) ) (_ bv101 8) ) )
 (assert (=  (select const_arr2 (_ bv2 32) ) (_ bv115 8) ) )
 (assert (=  (select const_arr2 (_ bv3 32) ) (_ bv0 8) ) )
-(assert (let ( (?B3 ((_ extract 31  0)  (bvadd  (_ bv31312 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) ) (?B2 (bvadd  (_ bv31312 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (?B1 (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (and  (and  (=  (concat  (select  unnamed (_ bv3 32) ) (concat  (select  unnamed (_ bv2 32) ) (concat  (select  unnamed (_ bv1 32) ) (select  unnamed (_ bv0 32) ) ) ) ) (concat  (select  const_arr2 (bvadd  (_ bv3 32) ?B3 ) ) (concat  (select  const_arr2 (bvadd  (_ bv2 32) ?B3 ) ) (concat  (select  const_arr2 (bvadd  (_ bv1 32) ?B3 ) ) (select  const_arr2 ?B3 ) ) ) ) ) (=  false (bvult  ?B1 (_ bv13 64) ) ) ) (bvult  ?B2 (_ bv1 64) ) ) ) )
+(assert (let ( (?B1 (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (let ( (?B2 (bvadd  (_ bv31312 64) ?B1 ) ) ) (let ( (?B3 ((_ extract 31  0)  ?B2 ) ) ) (and  (and  (=  (concat  (select  unnamed (_ bv3 32) ) (concat  (select  unnamed (_ bv2 32) ) (concat  (select  unnamed (_ bv1 32) ) (select  unnamed (_ bv0 32) ) ) ) ) (concat  (select  const_arr2 (bvadd  (_ bv3 32) ?B3 ) ) (concat  (select  const_arr2 (bvadd  (_ bv2 32) ?B3 ) ) (concat  (select  const_arr2 (bvadd  (_ bv1 32) ?B3 ) ) (select  const_arr2 ?B3 ) ) ) ) ) (=  false (bvult  ?B1 (_ bv13 64) ) ) ) (bvult  ?B2 (_ bv1 64) ) ) ) ) ) )
 (check-sat)
 (get-value ( (select unnamed (_ bv0 32) ) ) )
 (get-value ( (select unnamed (_ bv1 32) ) ) )
@@ -883,7 +883,7 @@
 (set-logic QF_AUFBV )
 (declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
-(assert (let ( (?B3 ((_ extract 31  0)  (bvadd  (_ bv18446744073709533360 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) ) (?B2 (bvadd  (_ bv18446744073709533360 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (?B1 (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (and  (and  (and  (and  (and  (=  false (=  (concat  (select  unnamed (_ bv3 32) ) (concat  (select  unnamed (_ bv2 32) ) (concat  (select  unnamed (_ bv1 32) ) (select  unnamed (_ bv0 32) ) ) ) ) (concat  (select  unnamed (bvadd  (_ bv3 32) ?B3 ) ) (concat  (select  unnamed (bvadd  (_ bv2 32) ?B3 ) ) (concat  (select  unnamed (bvadd  (_ bv1 32) ?B3 ) ) (select  unnamed ?B3 ) ) ) ) ) ) (=  false (bvult  ?B1 (_ bv13 64) ) ) ) (=  false (bvult  (bvadd  (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) (=  false (bvult  (bvadd  (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) (=  false (bvult  (bvadd  (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) (bvult  ?B2 (_ bv1 64) ) ) ) )
+(assert (let ( (?B1 (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (let ( (?B2 (bvadd  (_ bv18446744073709533360 64) ?B1 ) ) ) (let ( (?B3 ((_ extract 31  0)  ?B2 ) ) ) (and  (and  (and  (and  (and  (=  false (=  (concat  (select  unnamed (_ bv3 32) ) (concat  (select  unnamed (_ bv2 32) ) (concat  (select  unnamed (_ bv1 32) ) (select  unnamed (_ bv0 32) ) ) ) ) (concat  (select  unnamed (bvadd  (_ bv3 32) ?B3 ) ) (concat  (select  unnamed (bvadd  (_ bv2 32) ?B3 ) ) (concat  (select  unnamed (bvadd  (_ bv1 32) ?B3 ) ) (select  unnamed ?B3 ) ) ) ) ) ) (=  false (bvult  ?B1 (_ bv13 64) ) ) ) (=  false (bvult  (bvadd  (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) (=  false (bvult  (bvadd  (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) (=  false (bvult  (bvadd  (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) (bvult  ?B2 (_ bv1 64) ) ) ) ) ) )
 (check-sat)
 (get-value ( (select unnamed_1 (_ bv0 32) ) ) )
 (get-value ( (select unnamed_1 (_ bv1 32) ) ) )
@@ -905,7 +905,7 @@
 (assert (=  (select const_arr5 (_ bv1 32) ) (_ bv171 8) ) )
 (assert (=  (select const_arr5 (_ bv2 32) ) (_ bv171 8) ) )
 (assert (=  (select const_arr5 (_ bv3 32) ) (_ bv171 8) ) )
-(assert (let ( (?B3 ((_ extract 31  0)  (bvadd  (_ bv18446744073709533328 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) ) (?B2 (bvadd  (_ bv18446744073709533328 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (?B1 (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (and  (and  (and  (and  (and  (and  (=  (concat  (select  unnamed (_ bv3 32) ) (concat  (select  unnamed (_ bv2 32) ) (concat  (select  unnamed (_ bv1 32) ) (select  unnamed (_ bv0 32) ) ) ) ) (concat  (select  const_arr5 (bvadd  (_ bv3 32) ?B3 ) ) (concat  (select  const_arr5 (bvadd  (_ bv2 32) ?B3 ) ) (concat  (select  const_arr5 (bvadd  (_ bv1 32) ?B3 ) ) (select  const_arr5 ?B3 ) ) ) ) ) (=  false (bvult  ?B1 (_ bv13 64) ) ) ) (=  false (bvult  (bvadd  (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) (=  false (bvult  (bvadd  (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) (=  false (bvult  (bvadd  (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) (=  false (bvult  (bvadd  (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) (bvult  ?B2 (_ bv1 64) ) ) ) )
+(assert (let ( (?B1 (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (let ( (?B2 (bvadd  (_ bv18446744073709533328 64) ?B1 ) ) ) (let ( (?B3 ((_ extract 31  0)  ?B2 ) ) ) (and  (and  (and  (and  (and  (and  (=  (concat  (select  unnamed (_ bv3 32) ) (concat  (select  unnamed (_ bv2 32) ) (concat  (select  unnamed (_ bv1 32) ) (select  unnamed (_ bv0 32) ) ) ) ) (concat  (select  const_arr5 (bvadd  (_ bv3 32) ?B3 ) ) (concat  (select  const_arr5 (bvadd  (_ bv2 32) ?B3 ) ) (concat  (select  const_arr5 (bvadd  (_ bv1 32) ?B3 ) ) (select  const_arr5 ?B3 ) ) ) ) ) (=  false (bvult  ?B1 (_ bv13 64) ) ) ) (=  false (bvult  (bvadd  (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) (=  false (bvult  (bvadd  (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) (=  false (bvult  (bvadd  (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) (=  false (bvult  (bvadd  (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) (bvult  ?B2 (_ bv1 64) ) ) ) ) ) )
 (check-sat)
 (get-value ( (select unnamed_1 (_ bv0 32) ) ) )
 (get-value ( (select unnamed_1 (_ bv1 32) ) ) )
@@ -939,7 +939,7 @@
 (assert (=  (select const_arr1 (_ bv13 32) ) (_ bv0 8) ) )
 (assert (=  (select const_arr1 (_ bv14 32) ) (_ bv0 8) ) )
 (assert (=  (select const_arr1 (_ bv15 32) ) (_ bv0 8) ) )
-(assert (let ( (?B2 ((_ extract 31  0)  (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (?B1 (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (and  (=  (concat  (select  unnamed (_ bv3 32) ) (concat  (select  unnamed (_ bv2 32) ) (concat  (select  unnamed (_ bv1 32) ) (select  unnamed (_ bv0 32) ) ) ) ) (concat  (select  const_arr1 (bvadd  (_ bv3 32) ?B2 ) ) (concat  (select  const_arr1 (bvadd  (_ bv2 32) ?B2 ) ) (concat  (select  const_arr1 (bvadd  (_ bv1 32) ?B2 ) ) (select  const_arr1 ?B2 ) ) ) ) ) (bvult  ?B1 (_ bv13 64) ) ) ) )
+(assert (let ( (?B1 (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (let ( (?B2 ((_ extract 31  0)  ?B1 ) ) ) (and  (=  (concat  (select  unnamed (_ bv3 32) ) (concat  (select  unnamed (_ bv2 32) ) (concat  (select  unnamed (_ bv1 32) ) (select  unnamed (_ bv0 32) ) ) ) ) (concat  (select  const_arr1 (bvadd  (_ bv3 32) ?B2 ) ) (concat  (select  const_arr1 (bvadd  (_ bv2 32) ?B2 ) ) (concat  (select  const_arr1 (bvadd  (_ bv1 32) ?B2 ) ) (select  const_arr1 ?B2 ) ) ) ) ) (bvult  ?B1 (_ bv13 64) ) ) ) ) )
 (check-sat)
 (get-value ( (select unnamed (_ bv0 32) ) ) )
 (get-value ( (select unnamed (_ bv1 32) ) ) )
@@ -961,7 +961,7 @@
 (assert (=  (select const_arr4 (_ bv1 32) ) (_ bv171 8) ) )
 (assert (=  (select const_arr4 (_ bv2 32) ) (_ bv171 8) ) )
 (assert (=  (select const_arr4 (_ bv3 32) ) (_ bv171 8) ) )
-(assert (let ( (?B3 ((_ extract 31  0)  (bvadd  (_ bv111120 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) ) (?B2 (bvadd  (_ bv111120 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (?B1 (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (and  (and  (and  (and  (=  (concat  (select  unnamed (_ bv3 32) ) (concat  (select  unnamed (_ bv2 32) ) (concat  (select  unnamed (_ bv1 32) ) (select  unnamed (_ bv0 32) ) ) ) ) (concat  (select  const_arr4 (bvadd  (_ bv3 32) ?B3 ) ) (concat  (select  const_arr4 (bvadd  (_ bv2 32) ?B3 ) ) (concat  (select  const_arr4 (bvadd  (_ bv1 32) ?B3 ) ) (select  const_arr4 ?B3 ) ) ) ) ) (=  false (bvult  ?B1 (_ bv13 64) ) ) ) (=  false (bvult  (bvadd  (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) (=  false (bvult  (bvadd  (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) (bvult  ?B2 (_ bv1 64) ) ) ) )
+(assert (let ( (?B1 (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (let ( (?B2 (bvadd  (_ bv111120 64) ?B1 ) ) ) (let ( (?B3 ((_ extract 31  0)  ?B2 ) ) ) (and  (and  (and  (and  (=  (concat  (select  unnamed (_ bv3 32) ) (concat  (select  unnamed (_ bv2 32) ) (concat  (select  unnamed (_ bv1 32) ) (select  unnamed (_ bv0 32) ) ) ) ) (concat  (select  const_arr4 (bvadd  (_ bv3 32) ?B3 ) ) (concat  (select  const_arr4 (bvadd  (_ bv2 32) ?B3 ) ) (concat  (select  const_arr4 (bvadd  (_ bv1 32) ?B3 ) ) (select  const_arr4 ?B3 ) ) ) ) ) (=  false (bvult  ?B1 (_ bv13 64) ) ) ) (=  false (bvult  (bvadd  (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) (=  false (bvult  (bvadd  (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) (bvult  ?B2 (_ bv1 64) ) ) ) ) ) )
 (check-sat)
 (get-value ( (select unnamed_1 (_ bv0 32) ) ) )
 (get-value ( (select unnamed_1 (_ bv1 32) ) ) )
@@ -995,7 +995,7 @@
 (assert (=  (select const_arr3 (_ bv13 32) ) (_ bv0 8) ) )
 (assert (=  (select const_arr3 (_ bv14 32) ) (_ bv0 8) ) )
 (assert (=  (select const_arr3 (_ bv15 32) ) (_ bv0 8) ) )
-(assert (let ( (?B3 ((_ extract 31  0)  (bvadd  (_ bv31760 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) ) (?B2 (bvadd  (_ bv31760 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (?B1 (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (and  (and  (and  (=  (concat  (select  unnamed (_ bv3 32) ) (concat  (select  unnamed (_ bv2 32) ) (concat  (select  unnamed (_ bv1 32) ) (select  unnamed (_ bv0 32) ) ) ) ) (concat  (select  const_arr3 (bvadd  (_ bv3 32) ?B3 ) ) (concat  (select  const_arr3 (bvadd  (_ bv2 32) ?B3 ) ) (concat  (select  const_arr3 (bvadd  (_ bv1 32) ?B3 ) ) (select  const_arr3 ?B3 ) ) ) ) ) (=  false (bvult  ?B1 (_ bv13 64) ) ) ) (=  false (bvult  (bvadd  (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) (bvult  ?B2 (_ bv13 64) ) ) ) )
+(assert (let ( (?B1 (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (let ( (?B2 (bvadd  (_ bv31760 64) ?B1 ) ) ) (let ( (?B3 ((_ extract 31  0)  ?B2 ) ) ) (and  (and  (and  (=  (concat  (select  unnamed (_ bv3 32) ) (concat  (select  unnamed (_ bv2 32) ) (concat  (select  unnamed (_ bv1 32) ) (select  unnamed (_ bv0 32) ) ) ) ) (concat  (select  const_arr3 (bvadd  (_ bv3 32) ?B3 ) ) (concat  (select  const_arr3 (bvadd  (_ bv2 32) ?B3 ) ) (concat  (select  const_arr3 (bvadd  (_ bv1 32) ?B3 ) ) (select  const_arr3 ?B3 ) ) ) ) ) (=  false (bvult  ?B1 (_ bv13 64) ) ) ) (=  false (bvult  (bvadd  (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) (bvult  ?B2 (_ bv13 64) ) ) ) ) ) )
 (check-sat)
 (get-value ( (select unnamed (_ bv0 32) ) ) )
 (get-value ( (select unnamed (_ bv1 32) ) ) )
@@ -1012,7 +1012,7 @@
 (set-logic QF_AUFBV )
 (declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
-(assert (let ( (?B3 ((_ extract 31  0)  (bvadd  (_ bv18446744073709532800 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) ) (?B2 (bvadd  (_ bv18446744073709532800 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (?B1 (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (and  (and  (and  (and  (and  (and  (and  (=  (concat  (select  unnamed (_ bv3 32) ) (concat  (select  unnamed (_ bv2 32) ) (concat  (select  unnamed (_ bv1 32) ) (select  unnamed (_ bv0 32) ) ) ) ) (concat  (select  unnamed_1 (bvadd  (_ bv3 32) ?B3 ) ) (concat  (select  unnamed_1 (bvadd  (_ bv2 32) ?B3 ) ) (concat  (select  unnamed_1 (bvadd  (_ bv1 32) ?B3 ) ) (select  unnamed_1 ?B3 ) ) ) ) ) (=  false (bvult  ?B1 (_ bv13 64) ) ) ) (=  false (bvult  (bvadd  (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) (=  false (bvult  (bvadd  (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) (=  false (bvult  (bvadd  (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) (=  false (bvult  (bvadd  (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) (=  false (bvult  (bvadd  (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) (bvult  ?B2 (_ bv1 64) ) ) ) )
+(assert (let ( (?B1 (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (let ( (?B2 (bvadd  (_ bv18446744073709532800 64) ?B1 ) ) ) (let ( (?B3 ((_ extract 31  0)  ?B2 ) ) ) (and  (and  (and  (and  (and  (and  (and  (=  (concat  (select  unnamed (_ bv3 32) ) (concat  (select  unnamed (_ bv2 32) ) (concat  (select  unnamed (_ bv1 32) ) (select  unnamed (_ bv0 32) ) ) ) ) (concat  (select  unnamed_1 (bvadd  (_ bv3 32) ?B3 ) ) (concat  (select  unnamed_1 (bvadd  (_ bv2 32) ?B3 ) ) (concat  (select  unnamed_1 (bvadd  (_ bv1 32) ?B3 ) ) (select  unnamed_1 ?B3 ) ) ) ) ) (=  false (bvult  ?B1 (_ bv13 64) ) ) ) (=  false (bvult  (bvadd  (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) (=  false (bvult  (bvadd  (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) (=  false (bvult  (bvadd  (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) (=  false (bvult  (bvadd  (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) (=  false (bvult  (bvadd  (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) (bvult  ?B2 (_ bv1 64) ) ) ) ) ) )
 (check-sat)
 (get-value ( (select unnamed_1 (_ bv0 32) ) ) )
 (get-value ( (select unnamed_1 (_ bv1 32) ) ) )