diff options
Diffstat (limited to 'test/Expr/print-smt-let.smt2.good')
| -rw-r--r-- | test/Expr/print-smt-let.smt2.good | 381 |
1 files changed, 47 insertions, 334 deletions
diff --git a/test/Expr/print-smt-let.smt2.good b/test/Expr/print-smt-let.smt2.good index d14eece6..3fb9b35c 100644 --- a/test/Expr/print-smt-let.smt2.good +++ b/test/Expr/print-smt-let.smt2.good @@ -380,8 +380,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (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) ) ) ) ) ) ) ) ) (bvult (bvadd (_ bv31312 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (and (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) (= false (bvult ?B1 (_ bv13 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -393,9 +392,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (bvult (bvadd (_ bv31760 64) ?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) ) ) ) ) ) ) ) ) (and (and (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) (= false (bvult ?B1 (_ bv13 64) ) ) ) (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -407,10 +404,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?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) ) ) ) ) ) ) ) ) (bvult (bvadd (_ bv111120 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (and (and (and (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) (= false (bvult ?B1 (_ bv13 64) ) ) ) (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -422,11 +416,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (and (and (and (and (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) (= 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) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -438,12 +428,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) (= 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) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -455,13 +440,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) (= 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) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -473,14 +452,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= (_ bv18446744073657921168 64) ?B1 )) ) +(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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= (_ bv18446744073657921168 64) ?B1 ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -492,14 +464,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744069414584319 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744069414584319 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -511,14 +476,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744071562067967 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744071562067967 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -530,14 +488,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744072635809791 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744072635809791 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -549,14 +500,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073172680703 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073172680703 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -568,14 +512,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073441116159 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073441116159 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -587,14 +524,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073575333887 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073575333887 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -606,14 +536,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073642442751 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073642442751 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -625,14 +548,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073675997183 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073675997183 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -644,14 +560,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073692774399 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073692774399 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -663,14 +572,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073701163007 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073701163007 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -682,14 +584,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073705357311 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073705357311 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -701,14 +596,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073707454463 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073707454463 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -720,14 +608,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073708503039 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073708503039 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -739,14 +620,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709027327 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709027327 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -758,14 +632,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709289471 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709289471 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -777,14 +644,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709420543 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709420543 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -796,14 +656,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709486079 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709486079 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -815,14 +668,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709518847 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709518847 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -834,14 +680,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709535231 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709535231 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -853,14 +692,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709543423 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709543423 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -872,14 +704,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709547519 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709547519 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -891,14 +716,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709549567 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709549567 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -910,14 +728,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709550591 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709550591 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -929,14 +740,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709551103 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709551103 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -948,14 +752,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709551359 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709551359 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -967,14 +764,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709551487 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709551487 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -986,14 +776,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709551551 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709551551 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -1005,14 +788,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709551583 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709551583 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -1024,14 +800,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709551599 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709551599 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -1043,14 +812,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709551607 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709551607 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -1062,14 +824,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709551611 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709551611 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -1081,14 +836,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709551613 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709551613 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -1100,14 +848,7 @@ (set-option :produce-models true) (set-logic QF_AUFBV ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ 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) ) ) ) ) ) ) ) ) (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709551612 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) ) ) ) ) ) ) ) ) (and (and (and (and (and (and (and (= false (bvule (bvadd (_ bv51630448 64) ?B1 ) (_ bv18446744073709551612 64) ) ) (= 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) ) ) ) (= false (bvult (bvadd (_ bv18446744073709532800 64) ?B1 ) (_ bv1 64) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -1125,9 +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 (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (bvult ?B2 (_ bv1 64) ) ) -(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) ) ) ) ) ) ) ) ) (= (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 ) ) ) ) )) ) +(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) ) ) ) ) (check-sat) (get-value ( (select unnamed (_ bv0 32) ) ) ) (get-value ( (select unnamed (_ bv1 32) ) ) ) @@ -1144,12 +883,7 @@ (set-logic QF_AUFBV ) (declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (bvult ?B2 (_ bv1 64) ) ) -(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) ) ) ) ) ) ) ) ) (= 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 ) ) ) ) ) )) ) +(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) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -1171,13 +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 (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (bvult ?B2 (_ bv1 64) ) ) -(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) ) ) ) ) ) ) ) ) (= (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 ) ) ) ) )) ) +(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) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -1211,8 +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 (bvult ?B1 (_ bv13 64) ) ) -(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) ) ) ) ) ) ) ) ) (= (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 ) ) ) ) )) ) +(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) ) ) ) ) (check-sat) (get-value ( (select unnamed (_ bv0 32) ) ) ) (get-value ( (select unnamed (_ bv1 32) ) ) ) @@ -1234,11 +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 (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (bvult ?B2 (_ bv1 64) ) ) -(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) ) ) ) ) ) ) ) ) (= (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 ) ) ) ) )) ) +(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) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) @@ -1272,10 +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 (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (bvult ?B2 (_ bv13 64) ) ) -(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) ) ) ) ) ) ) ) ) (= (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 ) ) ) ) )) ) +(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) ) ) ) ) (check-sat) (get-value ( (select unnamed (_ bv0 32) ) ) ) (get-value ( (select unnamed (_ bv1 32) ) ) ) @@ -1292,14 +1012,7 @@ (set-logic QF_AUFBV ) (declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) ) (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(assert (= false (bvult ?B1 (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31312 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv31760 64) ?B1 ) (_ bv13 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv111120 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B1 ) (_ bv1 64) ) ) ) -(assert (bvult ?B2 (_ bv1 64) ) ) -(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) ) ) ) ) ) ) ) ) (= (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 ) ) ) ) )) ) +(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) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) (get-value ( (select unnamed_1 (_ bv1 32) ) ) ) |