diff options
Diffstat (limited to 'test/Expr')
| -rw-r--r-- | test/Expr/print-smt-let.smt2.good | 14 |
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) ) ) ) |