diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-15 15:31:48 -0600 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-15 13:31:48 -0800 |
commit | 55037e0bcef45c795f28ff3fcf6c1055af465c70 (patch) | |
tree | 397d89bd10e541e1206c5dafdb8cf731feb34730 /test/regress/regress1/uflia | |
parent | 52a39aca19b7238d08c3cebcfa46436a73194008 (diff) |
Refactor regressions (#1581)
Diffstat (limited to 'test/regress/regress1/uflia')
12 files changed, 2270 insertions, 0 deletions
diff --git a/test/regress/regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2 b/test/regress/regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2 new file mode 100644 index 000000000..ab8e5d1da --- /dev/null +++ b/test/regress/regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2 @@ -0,0 +1,104 @@ +(set-logic QF_UFLIA) +(declare-fun _base () Int) +(declare-fun _n () Int) +(assert (let ((.def_5 (<= 0 _n))) +.def_5 +)) +(declare-fun ___z2z___ (Int) Bool) +(declare-fun ___z3z___ (Int) Bool) +(declare-fun ___z4z___ (Int) Bool) +(declare-fun ___z5z___ (Int) Bool) +(declare-fun ___z6z___ (Int) Bool) +(declare-fun ___z7z___ (Int) Bool) +(declare-fun ___z8z___ (Int) Bool) +(declare-fun ___z9z___ (Int) Bool) +(declare-fun ___z10z___ (Int) Bool) +(declare-fun ___z11z___ (Int) Bool) +(declare-fun ___z12z___ (Int) Bool) +(declare-fun ___z13z___ (Int) Bool) +(declare-fun ___z14z___ (Int) Int) +(declare-fun ___z15z___ (Int) Bool) +(declare-fun ___z16z___ (Int) Int) +(declare-fun ___z17z___ (Int) Int) +(declare-fun ___z18z___ (Int) Int) +(declare-fun ___z19z___ (Int) Int) +(declare-fun ___z20z___ (Int) Int) +(declare-fun ___z22z___ (Int) Bool) +(declare-fun ___z23z___ (Int) Bool) +(declare-fun ___z24z___ (Int) Bool) +(declare-fun ___z25z___ (Int) Bool) +(declare-fun ___z26z___ (Int) Bool) +(declare-fun ___z27z___ (Int) Bool) +(declare-fun ___z28z___ (Int) Bool) +(declare-fun ___z29z___ (Int) Bool) +(declare-fun ___z30z___ (Int) Bool) +(declare-fun ___z31z___ (Int) Bool) +(declare-fun ___z32z___ (Int) Bool) +(declare-fun ___z33z___ (Int) Bool) +(declare-fun ___z34z___ (Int) Bool) +(declare-fun ___z35z___ (Int) Int) +(declare-fun ___z36z___ (Int) Bool) +(declare-fun ___z37z___ (Int) Int) + + +(assert (let ((.def_1132 (___z29z___ (- 1)))) +(let ((.def_1126 (___z20z___ (- 2)))) +(let ((.def_1127 (<= 1 .def_1126))) +(let ((.def_1124 (___z19z___ (- 2)))) +(let ((.def_1125 (= .def_1124 0))) +(let ((.def_1128 (and .def_1125 .def_1127))) +(let ((.def_1106 (___z17z___ (- 2)))) +(let ((.def_1107 (= .def_1106 0))) +(let ((.def_1129 (and .def_1107 .def_1128))) +(let ((.def_1122 (___z16z___ (- 2)))) +(let ((.def_1123 (= .def_1122 0))) +(let ((.def_1130 (and .def_1123 .def_1129))) +(let ((.def_1108 (___z18z___ (- 2)))) +(let ((.def_1114 (= .def_1108 0))) +(let ((.def_1131 (and .def_1114 .def_1130))) +(let ((.def_1133 (= .def_1131 .def_1132))) +.def_1133 +))))))))))))))))) +(push 1) +(check-sat) +(pop 1) +(assert (let ((.def_2016 (___z16z___ (- 3)))) +(let ((.def_2188 (+ (- 1) .def_2016))) +(let ((.def_2048 (___z34z___ (- 2)))) +(let ((.def_2189 (ite .def_2048 .def_2188 .def_2016))) +(let ((.def_2057 (___z13z___ (- 2)))) +(let ((.def_2190 (ite .def_2057 .def_2189 .def_2016))) +(let ((.def_2036 (___z30z___ (- 2)))) +(let ((.def_2191 (ite .def_2036 0 .def_2016))) +(let ((.def_2064 (___z9z___ (- 2)))) +(let ((.def_2192 (ite .def_2064 .def_2191 .def_2190))) +(let ((.def_2193 (___z25z___ (- 2)))) +(let ((.def_2194 (ite .def_2193 .def_2188 .def_2016))) +(let ((.def_2074 (___z4z___ (- 2)))) +(let ((.def_2195 (ite .def_2074 .def_2194 .def_2192))) +(let ((.def_2196 (___z24z___ (- 2)))) +(let ((.def_2197 (ite .def_2196 0 .def_2016))) +(let ((.def_2076 (___z3z___ (- 2)))) +(let ((.def_2198 (ite .def_2076 .def_2197 .def_2195))) +(let ((.def_2199 (+ 1 .def_2016))) +(let ((.def_2200 (___z23z___ (- 2)))) +(let ((.def_2201 (ite .def_2200 .def_2199 .def_2016))) +(let ((.def_2078 (___z2z___ (- 2)))) +(let ((.def_2202 (ite .def_2078 .def_2201 .def_2198))) +(let ((.def_2052 (= _base (- 2)))) +(let ((.def_2203 (ite .def_2052 0 .def_2202))) +(let ((.def_1122 (___z16z___ (- 2)))) +(let ((.def_2204 (= .def_1122 .def_2203))) +.def_2204 +)))))))))))))))))))))))))))) + +(push 1) +(assert (let ((.def_2052 (= _base (- 2)))) +(let ((.def_2278 (not .def_2052))) +(let ((.def_997 (___z15z___ 0))) +(let ((.def_2290 (or .def_997 .def_2278))) +(let ((.def_2291 (not .def_2290))) +.def_2291 +)))))) +(check-sat) +(pop 1) diff --git a/test/regress/regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2.expect b/test/regress/regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2.expect new file mode 100644 index 000000000..9403b1a25 --- /dev/null +++ b/test/regress/regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2.expect @@ -0,0 +1,3 @@ +% COMMAND-LINE: --incremental +% EXPECT: sat +% EXPECT: sat diff --git a/test/regress/regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2 b/test/regress/regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2 new file mode 100644 index 000000000..0274e4390 --- /dev/null +++ b/test/regress/regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2 @@ -0,0 +1,29 @@ +(set-logic QF_UFLIA) +(set-info :smt-lib-version 2.0) +(declare-fun _base () Int) +(declare-fun _n () Int) +(declare-fun ___z3z___ (Int) Bool) +(declare-fun ___z4z___ (Int) Bool) +(declare-fun ___z6z___ (Int) Bool) +(declare-fun ___z8z___ (Int) Bool) +(declare-fun ___z9z___ (Int) Bool) +(declare-fun ___z11z___ (Int) Bool) +(declare-fun ___z12z___ (Int) Int) +(declare-fun ___z14z___ (Int) Int) +(declare-fun ___z15z___ (Int) Int) +(declare-fun ___z16z___ (Int) Bool) +(declare-fun ___z19z___ (Int) Bool) +(declare-fun ___z20z___ (Int) Bool) +(declare-fun ___z22z___ (Int) Bool) +(declare-fun ___z24z___ (Int) Bool) +(declare-fun ___z25z___ (Int) Bool) +(assert (= (and (<= 1 (+ (___z14z___ (- 1)) (___z15z___ (- 1)))) (<= 1 (___z12z___ (- 1)))) (___z20z___ 0))) +(assert (= (or (not (___z16z___ 0)) (<= 0 (___z15z___ 0))) (___z11z___ 0))) +(assert (let ((?v_2 (___z14z___ (- 1))) (?v_0 (___z15z___ (- 1)))) (let ((?v_1 (+ 2 ?v_0))) (= (___z15z___ 0) (ite (= _base 0) 0 (ite (___z3z___ 0) (ite (___z19z___ 0) ?v_1 ?v_0) (ite (___z4z___ 0) (ite (___z20z___ 0) (+ 1 (+ ?v_2 (+ (- 1) ?v_0))) ?v_0) (ite (___z6z___ 0) (ite (___z22z___ 0) 0 ?v_0) (ite (___z8z___ 0) (ite (___z24z___ 0) ?v_1 ?v_0) (ite (___z9z___ 0) (ite (___z25z___ 0) (+ 1 (+ ?v_2 ?v_0)) ?v_0) ?v_0)))))))))) +(assert (= (and (<= 1 (+ (___z14z___ (- 1)) (___z15z___ (- 1)))) (<= 1 (___z12z___ (- 1)))) (___z25z___ 0))) +(assert (= (or (not (___z16z___ (- 1))) (<= 0 (___z15z___ (- 1)))) (___z11z___ (- 1)))) +(assert (let ((?v_2 (___z14z___ (- 2))) (?v_0 (___z15z___ (- 2)))) (let ((?v_1 (+ 2 ?v_0))) (= (___z15z___ (- 1)) (ite (= _base (- 1)) 0 (ite (___z3z___ (- 1)) (ite (___z19z___ (- 1)) ?v_1 ?v_0) (ite (___z4z___ (- 1)) (ite (___z20z___ (- 1)) (+ 1 (+ ?v_2 (+ (- 1) ?v_0))) ?v_0) (ite (___z6z___ (- 1)) (ite (___z22z___ (- 1)) 0 ?v_0) (ite (___z8z___ (- 1)) (ite (___z24z___ (- 1)) ?v_1 ?v_0) (ite (___z9z___ (- 1)) (ite (___z25z___ (- 1)) (+ 1 (+ ?v_2 ?v_0)) ?v_0) ?v_0)))))))))) +(push 1) +(assert (not (or (not (= _base (- 1))) (and (___z11z___ 0) (___z11z___ (- 1)))))) +(pop 1) +(check-sat) diff --git a/test/regress/regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2.expect b/test/regress/regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2.expect new file mode 100644 index 000000000..85c180889 --- /dev/null +++ b/test/regress/regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2.expect @@ -0,0 +1,2 @@ +% COMMAND-LINE: --incremental +% EXPECT: sat diff --git a/test/regress/regress1/uflia/FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2 b/test/regress/regress1/uflia/FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2 new file mode 100644 index 000000000..248a056d3 --- /dev/null +++ b/test/regress/regress1/uflia/FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2 @@ -0,0 +1,72 @@ +(set-logic QF_UFLIA) +(set-info :smt-lib-version 2.0) +(set-info :status sat) +(declare-fun _base () Int) +(declare-fun _n () Int) +(assert (<= 0 _n)) +(declare-fun ___z2z___ (Int) Bool) +(declare-fun ___z3z___ (Int) Bool) +(declare-fun ___z4z___ (Int) Bool) +(declare-fun ___z5z___ (Int) Bool) +(declare-fun ___z6z___ (Int) Bool) +(declare-fun ___z7z___ (Int) Bool) +(declare-fun ___z8z___ (Int) Bool) +(declare-fun ___z9z___ (Int) Bool) +(declare-fun ___z10z___ (Int) Int) +(declare-fun ___z11z___ (Int) Bool) +(declare-fun ___z12z___ (Int) Int) +(declare-fun ___z13z___ (Int) Int) +(declare-fun ___z14z___ (Int) Int) +(declare-fun ___z15z___ (Int) Int) +(declare-fun ___z16z___ (Int) Bool) +(declare-fun ___z17z___ (Int) Bool) +(declare-fun ___z18z___ (Int) Bool) +(declare-fun ___z19z___ (Int) Bool) +(declare-fun ___z20z___ (Int) Bool) +(declare-fun ___z21z___ (Int) Bool) +(declare-fun ___z22z___ (Int) Bool) +(declare-fun ___z23z___ (Int) Bool) +(declare-fun ___z24z___ (Int) Bool) +(declare-fun ___z25z___ (Int) Int) +(declare-fun ___z26z___ (Int) Bool) +(assert (= (<= 1 (___z14z___ (- 1))) (___z20z___ 0))) +(assert (= (or (not (___z16z___ 0)) (or (= (+ (___z14z___ (- 1)) (+ (___z15z___ (- 1)) (+ (___z13z___ (- 1)) (+ (___z12z___ (- 1)) (+ (* (- 1) (___z15z___ 0)) (+ (* (- 1) (___z14z___ 0)) (+ (* (- 1) (___z13z___ 0)) (* (- 1) (___z12z___ 0))))))))) 0) (= _base 0))) (___z11z___ 0))) +(assert (= (= (___z15z___ (- 1)) 1) (___z21z___ 0))) +(assert (let ((?v_0 (___z12z___ (- 1)))) (let ((?v_1 (+ (- 1) ?v_0))) (= (___z12z___ 0) (ite (= _base 0) (___z25z___ 0) (ite (___z2z___ 0) (ite (___z17z___ 0) ?v_1 ?v_0) (ite (___z3z___ 0) (ite (___z18z___ 0) ?v_1 ?v_0) (ite (___z4z___ 0) (ite (___z19z___ 0) ?v_1 ?v_0) (ite (___z7z___ 0) (ite (___z22z___ 0) ?v_1 ?v_0) (ite (___z8z___ 0) (ite (___z23z___ 0) ?v_1 ?v_0) (ite (___z9z___ 0) (ite (___z24z___ 0) ?v_1 ?v_0) ?v_0))))))))))) +(assert (= (___z22z___ 0) (and (= (___z14z___ (- 1)) 0) (and (= (___z15z___ (- 1)) 0) (and (= (___z13z___ (- 1)) 0) (<= 1 (___z12z___ (- 1)))))))) +(assert (let ((?v_0 (___z13z___ (- 1)))) (let ((?v_1 (+ (- 1) ?v_0))) (= (___z13z___ 0) (ite (= _base 0) 0 (ite (___z3z___ 0) (ite (___z18z___ 0) ?v_1 ?v_0) (ite (___z5z___ 0) (ite (___z20z___ 0) (+ 1 ?v_0) ?v_0) (ite (___z7z___ 0) (ite (___z22z___ 0) 1 ?v_0) (ite (___z8z___ 0) (ite (___z23z___ 0) ?v_1 ?v_0) ?v_0))))))))) +(assert (= (___z23z___ 0) (and (<= 1 (___z12z___ (- 1))) (<= 1 (___z13z___ (- 1)))))) +(assert (let ((?v_0 (___z14z___ (- 1)))) (let ((?v_1 (+ 1 ?v_0))) (= (___z14z___ 0) (ite (= _base 0) 0 (ite (___z2z___ 0) (ite (___z17z___ 0) ?v_1 ?v_0) (ite (___z4z___ 0) (ite (___z19z___ 0) 0 ?v_0) (ite (___z5z___ 0) (ite (___z20z___ 0) (+ (- 1) ?v_0) ?v_0) (ite (___z6z___ 0) (ite (___z21z___ 0) ?v_1 ?v_0) (ite (___z9z___ 0) (ite (___z24z___ 0) 0 ?v_0) ?v_0)))))))))) +(assert (= (___z24z___ 0) (and (<= 1 (___z12z___ (- 1))) (<= 1 (+ (___z14z___ (- 1)) (___z15z___ (- 1))))))) +(assert (let ((?v_2 (___z14z___ (- 1))) (?v_0 (___z15z___ (- 1)))) (let ((?v_1 (+ 2 ?v_0))) (= (___z15z___ 0) (ite (= _base 0) 0 (ite (___z3z___ 0) (ite (___z18z___ 0) ?v_1 ?v_0) (ite (___z4z___ 0) (ite (___z19z___ 0) (+ 1 (+ ?v_2 (+ (- 1) ?v_0))) ?v_0) (ite (___z6z___ 0) (ite (___z21z___ 0) 0 ?v_0) (ite (___z8z___ 0) (ite (___z23z___ 0) ?v_1 ?v_0) (ite (___z9z___ 0) (ite (___z24z___ 0) (+ 1 (+ ?v_2 ?v_0)) ?v_0) ?v_0)))))))))) +(assert (= (___z25z___ 0) (ite (= _base 0) (___z10z___ 0) (___z25z___ (- 1))))) +(assert (let ((?v_0 (= _base 0)) (?v_1 (___z26z___ 0))) (= (___z16z___ 0) (and (or (not ?v_0) ?v_1) (or ?v_0 (or ?v_1 (___z16z___ (- 1)))))))) +(assert (let ((?v_2 (___z9z___ 0)) (?v_0 (___z8z___ 0)) (?v_5 (___z7z___ 0)) (?v_14 (___z4z___ 0)) (?v_17 (___z3z___ 0)) (?v_19 (___z2z___ 0)) (?v_11 (___z5z___ 0)) (?v_8 (___z6z___ 0))) (let ((?v_3 (not ?v_2)) (?v_18 (not ?v_19)) (?v_20 (not ?v_17))) (let ((?v_15 (and ?v_20 ?v_18)) (?v_16 (not ?v_14))) (let ((?v_12 (and ?v_16 ?v_15)) (?v_13 (not ?v_11))) (let ((?v_9 (and ?v_13 ?v_12)) (?v_10 (not ?v_8))) (let ((?v_6 (and ?v_10 ?v_9)) (?v_7 (not ?v_5))) (let ((?v_1 (and ?v_7 ?v_6)) (?v_4 (not ?v_0))) (let ((?v_21 (and ?v_4 ?v_1))) (= (___z26z___ 0) (and (<= 0 (___z10z___ 0)) (or (and ?v_2 ?v_21) (or (and (and ?v_0 ?v_1) ?v_3) (or (and ?v_3 (and ?v_4 (and ?v_5 ?v_6))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_8 ?v_9)))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_11 ?v_12))))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_13 (and ?v_14 ?v_15)))))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_13 (and ?v_16 (and ?v_17 ?v_18))))))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_13 (and ?v_16 (and ?v_19 ?v_20))))))) (and ?v_21 ?v_3)))))))))))))))))))) +(assert (= (___z17z___ 0) (and (= (___z14z___ (- 1)) 0) (and (= (___z15z___ (- 1)) 0) (and (= (___z13z___ (- 1)) 0) (<= 1 (___z12z___ (- 1)))))))) +(assert (= (___z18z___ 0) (and (<= 1 (___z12z___ (- 1))) (<= 1 (___z13z___ (- 1)))))) +(assert (= (___z19z___ 0) (and (<= 1 (___z12z___ (- 1))) (<= 1 (+ (___z14z___ (- 1)) (___z15z___ (- 1))))))) +(assert (= (<= 1 (___z14z___ (- 2))) (___z20z___ (- 1)))) +(assert (= (or (not (___z16z___ (- 1))) (or (= (+ (___z14z___ (- 1)) (+ (___z15z___ (- 1)) (+ (___z13z___ (- 1)) (+ (___z12z___ (- 1)) (+ (* (- 1) (___z14z___ (- 2))) (+ (* (- 1) (___z15z___ (- 2))) (+ (* (- 1) (___z13z___ (- 2))) (* (- 1) (___z12z___ (- 2)))))))))) 0) (= _base (- 1)))) (___z11z___ (- 1)))) +(assert (= (= (___z15z___ (- 2)) 1) (___z21z___ (- 1)))) +(assert (let ((?v_0 (___z12z___ (- 2)))) (let ((?v_1 (+ (- 1) ?v_0))) (= (___z12z___ (- 1)) (ite (= _base (- 1)) (___z25z___ (- 1)) (ite (___z2z___ (- 1)) (ite (___z17z___ (- 1)) ?v_1 ?v_0) (ite (___z3z___ (- 1)) (ite (___z18z___ (- 1)) ?v_1 ?v_0) (ite (___z4z___ (- 1)) (ite (___z19z___ (- 1)) ?v_1 ?v_0) (ite (___z7z___ (- 1)) (ite (___z22z___ (- 1)) ?v_1 ?v_0) (ite (___z8z___ (- 1)) (ite (___z23z___ (- 1)) ?v_1 ?v_0) (ite (___z9z___ (- 1)) (ite (___z24z___ (- 1)) ?v_1 ?v_0) ?v_0))))))))))) +(assert (= (___z22z___ (- 1)) (and (= (___z14z___ (- 2)) 0) (and (= (___z15z___ (- 2)) 0) (and (= (___z13z___ (- 2)) 0) (<= 1 (___z12z___ (- 2)))))))) +(assert (let ((?v_0 (___z13z___ (- 2)))) (let ((?v_1 (+ (- 1) ?v_0))) (= (___z13z___ (- 1)) (ite (= _base (- 1)) 0 (ite (___z3z___ (- 1)) (ite (___z18z___ (- 1)) ?v_1 ?v_0) (ite (___z5z___ (- 1)) (ite (___z20z___ (- 1)) (+ 1 ?v_0) ?v_0) (ite (___z7z___ (- 1)) (ite (___z22z___ (- 1)) 1 ?v_0) (ite (___z8z___ (- 1)) (ite (___z23z___ (- 1)) ?v_1 ?v_0) ?v_0))))))))) +(assert (= (___z23z___ (- 1)) (and (<= 1 (___z12z___ (- 2))) (<= 1 (___z13z___ (- 2)))))) +(assert (let ((?v_0 (___z14z___ (- 2)))) (let ((?v_1 (+ 1 ?v_0))) (= (___z14z___ (- 1)) (ite (= _base (- 1)) 0 (ite (___z2z___ (- 1)) (ite (___z17z___ (- 1)) ?v_1 ?v_0) (ite (___z4z___ (- 1)) (ite (___z19z___ (- 1)) 0 ?v_0) (ite (___z5z___ (- 1)) (ite (___z20z___ (- 1)) (+ (- 1) ?v_0) ?v_0) (ite (___z6z___ (- 1)) (ite (___z21z___ (- 1)) ?v_1 ?v_0) (ite (___z9z___ (- 1)) (ite (___z24z___ (- 1)) 0 ?v_0) ?v_0)))))))))) +(assert (= (___z24z___ (- 1)) (and (<= 1 (___z12z___ (- 2))) (<= 1 (+ (___z14z___ (- 2)) (___z15z___ (- 2))))))) +(assert (let ((?v_2 (___z14z___ (- 2))) (?v_0 (___z15z___ (- 2)))) (let ((?v_1 (+ 2 ?v_0))) (= (___z15z___ (- 1)) (ite (= _base (- 1)) 0 (ite (___z3z___ (- 1)) (ite (___z18z___ (- 1)) ?v_1 ?v_0) (ite (___z4z___ (- 1)) (ite (___z19z___ (- 1)) (+ 1 (+ ?v_2 (+ (- 1) ?v_0))) ?v_0) (ite (___z6z___ (- 1)) (ite (___z21z___ (- 1)) 0 ?v_0) (ite (___z8z___ (- 1)) (ite (___z23z___ (- 1)) ?v_1 ?v_0) (ite (___z9z___ (- 1)) (ite (___z24z___ (- 1)) (+ 1 (+ ?v_2 ?v_0)) ?v_0) ?v_0)))))))))) + +;(assert (= _base (- 1))) +(assert (= (___z25z___ (- 1)) (ite (= _base (- 1)) (___z10z___ (- 1)) (___z25z___ (- 2))))) +;(assert (= (___z25z___ (- 1)) (___z10z___ (- 1)))) +;(assert (= (___z25z___ (- 1)) (___z25z___ (- 2)))) + +(assert (let ((?v_0 (= _base (- 1))) (?v_1 (___z26z___ (- 1)))) (= (___z16z___ (- 1)) (and (or (not ?v_0) ?v_1) (or ?v_0 (or ?v_1 (___z16z___ (- 2)))))))) +(assert (let ((?v_19 (___z2z___ (- 1))) (?v_17 (___z3z___ (- 1))) (?v_14 (___z4z___ (- 1))) (?v_5 (___z7z___ (- 1))) (?v_0 (___z8z___ (- 1))) (?v_2 (___z9z___ (- 1))) (?v_11 (___z5z___ (- 1))) (?v_8 (___z6z___ (- 1)))) (let ((?v_4 (not ?v_0)) (?v_7 (not ?v_5)) (?v_10 (not ?v_8)) (?v_13 (not ?v_11)) (?v_16 (not ?v_14)) (?v_20 (not ?v_17)) (?v_18 (not ?v_19))) (let ((?v_15 (and ?v_20 ?v_18))) (let ((?v_12 (and ?v_16 ?v_15))) (let ((?v_9 (and ?v_13 ?v_12))) (let ((?v_6 (and ?v_10 ?v_9))) (let ((?v_1 (and ?v_7 ?v_6))) (let ((?v_21 (and ?v_4 ?v_1)) (?v_3 (not ?v_2))) (= (___z26z___ (- 1)) (and (<= 0 (___z10z___ (- 1))) (or (and ?v_2 ?v_21) (or (and (and ?v_0 ?v_1) ?v_3) (or (and ?v_3 (and ?v_4 (and ?v_5 ?v_6))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_8 ?v_9)))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_11 ?v_12))))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_13 (and ?v_14 ?v_15)))))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_13 (and ?v_16 (and ?v_17 ?v_18))))))) (or (and ?v_3 (and ?v_4 (and ?v_7 (and ?v_10 (and ?v_13 (and ?v_16 (and ?v_19 ?v_20))))))) (and ?v_21 ?v_3)))))))))))))))))))) +(assert (= (___z17z___ (- 1)) (and (= (___z14z___ (- 2)) 0) (and (= (___z15z___ (- 2)) 0) (and (= (___z13z___ (- 2)) 0) (<= 1 (___z12z___ (- 2)))))))) +(assert (= (___z18z___ (- 1)) (and (<= 1 (___z12z___ (- 2))) (<= 1 (___z13z___ (- 2)))))) +(assert (= (___z19z___ (- 1)) (and (<= 1 (___z12z___ (- 2))) (<= 1 (+ (___z14z___ (- 2)) (___z15z___ (- 2))))))) +(assert (not (or (not (= _base (- 1))) (and (___z11z___ 0) (___z11z___ (- 1)))))) +(assert true) +(check-sat) +(exit) diff --git a/test/regress/regress1/uflia/Makefile.am b/test/regress/regress1/uflia/Makefile.am new file mode 100644 index 000000000..c9a5ee372 --- /dev/null +++ b/test/regress/regress1/uflia/Makefile.am @@ -0,0 +1,41 @@ +# don't override a BINARY imported from a personal.mk +@mk_if@eq ($(BINARY),) +@mk_empty@BINARY = cvc4 +end@mk_if@ + +LOG_COMPILER = @srcdir@/../../run_regression +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) + +if AUTOMAKE_1_11 +# old-style (pre-automake 1.12) test harness +TESTS_ENVIRONMENT = \ + $(LOG_COMPILER) \ + $(AM_LOG_FLAGS) $(LOG_FLAGS) +endif + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" +TESTS = \ + FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2 \ + microwave21.ec.minimized.smt2 \ + simple_cyclic2.smt2 \ + DRAGON_11_e1_2450.ec.minimized.smt2 \ + FIREFLY_3_e2_2236_e7_3681.ec.core.smt2 \ + speed2_e8_449_e8_517.ec.smt2 \ + stalmark_e7_27_e7_31.ec.smt2 + + +EXTRA_DIST = $(TESTS) \ + DRAGON_11_e1_2450.ec.minimized.smt2.expect \ + FIREFLY_3_e2_2236_e7_3681.ec.core.smt2.expect \ + speed2_e8_449_e8_517.ec.smt2.expect \ + stalmark_e7_27_e7_31.ec.smt2.expect + +# synonyms for "check" in this directory +.PHONY: regress regress1 test +regress regress1 test: check + +# do nothing in this subdir +.PHONY: regress0 regress2 regress3 regress4 +regress0 regress2 regress3 regress4: diff --git a/test/regress/regress1/uflia/microwave21.ec.minimized.smt2 b/test/regress/regress1/uflia/microwave21.ec.minimized.smt2 new file mode 100644 index 000000000..b37db9a1e --- /dev/null +++ b/test/regress/regress1/uflia/microwave21.ec.minimized.smt2 @@ -0,0 +1,444 @@ +; initialize_defs +; PROPERTY DEFGEN +(set-logic QF_UFNIA) +(set-info :status unsat) +(declare-fun _base () Int) +(declare-fun _n () Int) +(assert (>= _n 0)) + +; maxdepth = 1 +(declare-fun ___z2z___ (Int) Bool) + ; KP_START ; INPUT,STATE(1,)/102 +(declare-fun ___z3z___ (Int) Bool) + ; KP_CLEAR ; INPUT,STATE(1,)/103 +(declare-fun ___z4z___ (Int) Bool) + ; KP_0 ; INPUT,STATE(1,)/104 +(declare-fun ___z5z___ (Int) Bool) + ; KP_1 ; INPUT,STATE(1,)/105 +(declare-fun ___z6z___ (Int) Bool) + ; KP_2 ; INPUT,STATE(1,)/106 +(declare-fun ___z7z___ (Int) Bool) + ; KP_3 ; INPUT,STATE(1,)/107 +(declare-fun ___z8z___ (Int) Bool) + ; KP_4 ; INPUT,STATE(1,)/108 +(declare-fun ___z9z___ (Int) Bool) + ; KP_5 ; INPUT,STATE(1,)/109 +(declare-fun ___z10z___ (Int) Bool) + ; KP_6 ; INPUT,STATE(1,)/110 +(declare-fun ___z11z___ (Int) Bool) + ; KP_7 ; INPUT,STATE(1,)/111 +(declare-fun ___z12z___ (Int) Bool) + ; KP_8 ; INPUT,STATE(1,)/112 +(declare-fun ___z13z___ (Int) Bool) + ; KP_9 ; INPUT,STATE(1,)/113 +(declare-fun ___z14z___ (Int) Bool) + ; DOOR_CLOSED ; INPUT/114 +(declare-fun ___z15z___ (Int) Bool) + ; OK ; OUTPUT/115 +(declare-fun ___z19z___ (Int) Bool) + ; V20_START_PRESSED ; LOCAL/119 +(declare-fun ___z20z___ (Int) Bool) + ; V21_CLEAR_PRESSED ; LOCAL/120 +(declare-fun ___z21z___ (Int) Int) + ; V25_STEPS_TO_COOK ; LOCAL,STATE(1,)/121 +(declare-fun ___z22z___ (Int) Bool) + ; V26_rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_clock ; LOCAL,STATE(1,)/122 +(declare-fun ___z23z___ (Int) Bool) + ; V37_rlt_condact_resetmicrowave_microwave_KEYPAD_PROCESSING_rlt_init_step ; LOCAL,STATE(1,)/123 +(declare-fun ___z24z___ (Int) Int) + ; V38_microwave_microwave_KEYPAD_PROCESSING_DISPLAY_LEFT_DIGIT_DIGIT_TO_DISPLAY ; LOCAL,STATE(1,)/124 +(declare-fun ___z25z___ (Int) Int) + ; V39_microwave_microwave_KEYPAD_PROCESSING_DISPLAY_MIDDLE_DIGIT_DIGIT_TO_DISPLAY ; LOCAL,STATE(1,)/125 +(declare-fun ___z26z___ (Int) Int) + ; V40_microwave_microwave_KEYPAD_PROCESSING_DISPLAY_RIGHT_DIGIT_DIGIT_TO_DISPLAY ; LOCAL,STATE(1,)/126 +(declare-fun ___z33z___ (Int) Int) + ; V47_chart_microwave_mode_logic_start ; LOCAL/133 +(declare-fun ___z34z___ (Int) Int) + ; V48_chart_microwave_mode_logic_clear_off ; LOCAL/134 +(declare-fun ___z35z___ (Int) Int) + ; V49_chart_microwave_mode_logic_door_closed ; LOCAL/135 +(declare-fun ___z36z___ (Int) Bool) + ; V51_rlt_eval_microwave_mode_logic_ON_rlt_fired_1 ; LOCAL/136 +(declare-fun ___z37z___ (Int) Int) + ; V52_rlt_eval_microwave_mode_logic_ON_rlt_state_1_states___root ; LOCAL/137 +(declare-fun ___z38z___ (Int) Int) + ; V53_rlt_eval_microwave_mode_logic_ON_rlt_state_2_states___root ; LOCAL/138 +(declare-fun ___z39z___ (Int) Bool) + ; V54_rlt_eval_microwave_mode_logic_ON_rlt_fired_2 ; LOCAL/139 +(declare-fun ___z40z___ (Int) Bool) + ; V55_rlt_eval_microwave_mode_logic_ON_rlt_complete_1 ; LOCAL/140 +(declare-fun ___z41z___ (Int) Int) + ; V56_rlt_eval_microwave_mode_logic_ON_rlt_state_3_states___root ; LOCAL/141 +(declare-fun ___z42z___ (Int) Int) + ; V57_rlt_eval_microwave_mode_logic_ON_rlt_state_3_outports_mode ; LOCAL/142 +(declare-fun ___z43z___ (Int) Int) + ; V58_rlt_eval_microwave_mode_logic_ON_rlt_state_4_states___root ; LOCAL/143 +(declare-fun ___z44z___ (Int) Int) + ; V59_rlt_eval_microwave_mode_logic_ON_rlt_state_4_outports_mode ; LOCAL/144 +(declare-fun ___z45z___ (Int) Bool) + ; V60_rlt_eval_microwave_mode_logic_ON_rlt_fired_4 ; LOCAL/145 +(declare-fun ___z46z___ (Int) Bool) + ; V61_rlt_eval_microwave_mode_logic_ON_rlt_complete_2 ; LOCAL/146 +(declare-fun ___z47z___ (Int) Int) + ; V62_rlt_eval_microwave_mode_logic_ON_rlt_state_6_states___root ; LOCAL/147 +(declare-fun ___z48z___ (Int) Int) + ; V63_rlt_eval_microwave_mode_logic_ON_rlt_state_6_outports_steps_remaining ; LOCAL/148 +(declare-fun ___z49z___ (Int) Int) + ; V64_rlt_eval_microwave_mode_logic_ON_rlt_state_7_states___root ; LOCAL/149 +(declare-fun ___z50z___ (Int) Bool) + ; V65_rlt_eval_microwave_mode_logic_ON_rlt_fired_5 ; LOCAL/150 +(declare-fun ___z51z___ (Int) Int) + ; V66_rlt_eval_microwave_mode_logic_ON_rlt_state_8_outports_mode ; LOCAL/151 +(declare-fun ___z52z___ (Int) Int) + ; V67_rlt_eval_microwave_mode_logic_ON_rlt_state_9_states___root ; LOCAL/152 +(declare-fun ___z53z___ (Int) Int) + ; V68_rlt_eval_microwave_mode_logic_ON_rlt_state_10_states___root ; LOCAL/153 +(declare-fun ___z54z___ (Int) Bool) + ; V69_rlt_eval_microwave_mode_logic_ON_rlt_fired_6 ; LOCAL/154 +(declare-fun ___z55z___ (Int) Int) + ; V70_rlt_eval_microwave_mode_logic_ON_rlt_state_11_states___root ; LOCAL/155 +(declare-fun ___z56z___ (Int) Int) + ; V71_rlt_eval_microwave_mode_logic_ON_rlt_state_11_outports_mode ; LOCAL/156 +(declare-fun ___z57z___ (Int) Int) + ; V72_rlt_enter_microwave_mode_logic_ON_rlt_state_1_states___root ; LOCAL/157 +(declare-fun ___z58z___ (Int) Bool) + ; V73_rlt_enter_microwave_mode_logic_ON_rlt_fired_0 ; LOCAL/158 +(declare-fun ___z59z___ (Int) Bool) + ; V74_rlt_enter_microwave_mode_logic_ON_rlt_fired_1 ; LOCAL/159 +(declare-fun ___z60z___ (Int) Int) + ; V75_rlt_enter_microwave_mode_logic_ON_rlt_state_2_states___root ; LOCAL/160 +(declare-fun ___z61z___ (Int) Int) + ; V76_rlt_enter_microwave_mode_logic_ON_rlt_state_2_outports_mode ; LOCAL/161 +(declare-fun ___z62z___ (Int) Bool) + ; V77_rlt_enter_microwave_mode_logic_ON_rlt_fired_2 ; LOCAL/162 +(declare-fun ___z63z___ (Int) Int) + ; V78_rlt_enter_microwave_mode_logic_ON_rlt_state_4_states___root ; LOCAL/163 +(declare-fun ___z64z___ (Int) Bool) + ; V79_rlt_eval_microwave_mode_logic_rlt_fired_0 ; LOCAL/164 +(declare-fun ___z65z___ (Int) Int) + ; V80_rlt_eval_microwave_mode_logic_rlt_state_1_outports_steps_remaining ; LOCAL/165 +(declare-fun ___z66z___ (Int) Bool) + ; V81_rlt_eval_microwave_mode_logic_rlt_fired_1 ; LOCAL/166 +(declare-fun ___z67z___ (Int) Int) + ; V82_rlt_eval_microwave_mode_logic_rlt_state_2_states___root ; LOCAL/167 +(declare-fun ___z68z___ (Int) Int) + ; V83_rlt_eval_microwave_mode_logic_rlt_state_3_states___root ; LOCAL/168 +(declare-fun ___z69z___ (Int) Int) + ; V84_rlt_eval_microwave_mode_logic_rlt_state_3_outports_mode ; LOCAL/169 +(declare-fun ___z70z___ (Int) Int) + ; V85_rlt_enter_microwave_mode_logic_rlt_state_2_states___root ; LOCAL/170 +(declare-fun ___z71z___ (Int) Bool) + ; V86_chart_microwave_mode_logic_rlt_evtInitStep ; LOCAL,STATE(1,)/171 +(declare-fun ___z72z___ (Int) Int) + ; V87_chart_microwave_mode_logic_begin_state_states___root ; LOCAL/172 +(declare-fun ___z73z___ (Int) Int) + ; V88_chart_microwave_mode_logic_begin_state_outports_mode ; LOCAL/173 +(declare-fun ___z74z___ (Int) Int) + ; V89_chart_microwave_mode_logic_begin_state_outports_steps_remaining ; LOCAL/174 +(declare-fun ___z75z___ (Int) Int) + ; V90_chart_microwave_mode_logic_final_state_states___root ; LOCAL,STATE(1,)/175 +(declare-fun ___z76z___ (Int) Int) + ; V92_chart_microwave_mode_logic_steps_remaining ; LOCAL,STATE(1,)/176 +(declare-fun ___z77z___ (Int) Int) + ; V93_microwave_microwave_TIME_ON_DISPLAY_SECONDS_TO_MINUTES__QUOTIENT ; LOCAL/177 +(declare-fun ___z80z___ (Int) Int) + ; V96_microwave_microwave_mode_logic_mode ; LOCAL,STATE(1,)/180 + + +; Generic definitions: +(define-fun DEF__172 ((_M Int)) Bool(= (___z72z___ _M) (ite (= _M _base) 0 (___z75z___ (- _M 1))))) +(define-fun DEF__173 ((_M Int)) Bool(= (___z73z___ _M) (ite (= _M _base) 0 (___z80z___ (- _M 1))))) +(define-fun DEF__174 ((_M Int)) Bool(= (___z74z___ _M) (ite (= _M _base) 0 (___z76z___ (- _M 1))))) +(define-fun DEF__175 ((_M Int)) Bool(= (___z75z___ _M) (ite (= (___z71z___ _M) true) (___z70z___ _M) (ite (= (and (not (___z66z___ _M)) (and (>= (___z68z___ _M) 1) (<= (___z68z___ _M) 3))) true) (ite (= (___z54z___ _M) true) (ite (= (not (= (___z55z___ _M) 3)) true) 3 (___z55z___ _M)) (___z55z___ _M)) (___z68z___ _M))))) +(define-fun DEF__133 ((_M Int)) Bool(= (___z33z___ _M) (ite (= (= (___z19z___ _M) false) true) 0 1))) +(define-fun DEF__176 ((_M Int)) Bool(= (___z76z___ _M) (ite (= (___z71z___ _M) true) (___z74z___ _M) (ite (= (and (not (___z66z___ _M)) (and (>= (___z68z___ _M) 1) (<= (___z68z___ _M) 3))) true) (ite (= (___z50z___ _M) true) (- (___z48z___ _M) 1) (___z48z___ _M)) (___z65z___ _M))))) +(define-fun DEF__134 ((_M Int)) Bool(= (___z34z___ _M) (ite (= (= (___z20z___ _M) false) true) 0 1))) +(define-fun DEF__177 ((_M Int)) Bool(= (___z77z___ _M) (div (div (___z76z___ _M) 1) 60))) +(define-fun DEF__135 ((_M Int)) Bool(= (___z35z___ _M) (ite (= (= (___z14z___ _M) false) true) 0 1))) +(define-fun DEF__136 ((_M Int)) Bool(= (___z36z___ _M) (and (and (= (___z68z___ _M) 2) (<= (___z65z___ _M) 0)) (= (___z68z___ _M) 2)))) +(define-fun DEF__180 ((_M Int)) Bool(= (___z80z___ _M) (ite (= (___z71z___ _M) true) (ite (= (not (= (___z72z___ _M) 4)) true) 1 (___z73z___ _M)) (ite (= (and (not (___z66z___ _M)) (and (>= (___z68z___ _M) 1) (<= (___z68z___ _M) 3))) true) (ite (= (___z54z___ _M) true) (ite (= (not (= (___z55z___ _M) 3)) true) 3 (___z56z___ _M)) (___z56z___ _M)) (___z69z___ _M))))) +(define-fun DEF__137 ((_M Int)) Bool(= (___z37z___ _M) (ite (= (___z36z___ _M) true) (ite (= (and (>= (___z68z___ _M) 1) (<= (___z68z___ _M) 3)) true) 0 (___z68z___ _M)) (___z68z___ _M)))) +(define-fun DEF__138 ((_M Int)) Bool(= (___z38z___ _M) (ite (= (___z36z___ _M) true) (ite (= (not (= (___z37z___ _M) 4)) true) 4 (___z37z___ _M)) (___z37z___ _M)))) +(define-fun DEF__139 ((_M Int)) Bool(= (___z39z___ _M) (and (= (___z38z___ _M) 3) (and (and (ite (= (not (= (___z33z___ _M) 0)) true) true false) (ite (= (not (= (___z35z___ _M) 0)) true) true false)) (not (___z36z___ _M)))))) +(define-fun DEF__140 ((_M Int)) Bool(= (___z40z___ _M) (or (___z39z___ _M) (___z36z___ _M)))) +(define-fun DEF__141 ((_M Int)) Bool(= (___z41z___ _M) (ite (= (___z39z___ _M) true) (ite (= (___z38z___ _M) 3) 1 (___z38z___ _M)) (___z38z___ _M)))) +(define-fun DEF__142 ((_M Int)) Bool(= (___z42z___ _M) (ite (= (___z36z___ _M) true) (ite (= (not (= (___z37z___ _M) 4)) true) 1 (___z69z___ _M)) (___z69z___ _M)))) +(define-fun DEF__143 ((_M Int)) Bool(= (___z43z___ _M) (ite (= (___z39z___ _M) true) (ite (= (not (= (___z41z___ _M) 2)) true) 2 (___z41z___ _M)) (___z41z___ _M)))) +(define-fun DEF__144 ((_M Int)) Bool(= (___z44z___ _M) (ite (= (___z39z___ _M) true) (ite (= (not (= (___z41z___ _M) 2)) true) 2 (___z42z___ _M)) (___z42z___ _M)))) +(define-fun DEF__145 ((_M Int)) Bool(= (___z45z___ _M) (and (and (= (___z43z___ _M) 3) (and (ite (= (not (= (___z34z___ _M) 0)) true) true false) (not (___z40z___ _M)))) (and (= (___z43z___ _M) 3) (not (___z40z___ _M)))))) +(define-fun DEF__146 ((_M Int)) Bool(= (___z46z___ _M) (or (___z45z___ _M) (___z40z___ _M)))) +(define-fun DEF__147 ((_M Int)) Bool(= (___z47z___ _M) (ite (= (___z45z___ _M) true) (ite (= (and (>= (___z43z___ _M) 1) (<= (___z43z___ _M) 3)) true) 0 (___z43z___ _M)) (___z43z___ _M)))) +(define-fun DEF__148 ((_M Int)) Bool(= (___z48z___ _M) (ite (= (___z45z___ _M) true) 0 (___z65z___ _M)))) +(define-fun DEF__149 ((_M Int)) Bool(= (___z49z___ _M) (ite (= (___z45z___ _M) true) (ite (= (not (= (___z47z___ _M) 4)) true) 4 (___z47z___ _M)) (___z47z___ _M)))) +(define-fun DEF__150 ((_M Int)) Bool(= (___z50z___ _M) (and (= (___z49z___ _M) 2) (and (> (___z48z___ _M) 0) (not (___z46z___ _M)))))) +(define-fun DEF__151 ((_M Int)) Bool(= (___z51z___ _M) (ite (= (___z45z___ _M) true) (ite (= (not (= (___z47z___ _M) 4)) true) 1 (___z44z___ _M)) (___z44z___ _M)))) +(define-fun DEF__152 ((_M Int)) Bool(= (___z52z___ _M) (ite (= (___z50z___ _M) true) (ite (= (___z49z___ _M) 2) 1 (___z49z___ _M)) (___z49z___ _M)))) +(define-fun DEF__153 ((_M Int)) Bool(= (___z53z___ _M) (ite (= (___z50z___ _M) true) (ite (= (not (= (___z52z___ _M) 2)) true) 2 (___z52z___ _M)) (___z52z___ _M)))) +(define-fun DEF__154 ((_M Int)) Bool(= (___z54z___ _M) (and (= (___z53z___ _M) 2) (and (or (ite (= (not (= (___z34z___ _M) 0)) true) true false) (not (ite (= (not (= (___z35z___ _M) 0)) true) true false))) (not (or (___z50z___ _M) (___z46z___ _M))))))) +(define-fun DEF__155 ((_M Int)) Bool(= (___z55z___ _M) (ite (= (___z54z___ _M) true) (ite (= (___z53z___ _M) 2) 1 (___z53z___ _M)) (___z53z___ _M)))) +(define-fun DEF__156 ((_M Int)) Bool(= (___z56z___ _M) (ite (= (___z50z___ _M) true) (ite (= (not (= (___z52z___ _M) 2)) true) 2 (___z51z___ _M)) (___z51z___ _M)))) +(define-fun DEF__157 ((_M Int)) Bool(= (___z57z___ _M) (ite (= (not (and (>= (___z67z___ _M) 1) (<= (___z67z___ _M) 3))) true) 1 (___z67z___ _M)))) +(define-fun DEF__115 ((_M Int)) Bool(= (___z15z___ _M) (ite (= _M _base) (or (not (and (___z22z___ _M) (not (___z3z___ _M)))) (or (not (or (or (or (or (or (or (or (or (or (___z5z___ _M) (___z6z___ _M)) (___z7z___ _M)) (___z8z___ _M)) (___z9z___ _M)) (___z10z___ _M)) (___z11z___ _M)) (___z12z___ _M)) (___z13z___ _M)) (___z4z___ _M))) (= (___z77z___ _M) (div (div (___z21z___ _M) 1) 60)))) (or (not (and (___z22z___ _M) (not (___z3z___ _M)))) (or (not (or (or (or (or (or (or (or (or (or (and (___z5z___ _M) (not (___z5z___ (- _M 1)))) (and (___z6z___ _M) (not (___z6z___ (- _M 1))))) (and (___z7z___ _M) (not (___z7z___ (- _M 1))))) (and (___z8z___ _M) (not (___z8z___ (- _M 1))))) (and (___z9z___ _M) (not (___z9z___ (- _M 1))))) (and (___z10z___ _M) (not (___z10z___ (- _M 1))))) (and (___z11z___ _M) (not (___z11z___ (- _M 1))))) (and (___z12z___ _M) (not (___z12z___ (- _M 1))))) (and (___z13z___ _M) (not (___z13z___ (- _M 1))))) (and (___z4z___ _M) (not (___z4z___ (- _M 1)))))) (= (___z77z___ _M) (div (div (___z21z___ _M) 1) 60))))))) +(define-fun DEF__158 ((_M Int)) Bool(= (___z58z___ _M) (and (not (and (>= (___z67z___ _M) 1) (<= (___z67z___ _M) 3))) (and (>= (___z57z___ _M) 1) (<= (___z57z___ _M) 3))))) +(define-fun DEF__159 ((_M Int)) Bool(= (___z59z___ _M) (and (___z58z___ _M) (and (and (>= (___z57z___ _M) 1) (<= (___z57z___ _M) 3)) (ite (= (not (= (___z35z___ _M) 0)) true) true false))))) +(define-fun DEF__160 ((_M Int)) Bool(= (___z60z___ _M) (ite (= (___z59z___ _M) true) (ite (= (not (= (___z57z___ _M) 2)) true) 2 (___z57z___ _M)) (___z57z___ _M)))) +(define-fun DEF__161 ((_M Int)) Bool(= (___z61z___ _M) (ite (= (___z59z___ _M) true) (ite (= (not (= (___z57z___ _M) 2)) true) 2 (___z73z___ _M)) (___z73z___ _M)))) +(define-fun DEF__119 ((_M Int)) Bool(= (___z19z___ _M) (ite (= _M _base) (___z2z___ _M) (and (___z2z___ _M) (not (___z2z___ (- _M 1))))))) +(define-fun DEF__162 ((_M Int)) Bool(= (___z62z___ _M) (and (___z58z___ _M) (and (and (>= (___z60z___ _M) 1) (<= (___z60z___ _M) 3)) (not (___z59z___ _M)))))) +(define-fun DEF__120 ((_M Int)) Bool(= (___z20z___ _M) (ite (= _M _base) (___z3z___ _M) (and (___z3z___ _M) (not (___z3z___ (- _M 1))))))) +(define-fun DEF__163 ((_M Int)) Bool(= (___z63z___ _M) (ite (= (___z62z___ _M) true) (ite (= (not (= (___z60z___ _M) 3)) true) 3 (___z60z___ _M)) (___z60z___ _M)))) +(define-fun DEF__121 ((_M Int)) Bool(= (___z21z___ _M) (ite (= _M _base) (ite (= (and (___z23z___ _M) (not (___z22z___ _M))) true) 0 (* (+ (+ (* (___z26z___ _M) 1) (* (___z25z___ _M) 10)) (* (___z24z___ _M) 60)) 1)) (ite (= (and (___z23z___ _M) (not (___z22z___ _M))) true) 0 (ite (= (___z22z___ _M) true) (* (+ (+ (* (___z26z___ _M) 1) (* (___z25z___ _M) 10)) (* (___z24z___ _M) 60)) 1) (___z21z___ (- _M 1))))))) +(define-fun DEF__164 ((_M Int)) Bool(= (___z64z___ _M) (= (___z72z___ _M) 4))) +(define-fun DEF__122 ((_M Int)) Bool(= (___z22z___ _M) (ite (= _M _base) true (ite (= 1 (___z80z___ (- _M 1))) true false)))) +(define-fun DEF__165 ((_M Int)) Bool(= (___z65z___ _M) (ite (= (___z64z___ _M) true) (___z21z___ _M) (___z74z___ _M)))) +(define-fun DEF__123 ((_M Int)) Bool(= (___z23z___ _M) (ite (= _M _base) true (ite (= (not (___z22z___ _M)) true) true (ite (= (___z22z___ (- _M 1)) true) false (___z23z___ (- _M 1))))))) +(define-fun DEF__166 ((_M Int)) Bool(= (___z66z___ _M) (and (___z64z___ _M) (and (= (___z72z___ _M) 4) (and (ite (= (not (= (___z33z___ _M) 0)) true) true false) (ite (= (not (= (ite (= (= (> (___z21z___ _M) 0) false) true) 0 1) 0)) true) true false)))))) +(define-fun DEF__124 ((_M Int)) Bool(= (___z24z___ _M) (ite (= _M _base) 0 (ite (= (___z22z___ _M) true) (ite (= (___z23z___ _M) true) 0 (ite (= (___z3z___ _M) true) 0 (ite (= (ite (<= (ite (= (and (___z4z___ _M) (not (___z4z___ (- _M 1)))) true) 0 (ite (= (and (___z5z___ _M) (not (___z5z___ (- _M 1)))) true) 1 (ite (= (and (___z6z___ _M) (not (___z6z___ (- _M 1)))) true) 2 (ite (= (and (___z7z___ _M) (not (___z7z___ (- _M 1)))) true) 3 (ite (= (and (___z8z___ _M) (not (___z8z___ (- _M 1)))) true) 4 (ite (= (and (___z9z___ _M) (not (___z9z___ (- _M 1)))) true) 5 (ite (= (and (___z10z___ _M) (not (___z10z___ (- _M 1)))) true) 6 (ite (= (and (___z11z___ _M) (not (___z11z___ (- _M 1)))) true) 7 (ite (= (and (___z12z___ _M) (not (___z12z___ (- _M 1)))) true) 8 (ite (= (and (___z13z___ _M) (not (___z13z___ (- _M 1)))) true) 9 10)))))))))) 9) true false) true) (___z25z___ (- _M 1)) (___z24z___ (- _M 1))))) (___z24z___ (- _M 1)))))) +(define-fun DEF__167 ((_M Int)) Bool(= (___z67z___ _M) (ite (= (___z66z___ _M) true) (ite (= (___z72z___ _M) 4) 0 (___z72z___ _M)) (___z72z___ _M)))) +(define-fun DEF__125 ((_M Int)) Bool(= (___z25z___ _M) (ite (= _M _base) 0 (ite (= (___z22z___ _M) true) (ite (= (___z23z___ _M) true) 0 (ite (= (___z3z___ _M) true) 0 (ite (= (ite (<= (ite (= (and (___z4z___ _M) (not (___z4z___ (- _M 1)))) true) 0 (ite (= (and (___z5z___ _M) (not (___z5z___ (- _M 1)))) true) 1 (ite (= (and (___z6z___ _M) (not (___z6z___ (- _M 1)))) true) 2 (ite (= (and (___z7z___ _M) (not (___z7z___ (- _M 1)))) true) 3 (ite (= (and (___z8z___ _M) (not (___z8z___ (- _M 1)))) true) 4 (ite (= (and (___z9z___ _M) (not (___z9z___ (- _M 1)))) true) 5 (ite (= (and (___z10z___ _M) (not (___z10z___ (- _M 1)))) true) 6 (ite (= (and (___z11z___ _M) (not (___z11z___ (- _M 1)))) true) 7 (ite (= (and (___z12z___ _M) (not (___z12z___ (- _M 1)))) true) 8 (ite (= (and (___z13z___ _M) (not (___z13z___ (- _M 1)))) true) 9 10)))))))))) 9) true false) true) (___z26z___ (- _M 1)) (___z25z___ (- _M 1))))) (___z25z___ (- _M 1)))))) +(define-fun DEF__168 ((_M Int)) Bool(= (___z68z___ _M) (ite (= (___z66z___ _M) true) (___z63z___ _M) (___z67z___ _M)))) +(define-fun DEF__126 ((_M Int)) Bool(= (___z26z___ _M) (ite (= _M _base) (ite (= (___z3z___ _M) true) 0 (ite (= (ite (<= (ite (= (___z4z___ _M) true) 0 (ite (= (___z5z___ _M) true) 1 (ite (= (___z6z___ _M) true) 2 (ite (= (___z7z___ _M) true) 3 (ite (= (___z8z___ _M) true) 4 (ite (= (___z9z___ _M) true) 5 (ite (= (___z10z___ _M) true) 6 (ite (= (___z11z___ _M) true) 7 (ite (= (___z12z___ _M) true) 8 (ite (= (___z13z___ _M) true) 9 10)))))))))) 9) true false) true) (ite (= (___z4z___ _M) true) 0 (ite (= (___z5z___ _M) true) 1 (ite (= (___z6z___ _M) true) 2 (ite (= (___z7z___ _M) true) 3 (ite (= (___z8z___ _M) true) 4 (ite (= (___z9z___ _M) true) 5 (ite (= (___z10z___ _M) true) 6 (ite (= (___z11z___ _M) true) 7 (ite (= (___z12z___ _M) true) 8 (ite (= (___z13z___ _M) true) 9 10)))))))))) 0)) (ite (= (___z22z___ _M) true) (ite (= (___z23z___ _M) true) (ite (= (___z3z___ _M) true) 0 (ite (= (ite (<= (ite (= (___z4z___ _M) true) 0 (ite (= (___z5z___ _M) true) 1 (ite (= (___z6z___ _M) true) 2 (ite (= (___z7z___ _M) true) 3 (ite (= (___z8z___ _M) true) 4 (ite (= (___z9z___ _M) true) 5 (ite (= (___z10z___ _M) true) 6 (ite (= (___z11z___ _M) true) 7 (ite (= (___z12z___ _M) true) 8 (ite (= (___z13z___ _M) true) 9 10)))))))))) 9) true false) true) (ite (= (___z4z___ _M) true) 0 (ite (= (___z5z___ _M) true) 1 (ite (= (___z6z___ _M) true) 2 (ite (= (___z7z___ _M) true) 3 (ite (= (___z8z___ _M) true) 4 (ite (= (___z9z___ _M) true) 5 (ite (= (___z10z___ _M) true) 6 (ite (= (___z11z___ _M) true) 7 (ite (= (___z12z___ _M) true) 8 (ite (= (___z13z___ _M) true) 9 10)))))))))) 0)) (ite (= (___z3z___ _M) true) 0 (ite (= (ite (<= (ite (= (and (___z4z___ _M) (not (___z4z___ (- _M 1)))) true) 0 (ite (= (and (___z5z___ _M) (not (___z5z___ (- _M 1)))) true) 1 (ite (= (and (___z6z___ _M) (not (___z6z___ (- _M 1)))) true) 2 (ite (= (and (___z7z___ _M) (not (___z7z___ (- _M 1)))) true) 3 (ite (= (and (___z8z___ _M) (not (___z8z___ (- _M 1)))) true) 4 (ite (= (and (___z9z___ _M) (not (___z9z___ (- _M 1)))) true) 5 (ite (= (and (___z10z___ _M) (not (___z10z___ (- _M 1)))) true) 6 (ite (= (and (___z11z___ _M) (not (___z11z___ (- _M 1)))) true) 7 (ite (= (and (___z12z___ _M) (not (___z12z___ (- _M 1)))) true) 8 (ite (= (and (___z13z___ _M) (not (___z13z___ (- _M 1)))) true) 9 10)))))))))) 9) true false) true) (ite (= (and (___z4z___ _M) (not (___z4z___ (- _M 1)))) true) 0 (ite (= (and (___z5z___ _M) (not (___z5z___ (- _M 1)))) true) 1 (ite (= (and (___z6z___ _M) (not (___z6z___ (- _M 1)))) true) 2 (ite (= (and (___z7z___ _M) (not (___z7z___ (- _M 1)))) true) 3 (ite (= (and (___z8z___ _M) (not (___z8z___ (- _M 1)))) true) 4 (ite (= (and (___z9z___ _M) (not (___z9z___ (- _M 1)))) true) 5 (ite (= (and (___z10z___ _M) (not (___z10z___ (- _M 1)))) true) 6 (ite (= (and (___z11z___ _M) (not (___z11z___ (- _M 1)))) true) 7 (ite (= (and (___z12z___ _M) (not (___z12z___ (- _M 1)))) true) 8 (ite (= (and (___z13z___ _M) (not (___z13z___ (- _M 1)))) true) 9 10)))))))))) (___z26z___ (- _M 1))))) (___z26z___ (- _M 1)))))) +(define-fun DEF__169 ((_M Int)) Bool(= (___z69z___ _M) (ite (= (___z66z___ _M) true) (ite (= (___z62z___ _M) true) (ite (= (not (= (___z60z___ _M) 3)) true) 3 (___z61z___ _M)) (___z61z___ _M)) (___z73z___ _M)))) +(define-fun DEF__170 ((_M Int)) Bool(= (___z70z___ _M) (ite (= (not (= (___z72z___ _M) 4)) true) 4 (___z72z___ _M)))) +(define-fun DEF__171 ((_M Int)) Bool(= (___z71z___ _M) (ite (= _M _base) true (ite (= true true) false (___z71z___ (- _M 1)))))) +; Transition: +(define-fun trans ((_M Int)) Bool (and (DEF__171 _M) (DEF__170 _M) (DEF__169 _M) (DEF__126 _M) (DEF__168 _M) (DEF__125 _M) (DEF__167 _M) (DEF__124 _M) (DEF__166 _M) (DEF__123 _M) (DEF__165 _M) (DEF__122 _M) (DEF__164 _M) (DEF__121 _M) (DEF__163 _M) (DEF__120 _M) (DEF__162 _M) (DEF__119 _M) (DEF__161 _M) (DEF__160 _M) (DEF__159 _M) (DEF__158 _M) (DEF__115 _M) (DEF__157 _M) (DEF__156 _M) (DEF__155 _M) (DEF__154 _M) (DEF__153 _M) (DEF__152 _M) (DEF__151 _M) (DEF__150 _M) (DEF__149 _M) (DEF__148 _M) (DEF__147 _M) (DEF__146 _M) (DEF__145 _M) (DEF__144 _M) (DEF__143 _M) (DEF__142 _M) (DEF__141 _M) (DEF__140 _M) (DEF__139 _M) (DEF__138 _M) (DEF__137 _M) (DEF__180 _M) (DEF__136 _M) (DEF__135 _M) (DEF__177 _M) (DEF__134 _M) (DEF__176 _M) (DEF__133 _M) (DEF__175 _M) (DEF__174 _M) (DEF__173 _M) (DEF__172 _M) )) + +(define-fun P ((_M Int)) Bool(= (___z15z___ _M) true)) + + + +; BASE DONE + +; Begin induction: +; print_initialization +; def_assert_both1 +; def_assert_both +(assert (DEF__172 0)) +; print_checker_assertion +(assert (DEF__173 0)) +; print_checker_assertion +(assert (DEF__174 0)) +; print_checker_assertion +(assert (DEF__175 0)) +; print_checker_assertion +(assert (DEF__133 0)) +; print_checker_assertion +(assert (DEF__176 0)) +; print_checker_assertion +(assert (DEF__134 0)) +; print_checker_assertion +(assert (DEF__177 0)) +; print_checker_assertion +(assert (DEF__135 0)) +; print_checker_assertion +(assert (DEF__136 0)) +; print_checker_assertion +(assert (DEF__180 0)) +; print_checker_assertion +(assert (DEF__137 0)) +; print_checker_assertion +(assert (DEF__138 0)) +; print_checker_assertion +(assert (DEF__139 0)) +; print_checker_assertion +(assert (DEF__140 0)) +; print_checker_assertion +(assert (DEF__141 0)) +; print_checker_assertion +(assert (DEF__142 0)) +; print_checker_assertion +(assert (DEF__143 0)) +; print_checker_assertion +(assert (DEF__144 0)) +; print_checker_assertion +(assert (DEF__145 0)) +; print_checker_assertion +(assert (DEF__146 0)) +; print_checker_assertion +(assert (DEF__147 0)) +; print_checker_assertion +(assert (DEF__148 0)) +; print_checker_assertion +(assert (DEF__149 0)) +; print_checker_assertion +(assert (DEF__150 0)) +; print_checker_assertion +(assert (DEF__151 0)) +; print_checker_assertion +(assert (DEF__152 0)) +; print_checker_assertion +(assert (DEF__153 0)) +; print_checker_assertion +(assert (DEF__154 0)) +; print_checker_assertion +(assert (DEF__155 0)) +; print_checker_assertion +(assert (DEF__156 0)) +; print_checker_assertion +(assert (DEF__157 0)) +; print_checker_assertion +(assert (DEF__115 0)) +; print_checker_assertion +(assert (DEF__158 0)) +; print_checker_assertion +(assert (DEF__159 0)) +; print_checker_assertion +(assert (DEF__160 0)) +; print_checker_assertion +(assert (DEF__161 0)) +; print_checker_assertion +(assert (DEF__119 0)) +; print_checker_assertion +(assert (DEF__162 0)) +; print_checker_assertion +(assert (DEF__120 0)) +; print_checker_assertion +(assert (DEF__163 0)) +; print_checker_assertion +(assert (DEF__121 0)) +; print_checker_assertion +(assert (DEF__164 0)) +; print_checker_assertion +(assert (DEF__122 0)) +; print_checker_assertion +(assert (DEF__165 0)) +; print_checker_assertion +(assert (DEF__123 0)) +; print_checker_assertion +(assert (DEF__166 0)) +; print_checker_assertion +(assert (DEF__124 0)) +; print_checker_assertion +(assert (DEF__167 0)) +; print_checker_assertion +(assert (DEF__125 0)) +; print_checker_assertion +(assert (DEF__168 0)) +; print_checker_assertion +(assert (DEF__126 0)) +; print_checker_assertion +(assert (DEF__169 0)) +; print_checker_assertion +(assert (DEF__170 0)) +; print_checker_assertion +(assert (DEF__171 0)) +; print_checker_assertion +; def_assert_both1 +; def_assert_both +(assert (DEF__172 (- 0 1))) +; print_checker_assertion +(assert (DEF__173 (- 0 1))) +; print_checker_assertion +(assert (DEF__174 (- 0 1))) +; print_checker_assertion +(assert (DEF__175 (- 0 1))) +; print_checker_assertion +(assert (DEF__133 (- 0 1))) +; print_checker_assertion +(assert (DEF__176 (- 0 1))) +; print_checker_assertion +(assert (DEF__134 (- 0 1))) +; print_checker_assertion +(assert (DEF__177 (- 0 1))) +; print_checker_assertion +(assert (DEF__135 (- 0 1))) +; print_checker_assertion +(assert (DEF__136 (- 0 1))) +; print_checker_assertion +(assert (DEF__180 (- 0 1))) +; print_checker_assertion +(assert (DEF__137 (- 0 1))) +; print_checker_assertion +(assert (DEF__138 (- 0 1))) +; print_checker_assertion +(assert (DEF__139 (- 0 1))) +; print_checker_assertion +(assert (DEF__140 (- 0 1))) +; print_checker_assertion +(assert (DEF__141 (- 0 1))) +; print_checker_assertion +(assert (DEF__142 (- 0 1))) +; print_checker_assertion +(assert (DEF__143 (- 0 1))) +; print_checker_assertion +(assert (DEF__144 (- 0 1))) +; print_checker_assertion +(assert (DEF__145 (- 0 1))) +; print_checker_assertion +(assert (DEF__146 (- 0 1))) +; print_checker_assertion +(assert (DEF__147 (- 0 1))) +; print_checker_assertion +(assert (DEF__148 (- 0 1))) +; print_checker_assertion +(assert (DEF__149 (- 0 1))) +; print_checker_assertion +(assert (DEF__150 (- 0 1))) +; print_checker_assertion +(assert (DEF__151 (- 0 1))) +; print_checker_assertion +(assert (DEF__152 (- 0 1))) +; print_checker_assertion +(assert (DEF__153 (- 0 1))) +; print_checker_assertion +(assert (DEF__154 (- 0 1))) +; print_checker_assertion +(assert (DEF__155 (- 0 1))) +; print_checker_assertion +(assert (DEF__156 (- 0 1))) +; print_checker_assertion +(assert (DEF__157 (- 0 1))) +; print_checker_assertion +(assert (DEF__115 (- 0 1))) +; print_checker_assertion +(assert (DEF__158 (- 0 1))) +; print_checker_assertion +(assert (DEF__159 (- 0 1))) +; print_checker_assertion +(assert (DEF__160 (- 0 1))) +; print_checker_assertion +(assert (DEF__161 (- 0 1))) +; print_checker_assertion +(assert (DEF__119 (- 0 1))) +; print_checker_assertion +(assert (DEF__162 (- 0 1))) +; print_checker_assertion +(assert (DEF__120 (- 0 1))) +; print_checker_assertion +(assert (DEF__163 (- 0 1))) +; print_checker_assertion +(assert (DEF__121 (- 0 1))) +; print_checker_assertion +(assert (DEF__164 (- 0 1))) +; print_checker_assertion +(assert (DEF__122 (- 0 1))) +; print_checker_assertion +(assert (DEF__165 (- 0 1))) +; print_checker_assertion +(assert (DEF__123 (- 0 1))) +; print_checker_assertion +(assert (DEF__166 (- 0 1))) +; print_checker_assertion +(assert (DEF__124 (- 0 1))) +; print_checker_assertion +(assert (DEF__167 (- 0 1))) +; print_checker_assertion +(assert (DEF__125 (- 0 1))) +; print_checker_assertion +(assert (DEF__168 (- 0 1))) +; print_checker_assertion +(assert (DEF__126 (- 0 1))) +; print_checker_assertion +(assert (DEF__169 (- 0 1))) +; print_checker_assertion +(assert (DEF__170 (- 0 1))) +; print_checker_assertion +(assert (DEF__171 (- 0 1))) +; print_checker_assertion + +; Checking k=2 base +; not refinement_pass +(assert (not (=> (= _base (- 0 1)) (and (P (- 0 1)) (P 0))))) +(assert true) +(check-sat) diff --git a/test/regress/regress1/uflia/simple_cyclic2.smt2 b/test/regress/regress1/uflia/simple_cyclic2.smt2 new file mode 100644 index 000000000..7a0b39999 --- /dev/null +++ b/test/regress/regress1/uflia/simple_cyclic2.smt2 @@ -0,0 +1,44 @@ +(set-logic QF_UFIDL) +(set-info :source | +Benchmark generated from the verification of programs manipulating linked lists inside UCLID. For more information see: +"Verifying properties of well-founded linked lists", Shuvendu Lahiri and Shaz Qaader, POPL 2006 + +This benchmark was automatically translated into SMT-LIB format by Albert Oliveras. +|) +(set-info :smt-lib-version 2.0) +(set-info :category "industrial") +(set-info :status sat) +(declare-fun t.l () Int) +(declare-fun en_LOCATION () Int) +(declare-fun NULL () Int) +(declare-fun ZERO () Int) +(declare-fun i1 () Int) +(declare-fun t.l0 () Int) +(declare-fun t.pc () Int) +(declare-fun t.t () Int) +(declare-fun PRED_VAR__p_0 () Bool) +(declare-fun PRED_VAR__p_1 () Bool) +(declare-fun PRED_VAR__p_2 () Bool) +(declare-fun PRED_VAR__p_16 () Bool) +(declare-fun PRED_VAR__p_11 () Bool) +(declare-fun PRED_VAR__p_10 () Bool) +(declare-fun PRED_VAR__p_14 () Bool) +(declare-fun PRED_VAR__p_12 () Bool) +(declare-fun PRED_VAR__p_15 () Bool) +(declare-fun PRED_VAR__p_18 () Bool) +(declare-fun PRED_VAR__p_19 () Bool) +(declare-fun PRED_VAR__p_3 () Bool) +(declare-fun PRED_VAR__p_20 () Bool) +(declare-fun PRED_VAR__p_8 () Bool) +(declare-fun PRED_VAR__p_9 () Bool) +(declare-fun t.I_nxt (Int) Int) +(declare-fun t.I_nxt0 (Int) Int) +(declare-fun t.data (Int) Int) +(declare-fun t.nxt (Int) Int) +(declare-fun t.H_nxt (Int) Bool) +(declare-fun t.R_nxt (Int Int) Bool) +(declare-fun t.H_nxt0 (Int) Bool) +(declare-fun t.R_nxt0 (Int Int) Bool) +(assert (let ((?v_0 (t.nxt t.l))) (let ((?v_7 (t.H_nxt ?v_0)) (?v_242 (+ 1 (+ 1 (+ 1 (+ 1 en_LOCATION)))))) (let ((?v_1 (= t.pc ?v_242)) (?v_2 (t.R_nxt ?v_0 i1))) (let ((?v_3 (not ?v_1))) (let ((?v_6 (or (and ?v_1 ?v_2) (and ?v_3 ?v_2))) (?v_4 (t.R_nxt t.l i1))) (let ((?v_247 (or (and ?v_1 ?v_4) (and ?v_3 ?v_4))) (?v_112 (= i1 t.l))) (let ((?v_5 (and ?v_247 (not ?v_112))) (?v_8 (t.R_nxt ?v_0 t.l)) (?v_9 (t.R_nxt ?v_0 t.t))) (let ((?v_12 (or (and ?v_1 ?v_9) (and ?v_3 ?v_9))) (?v_10 (t.R_nxt t.l t.t)) (?v_127 (= t.t t.l))) (let ((?v_22 (not ?v_127))) (let ((?v_11 (and (or (and ?v_1 ?v_10) (and ?v_3 ?v_10)) ?v_22)) (?v_13 (t.R_nxt ?v_0 ?v_0))) (let ((?v_16 (or (and ?v_1 ?v_13) (and ?v_3 ?v_13))) (?v_14 (t.R_nxt t.l ?v_0)) (?v_55 (= ?v_0 t.l))) (let ((?v_15 (and (or (and ?v_1 ?v_14) (and ?v_3 ?v_14)) (not ?v_55))) (?v_18 (t.nxt t.t))) (let ((?v_17 (t.R_nxt ?v_0 ?v_18))) (let ((?v_21 (or (and ?v_1 ?v_17) (and ?v_3 ?v_17))) (?v_19 (t.R_nxt t.l ?v_18)) (?v_72 (= ?v_18 t.l))) (let ((?v_20 (and (or (and ?v_1 ?v_19) (and ?v_3 ?v_19)) (not ?v_72))) (?v_31 (t.H_nxt ?v_18)) (?v_147 (= t.pc en_LOCATION))) (let ((?v_23 (and ?v_147 ?v_22)) (?v_24 (t.R_nxt ?v_18 i1))) (let ((?v_26 (not ?v_23))) (let ((?v_25 (and ?v_26 ?v_24))) (let ((?v_30 (or (and ?v_23 (or (and ?v_23 ?v_24) ?v_25)) ?v_25)) (?v_27 (t.R_nxt t.t i1))) (let ((?v_28 (and ?v_26 ?v_27)) (?v_116 (= i1 t.t))) (let ((?v_29 (and (or (and ?v_23 (or (and ?v_23 ?v_27) ?v_28)) ?v_28) (not ?v_116))) (?v_32 (t.R_nxt ?v_18 t.l))) (let ((?v_33 (and ?v_26 ?v_32))) (let ((?v_37 (or (and ?v_23 (or (and ?v_23 ?v_32) ?v_33)) ?v_33)) (?v_34 (t.R_nxt t.t t.l))) (let ((?v_35 (and ?v_26 ?v_34))) (let ((?v_36 (and (or (and ?v_23 (or (and ?v_23 ?v_34) ?v_35)) ?v_35) ?v_22)) (?v_38 (t.R_nxt ?v_18 t.t))) (let ((?v_39 (and ?v_26 ?v_38)) (?v_40 (t.R_nxt ?v_18 ?v_0))) (let ((?v_41 (and ?v_26 ?v_40))) (let ((?v_45 (or (and ?v_23 (or (and ?v_23 ?v_40) ?v_41)) ?v_41)) (?v_42 (t.R_nxt t.t ?v_0))) (let ((?v_43 (and ?v_26 ?v_42)) (?v_60 (= ?v_0 t.t))) (let ((?v_44 (and (or (and ?v_23 (or (and ?v_23 ?v_42) ?v_43)) ?v_43) (not ?v_60))) (?v_46 (t.R_nxt ?v_18 ?v_18))) (let ((?v_47 (and ?v_26 ?v_46))) (let ((?v_51 (or (and ?v_23 (or (and ?v_23 ?v_46) ?v_47)) ?v_47)) (?v_48 (t.R_nxt t.t ?v_18))) (let ((?v_49 (and ?v_26 ?v_48)) (?v_78 (= ?v_18 t.t))) (let ((?v_50 (and (or (and ?v_23 (or (and ?v_23 ?v_48) ?v_49)) ?v_49) (not ?v_78))) (?v_54 (t.I_nxt t.l))) (let ((?v_53 (= ?v_54 i1)) (?v_67 (t.H_nxt i1)) (?v_120 (= i1 ?v_0)) (?v_56 (not ?v_7)) (?v_57 (t.I_nxt ?v_0))) (let ((?v_86 (= i1 ?v_57))) (let ((?v_52 (or (and ?v_67 ?v_120) (and ?v_56 ?v_86))) (?v_59 (= ?v_54 t.l))) (let ((?v_260 (not ?v_59)) (?v_71 (t.H_nxt t.l)) (?v_89 (= ?v_57 t.l))) (let ((?v_58 (or (and ?v_71 ?v_55) (and ?v_56 ?v_89))) (?v_62 (= ?v_54 t.t)) (?v_77 (t.H_nxt t.t)) (?v_93 (= t.t ?v_57))) (let ((?v_61 (or (and ?v_77 ?v_60) (and ?v_56 ?v_93))) (?v_64 (= ?v_54 ?v_0)) (?v_95 (= ?v_0 ?v_57))) (let ((?v_63 (or ?v_7 ?v_95)) (?v_66 (= ?v_54 ?v_18)) (?v_81 (= ?v_18 ?v_0)) (?v_97 (= ?v_18 ?v_57))) (let ((?v_65 (or (and ?v_31 ?v_81) (and ?v_56 ?v_97))) (?v_70 (t.I_nxt t.t))) (let ((?v_69 (= ?v_70 i1)) (?v_123 (= i1 ?v_18)) (?v_73 (not ?v_31)) (?v_74 (t.I_nxt ?v_18))) (let ((?v_99 (= i1 ?v_74))) (let ((?v_68 (or (and ?v_67 ?v_123) (and ?v_73 ?v_99))) (?v_76 (= ?v_70 t.l)) (?v_102 (= ?v_74 t.l))) (let ((?v_75 (or (and ?v_71 ?v_72) (and ?v_73 ?v_102))) (?v_80 (= ?v_70 t.t)) (?v_106 (= t.t ?v_74))) (let ((?v_79 (or (and ?v_77 ?v_78) (and ?v_73 ?v_106))) (?v_83 (= ?v_70 ?v_0)) (?v_108 (= ?v_0 ?v_74))) (let ((?v_82 (or (and ?v_7 ?v_81) (and ?v_73 ?v_108))) (?v_85 (= ?v_70 ?v_18)) (?v_110 (= ?v_18 ?v_74))) (let ((?v_84 (or ?v_31 ?v_110)) (?v_87 (t.nxt ?v_0))) (let ((?v_90 (not (t.H_nxt ?v_87))) (?v_91 (t.I_nxt ?v_87))) (let ((?v_88 (or (and ?v_67 (= i1 ?v_87)) (and ?v_90 (= i1 ?v_91)))) (?v_92 (or (and ?v_71 (= t.l ?v_87)) (and ?v_90 (= t.l ?v_91)))) (?v_94 (or (and ?v_77 (= t.t ?v_87)) (and ?v_90 (= t.t ?v_91)))) (?v_96 (or (and ?v_7 (= ?v_0 ?v_87)) (and ?v_90 (= ?v_0 ?v_91)))) (?v_98 (or (and ?v_31 (= ?v_18 ?v_87)) (and ?v_90 (= ?v_18 ?v_91)))) (?v_100 (t.nxt ?v_18))) (let ((?v_103 (not (t.H_nxt ?v_100))) (?v_104 (t.I_nxt ?v_100))) (let ((?v_101 (or (and ?v_67 (= i1 ?v_100)) (and ?v_103 (= i1 ?v_104)))) (?v_105 (or (and ?v_71 (= t.l ?v_100)) (and ?v_103 (= t.l ?v_104)))) (?v_107 (or (and ?v_77 (= t.t ?v_100)) (and ?v_103 (= t.t ?v_104)))) (?v_109 (or (and ?v_7 (= ?v_0 ?v_100)) (and ?v_103 (= ?v_0 ?v_104)))) (?v_111 (or (and ?v_31 (= ?v_18 ?v_100)) (and ?v_103 (= ?v_18 ?v_104)))) (?v_156 (t.R_nxt i1 i1)) (?v_115 (t.R_nxt i1 t.l)) (?v_113 (t.nxt i1))) (let ((?v_117 (not (t.H_nxt ?v_113)))) (let ((?v_114 (or ?v_112 (and ?v_117 (t.R_nxt ?v_113 t.l)))) (?v_119 (t.R_nxt i1 t.t)) (?v_118 (or ?v_116 (and ?v_117 (t.R_nxt ?v_113 t.t)))) (?v_122 (t.R_nxt i1 ?v_0)) (?v_121 (or ?v_120 (and ?v_117 (t.R_nxt ?v_113 ?v_0)))) (?v_125 (t.R_nxt i1 ?v_18)) (?v_124 (or ?v_123 (and ?v_117 (t.R_nxt ?v_113 ?v_18)))) (?v_149 (not ?v_4)) (?v_126 (or ?v_112 (and ?v_56 ?v_2))) (?v_169 (t.R_nxt t.l t.l)) (?v_190 (not ?v_10)) (?v_128 (or ?v_127 (and ?v_56 ?v_9))) (?v_209 (not ?v_14)) (?v_129 (or ?v_55 (and ?v_56 ?v_13))) (?v_227 (not ?v_19)) (?v_130 (or ?v_72 (and ?v_56 ?v_17))) (?v_157 (not ?v_27)) (?v_131 (or ?v_116 (and ?v_73 ?v_24))) (?v_178 (not ?v_34)) (?v_132 (or ?v_127 (and ?v_73 ?v_32))) (?v_196 (t.R_nxt t.t t.t)) (?v_214 (not ?v_42)) (?v_133 (or ?v_60 (and ?v_73 ?v_40))) (?v_232 (not ?v_48)) (?v_134 (or ?v_78 (and ?v_73 ?v_46))) (?v_135 (or ?v_120 (and ?v_90 (t.R_nxt ?v_87 i1)))) (?v_136 (or ?v_55 (and ?v_90 (t.R_nxt ?v_87 t.l)))) (?v_137 (or ?v_60 (and ?v_90 (t.R_nxt ?v_87 t.t)))) (?v_138 (or ?v_81 (and ?v_90 (t.R_nxt ?v_87 ?v_18)))) (?v_139 (or ?v_123 (and ?v_103 (t.R_nxt ?v_100 i1)))) (?v_140 (or ?v_72 (and ?v_103 (t.R_nxt ?v_100 t.l)))) (?v_141 (or ?v_78 (and ?v_103 (t.R_nxt ?v_100 t.t)))) (?v_142 (or ?v_81 (and ?v_103 (t.R_nxt ?v_100 ?v_0)))) (?v_146 (= (t.I_nxt0 t.l0) t.l0)) (?v_143 (= i1 NULL)) (?v_145 (t.H_nxt0 i1)) (?v_144 (= t.l t.l0)) (?v_168 (= t.l NULL)) (?v_170 (t.H_nxt0 t.l)) (?v_187 (= t.t NULL)) (?v_188 (t.H_nxt0 t.t)) (?v_206 (= ?v_0 NULL)) (?v_207 (t.H_nxt0 ?v_0)) (?v_224 (= ?v_18 NULL)) (?v_225 (t.H_nxt0 ?v_18))) (let ((?v_148 (not ?v_143)) (?v_150 (t.R_nxt0 t.l i1)) (?v_152 (and ?v_146 (and ?v_1 (not ?v_147))))) (let ((?v_151 (and ?v_145 ?v_152))) (let ((?v_160 (and ?v_22 (and ?v_59 (and ?v_67 (and ?v_4 (and ?v_144 (and ?v_150 ?v_151))))))) (?v_154 (not ?v_150))) (let ((?v_161 (and ?v_22 (and ?v_59 (and ?v_67 (and ?v_149 (and ?v_144 (and ?v_154 ?v_151))))))) (?v_153 (not ?v_67)) (?v_158 (not ?v_145))) (let ((?v_155 (and ?v_158 ?v_152)) (?v_159 (and ?v_146 (and ?v_147 ?v_3)))) (let ((?v_163 (and ?v_145 ?v_159)) (?v_164 (and ?v_158 ?v_159)) (?v_162 (not ?v_156))) (let ((?v_165 (and ?v_59 (and ?v_67 (and ?v_4 (and ?v_144 (and ?v_150 ?v_163))))))) (let ((?v_167 (and ?v_22 ?v_165)) (?v_258 (t.data i1))) (let ((?v_166 (= ?v_258 ZERO)) (?v_171 (not ?v_168)) (?v_172 (t.R_nxt0 t.l t.l)) (?v_173 (and ?v_170 ?v_152))) (let ((?v_180 (and ?v_22 (and ?v_59 (and ?v_71 (and ?v_169 (and ?v_144 (and ?v_172 ?v_173))))))) (?v_175 (not ?v_169)) (?v_176 (not ?v_172))) (let ((?v_181 (and ?v_22 (and ?v_59 (and ?v_71 (and ?v_175 (and ?v_144 (and ?v_176 ?v_173))))))) (?v_174 (not ?v_71)) (?v_179 (not ?v_170))) (let ((?v_177 (and ?v_179 ?v_152)) (?v_182 (and ?v_170 ?v_159)) (?v_183 (and ?v_179 ?v_159))) (let ((?v_184 (and ?v_59 (and ?v_71 (and ?v_169 (and ?v_144 (and ?v_172 ?v_182))))))) (let ((?v_186 (and ?v_22 ?v_184)) (?v_185 (= (t.data t.l) ZERO)) (?v_189 (not ?v_187)) (?v_191 (t.R_nxt0 t.l t.t)) (?v_192 (and ?v_188 ?v_152))) (let ((?v_199 (and ?v_22 (and ?v_59 (and ?v_77 (and ?v_10 (and ?v_144 (and ?v_191 ?v_192))))))) (?v_194 (not ?v_191))) (let ((?v_200 (and ?v_22 (and ?v_59 (and ?v_77 (and ?v_190 (and ?v_144 (and ?v_194 ?v_192))))))) (?v_193 (not ?v_77)) (?v_198 (not ?v_188))) (let ((?v_195 (and ?v_198 ?v_152)) (?v_197 (not ?v_196)) (?v_201 (and ?v_188 ?v_159)) (?v_202 (and ?v_198 ?v_159))) (let ((?v_203 (and ?v_59 (and ?v_77 (and ?v_10 (and ?v_144 (and ?v_191 ?v_201))))))) (let ((?v_205 (and ?v_22 ?v_203)) (?v_204 (= (t.data t.t) ZERO)) (?v_208 (not ?v_206)) (?v_210 (t.R_nxt0 t.l ?v_0)) (?v_211 (and ?v_207 ?v_152))) (let ((?v_216 (and ?v_22 (and ?v_59 (and ?v_7 (and ?v_14 (and ?v_144 (and ?v_210 ?v_211))))))) (?v_212 (not ?v_210))) (let ((?v_217 (and ?v_22 (and ?v_59 (and ?v_7 (and ?v_209 (and ?v_144 (and ?v_212 ?v_211))))))) (?v_215 (not ?v_207))) (let ((?v_213 (and ?v_215 ?v_152)) (?v_219 (and ?v_207 ?v_159)) (?v_220 (and ?v_215 ?v_159)) (?v_218 (not ?v_13))) (let ((?v_221 (and ?v_59 (and ?v_7 (and ?v_14 (and ?v_144 (and ?v_210 ?v_219))))))) (let ((?v_223 (and ?v_22 ?v_221)) (?v_222 (= (t.data ?v_0) ZERO)) (?v_226 (not ?v_224)) (?v_228 (t.R_nxt0 t.l ?v_18)) (?v_229 (and ?v_225 ?v_152))) (let ((?v_234 (and ?v_22 (and ?v_59 (and ?v_31 (and ?v_19 (and ?v_144 (and ?v_228 ?v_229))))))) (?v_230 (not ?v_228))) (let ((?v_235 (and ?v_22 (and ?v_59 (and ?v_31 (and ?v_227 (and ?v_144 (and ?v_230 ?v_229))))))) (?v_233 (not ?v_225))) (let ((?v_231 (and ?v_233 ?v_152)) (?v_237 (and ?v_225 ?v_159)) (?v_238 (and ?v_233 ?v_159)) (?v_236 (not ?v_46))) (let ((?v_239 (and ?v_59 (and ?v_31 (and ?v_19 (and ?v_144 (and ?v_228 ?v_237))))))) (let ((?v_241 (and ?v_22 ?v_239)) (?v_240 (= (t.data ?v_18) ZERO)) (?v_246 (or ?v_1 ?v_23))) (let ((?v_244 (ite ?v_246 en_LOCATION (+ 1 (+ 1 ?v_242))))) (let ((?v_243 (= ?v_244 ?v_242)) (?v_278 (not PRED_VAR__p_0)) (?v_245 (= ?v_244 en_LOCATION)) (?v_269 (not PRED_VAR__p_1)) (?v_274 (not PRED_VAR__p_3)) (?v_271 (not PRED_VAR__p_16)) (?v_248 (and ?v_26 ?v_4)) (?v_254 (not ?v_246)) (?v_249 (and ?v_147 ?v_127))) (let ((?v_255 (not ?v_249))) (let ((?v_250 (and ?v_255 ?v_4))) (let ((?v_251 (or (and ?v_246 (or (and ?v_1 ?v_247) (and ?v_3 (or (and ?v_23 (or (and ?v_23 (or (and ?v_23 ?v_4) ?v_248)) ?v_248)) ?v_248)))) (and ?v_254 (or (and ?v_249 (or (and ?v_249 ?v_4) ?v_250)) ?v_250)))) (?v_270 (not PRED_VAR__p_8)) (?v_261 (ite ?v_246 (ite ?v_1 ?v_0 (ite ?v_23 ?v_18 t.t)) t.t))) (let ((?v_252 (t.R_nxt ?v_261 i1))) (let ((?v_253 (and ?v_26 ?v_252)) (?v_256 (and ?v_255 ?v_252))) (let ((?v_257 (or (and ?v_246 (or (and ?v_1 (or (and ?v_1 ?v_252) (and ?v_3 ?v_252))) (and ?v_3 (or (and ?v_23 (or (and ?v_23 (or (and ?v_23 ?v_252) ?v_253)) ?v_253)) ?v_253)))) (and ?v_254 (or (and ?v_249 (or (and ?v_249 ?v_252) ?v_256)) ?v_256)))) (?v_277 (not PRED_VAR__p_9)) (?v_273 (not PRED_VAR__p_14)) (?v_259 (= (ite ?v_246 (ite ?v_1 (ite ?v_1 (ite ?v_112 ZERO ?v_258) ?v_258) (ite ?v_23 (ite ?v_23 (ite ?v_116 ZERO ?v_258) ?v_258) ?v_258)) ?v_258) ZERO)) (?v_262 (= (t.I_nxt ?v_261) t.l)) (?v_263 (= ?v_261 t.l)) (?v_268 (not PRED_VAR__p_18)) (?v_267 (not PRED_VAR__p_19)) (?v_264 (and ?v_26 ?v_156)) (?v_265 (and ?v_255 ?v_156))) (let ((?v_266 (or (and ?v_246 (or (and ?v_1 (or (and ?v_1 ?v_156) (and ?v_3 ?v_156))) (and ?v_3 (or (and ?v_23 (or (and ?v_23 (or (and ?v_23 ?v_156) ?v_264)) ?v_264)) ?v_264)))) (and ?v_254 (or (and ?v_249 (or (and ?v_249 ?v_156) ?v_265)) ?v_265)))) (?v_281 (not PRED_VAR__p_20)) (?v_275 (and PRED_VAR__p_2 (and PRED_VAR__p_0 ?v_269)))) (let ((?v_272 (and PRED_VAR__p_3 ?v_275))) (let ((?v_280 (and ?v_268 (and PRED_VAR__p_10 (and PRED_VAR__p_14 (and PRED_VAR__p_8 (and PRED_VAR__p_11 (and PRED_VAR__p_16 ?v_272))))))) (?v_282 (and ?v_268 (and PRED_VAR__p_10 (and PRED_VAR__p_14 (and ?v_270 (and PRED_VAR__p_11 (and ?v_271 ?v_272))))))) (?v_276 (and ?v_274 ?v_275)) (?v_279 (and PRED_VAR__p_2 (and PRED_VAR__p_1 ?v_278)))) (let ((?v_283 (and PRED_VAR__p_3 ?v_279)) (?v_284 (and ?v_274 ?v_279))) (let ((?v_285 (and PRED_VAR__p_10 (and PRED_VAR__p_14 (and PRED_VAR__p_8 (and PRED_VAR__p_11 (and PRED_VAR__p_16 ?v_283))))))) (let ((?v_286 (and ?v_268 ?v_285))) (and (and (and (and (and (and (and (and (and (and (or ?v_7 (and (or (not ?v_6) ?v_5) (or (not ?v_5) ?v_6))) (and (or ?v_7 (not (or (and ?v_1 ?v_8) (and ?v_3 ?v_8)))) (and (or ?v_7 (and (or (not ?v_12) ?v_11) (or (not ?v_11) ?v_12))) (and (or ?v_7 (and (or (not ?v_16) ?v_15) (or (not ?v_15) ?v_16))) (or ?v_7 (and (or (not ?v_21) ?v_20) (or (not ?v_20) ?v_21))))))) (and (or ?v_31 (and (or (not ?v_30) ?v_29) (or (not ?v_29) ?v_30))) (and (or ?v_31 (and (or (not ?v_37) ?v_36) (or (not ?v_36) ?v_37))) (and (or ?v_31 (not (or (and ?v_23 (or (and ?v_23 ?v_38) ?v_39)) ?v_39))) (and (or ?v_31 (and (or (not ?v_45) ?v_44) (or (not ?v_44) ?v_45))) (or ?v_31 (and (or (not ?v_51) ?v_50) (or (not ?v_50) ?v_51)))))))) (and (and (or (not ?v_53) ?v_52) (or (not ?v_52) ?v_53)) (and (and (or ?v_260 ?v_58) (or (not ?v_58) ?v_59)) (and (and (or (not ?v_62) ?v_61) (or (not ?v_61) ?v_62)) (and (and (or (not ?v_64) ?v_63) (or (not ?v_63) ?v_64)) (and (and (or (not ?v_66) ?v_65) (or (not ?v_65) ?v_66)) (and (and (or (not ?v_69) ?v_68) (or (not ?v_68) ?v_69)) (and (and (or (not ?v_76) ?v_75) (or (not ?v_75) ?v_76)) (and (and (or (not ?v_80) ?v_79) (or (not ?v_79) ?v_80)) (and (and (or (not ?v_83) ?v_82) (or (not ?v_82) ?v_83)) (and (and (or (not ?v_85) ?v_84) (or (not ?v_84) ?v_85)) (and (and (or (not ?v_86) ?v_88) (or (not ?v_88) ?v_86)) (and (and (or (not ?v_89) ?v_92) (or (not ?v_92) ?v_89)) (and (and (or (not ?v_93) ?v_94) (or (not ?v_94) ?v_93)) (and (and (or (not ?v_95) ?v_96) (or (not ?v_96) ?v_95)) (and (and (or (not ?v_97) ?v_98) (or (not ?v_98) ?v_97)) (and (and (or (not ?v_99) ?v_101) (or (not ?v_101) ?v_99)) (and (and (or (not ?v_102) ?v_105) (or (not ?v_105) ?v_102)) (and (and (or (not ?v_106) ?v_107) (or (not ?v_107) ?v_106)) (and (and (or (not ?v_108) ?v_109) (or (not ?v_109) ?v_108)) (and (or (not ?v_110) ?v_111) (or (not ?v_111) ?v_110)))))))))))))))))))))) (and ?v_156 (and (and (or (not ?v_115) ?v_114) (or (not ?v_114) ?v_115)) (and (and (or (not ?v_119) ?v_118) (or (not ?v_118) ?v_119)) (and (and (or (not ?v_122) ?v_121) (or (not ?v_121) ?v_122)) (and (and (or (not ?v_125) ?v_124) (or (not ?v_124) ?v_125)) (and (and (or ?v_149 ?v_126) (or (not ?v_126) ?v_4)) (and ?v_169 (and (and (or ?v_190 ?v_128) (or (not ?v_128) ?v_10)) (and (and (or ?v_209 ?v_129) (or (not ?v_129) ?v_14)) (and (and (or ?v_227 ?v_130) (or (not ?v_130) ?v_19)) (and (and (or ?v_157 ?v_131) (or (not ?v_131) ?v_27)) (and (and (or ?v_178 ?v_132) (or (not ?v_132) ?v_34)) (and ?v_196 (and (and (or ?v_214 ?v_133) (or (not ?v_133) ?v_42)) (and (and (or ?v_232 ?v_134) (or (not ?v_134) ?v_48)) (and (and (or (not ?v_2) ?v_135) (or (not ?v_135) ?v_2)) (and (and (or (not ?v_8) ?v_136) (or (not ?v_136) ?v_8)) (and (and (or (not ?v_9) ?v_137) (or (not ?v_137) ?v_9)) (and ?v_13 (and (and (or (not ?v_17) ?v_138) (or (not ?v_138) ?v_17)) (and (and (or (not ?v_24) ?v_139) (or (not ?v_139) ?v_24)) (and (and (or (not ?v_32) ?v_140) (or (not ?v_140) ?v_32)) (and (and (or (not ?v_38) ?v_141) (or (not ?v_141) ?v_38)) (and (and (or (not ?v_40) ?v_142) (or (not ?v_142) ?v_40)) ?v_46))))))))))))))))))))))))) (and (t.H_nxt NULL) (= (t.nxt NULL) NULL))) ?v_146) (and (or (not (or (= i1 t.l0) ?v_143)) ?v_145) (and (or (not (or ?v_144 ?v_168)) ?v_170) (and (or (not (or (= t.t t.l0) ?v_187)) ?v_188) (and (or (not (or (= ?v_0 t.l0) ?v_206)) ?v_207) (or (not (or (= ?v_18 t.l0) ?v_224)) ?v_225)))))) (not (= NULL t.l0))) (and (and (or (or (or (or (or (or (or (or (or (or (or (or (or (and ?v_148 ?v_160) (and ?v_148 ?v_161)) (and ?v_148 (and ?v_22 (and ?v_59 (and ?v_153 (and ?v_4 (and ?v_144 (and ?v_150 ?v_155)))))))) (and ?v_148 (and ?v_22 (and ?v_59 (and ?v_153 (and ?v_149 (and ?v_144 (and ?v_154 ?v_155)))))))) (and ?v_76 (and ?v_156 (and ?v_157 (and ?v_59 (and ?v_67 (and ?v_149 (and ?v_144 (and ?v_154 ?v_163))))))))) (and ?v_76 (and ?v_156 (and ?v_157 (and ?v_148 (and ?v_59 (and ?v_153 (and ?v_149 (and ?v_144 (and ?v_154 ?v_164)))))))))) (and ?v_156 (and ?v_27 ?v_160))) (and ?v_162 (and ?v_157 ?v_160))) (and ?v_156 (and ?v_27 ?v_161))) (and ?v_162 (and ?v_157 ?v_161))) (and ?v_76 (and ?v_156 (and ?v_27 ?v_167)))) (and ?v_76 (and ?v_156 (and ?v_27 (and ?v_148 (and ?v_22 (and ?v_59 (and ?v_153 (and ?v_4 (and ?v_144 (and ?v_150 ?v_164))))))))))) (and ?v_166 (and ?v_76 (and ?v_156 (and ?v_27 (and ?v_148 ?v_165)))))) (and ?v_166 (and ?v_76 (and ?v_156 (and ?v_148 ?v_167))))) (and (or (or (or (or (or (or (or (or (or (or (or (or (or (and ?v_171 ?v_180) (and ?v_171 ?v_181)) (and ?v_171 (and ?v_22 (and ?v_59 (and ?v_174 (and ?v_169 (and ?v_144 (and ?v_172 ?v_177)))))))) (and ?v_171 (and ?v_22 (and ?v_59 (and ?v_174 (and ?v_175 (and ?v_144 (and ?v_176 ?v_177)))))))) (and ?v_76 (and ?v_169 (and ?v_178 (and ?v_59 (and ?v_71 (and ?v_175 (and ?v_144 (and ?v_176 ?v_182))))))))) (and ?v_76 (and ?v_169 (and ?v_178 (and ?v_171 (and ?v_59 (and ?v_174 (and ?v_175 (and ?v_144 (and ?v_176 ?v_183)))))))))) (and ?v_169 (and ?v_34 ?v_180))) (and ?v_175 (and ?v_178 ?v_180))) (and ?v_169 (and ?v_34 ?v_181))) (and ?v_175 (and ?v_178 ?v_181))) (and ?v_76 (and ?v_169 (and ?v_34 ?v_186)))) (and ?v_76 (and ?v_169 (and ?v_34 (and ?v_171 (and ?v_22 (and ?v_59 (and ?v_174 (and ?v_169 (and ?v_144 (and ?v_172 ?v_183))))))))))) (and ?v_185 (and ?v_76 (and ?v_169 (and ?v_34 (and ?v_171 ?v_184)))))) (and ?v_185 (and ?v_76 (and ?v_169 (and ?v_171 ?v_186))))) (and (or (or (or (or (or (or (or (or (or (or (or (or (or (and ?v_189 ?v_199) (and ?v_189 ?v_200)) (and ?v_189 (and ?v_22 (and ?v_59 (and ?v_193 (and ?v_10 (and ?v_144 (and ?v_191 ?v_195)))))))) (and ?v_189 (and ?v_22 (and ?v_59 (and ?v_193 (and ?v_190 (and ?v_144 (and ?v_194 ?v_195)))))))) (and ?v_76 (and ?v_196 (and ?v_197 (and ?v_59 (and ?v_77 (and ?v_190 (and ?v_144 (and ?v_194 ?v_201))))))))) (and ?v_76 (and ?v_196 (and ?v_197 (and ?v_189 (and ?v_59 (and ?v_193 (and ?v_190 (and ?v_144 (and ?v_194 ?v_202)))))))))) (and ?v_196 (and ?v_196 ?v_199))) (and ?v_197 (and ?v_197 ?v_199))) (and ?v_196 (and ?v_196 ?v_200))) (and ?v_197 (and ?v_197 ?v_200))) (and ?v_76 (and ?v_196 (and ?v_196 ?v_205)))) (and ?v_76 (and ?v_196 (and ?v_196 (and ?v_189 (and ?v_22 (and ?v_59 (and ?v_193 (and ?v_10 (and ?v_144 (and ?v_191 ?v_202))))))))))) (and ?v_204 (and ?v_76 (and ?v_196 (and ?v_196 (and ?v_189 ?v_203)))))) (and ?v_204 (and ?v_76 (and ?v_196 (and ?v_189 ?v_205))))) (and (or (or (or (or (or (or (or (or (or (or (or (or (or (and ?v_208 ?v_216) (and ?v_208 ?v_217)) (and ?v_208 (and ?v_22 (and ?v_59 (and ?v_56 (and ?v_14 (and ?v_144 (and ?v_210 ?v_213)))))))) (and ?v_208 (and ?v_22 (and ?v_59 (and ?v_56 (and ?v_209 (and ?v_144 (and ?v_212 ?v_213)))))))) (and ?v_76 (and ?v_13 (and ?v_214 (and ?v_59 (and ?v_7 (and ?v_209 (and ?v_144 (and ?v_212 ?v_219))))))))) (and ?v_76 (and ?v_13 (and ?v_214 (and ?v_208 (and ?v_59 (and ?v_56 (and ?v_209 (and ?v_144 (and ?v_212 ?v_220)))))))))) (and ?v_13 (and ?v_42 ?v_216))) (and ?v_218 (and ?v_214 ?v_216))) (and ?v_13 (and ?v_42 ?v_217))) (and ?v_218 (and ?v_214 ?v_217))) (and ?v_76 (and ?v_13 (and ?v_42 ?v_223)))) (and ?v_76 (and ?v_13 (and ?v_42 (and ?v_208 (and ?v_22 (and ?v_59 (and ?v_56 (and ?v_14 (and ?v_144 (and ?v_210 ?v_220))))))))))) (and ?v_222 (and ?v_76 (and ?v_13 (and ?v_42 (and ?v_208 ?v_221)))))) (and ?v_222 (and ?v_76 (and ?v_13 (and ?v_208 ?v_223))))) (or (or (or (or (or (or (or (or (or (or (or (or (or (and ?v_226 ?v_234) (and ?v_226 ?v_235)) (and ?v_226 (and ?v_22 (and ?v_59 (and ?v_73 (and ?v_19 (and ?v_144 (and ?v_228 ?v_231)))))))) (and ?v_226 (and ?v_22 (and ?v_59 (and ?v_73 (and ?v_227 (and ?v_144 (and ?v_230 ?v_231)))))))) (and ?v_76 (and ?v_46 (and ?v_232 (and ?v_59 (and ?v_31 (and ?v_227 (and ?v_144 (and ?v_230 ?v_237))))))))) (and ?v_76 (and ?v_46 (and ?v_232 (and ?v_226 (and ?v_59 (and ?v_73 (and ?v_227 (and ?v_144 (and ?v_230 ?v_238)))))))))) (and ?v_46 (and ?v_48 ?v_234))) (and ?v_236 (and ?v_232 ?v_234))) (and ?v_46 (and ?v_48 ?v_235))) (and ?v_236 (and ?v_232 ?v_235))) (and ?v_76 (and ?v_46 (and ?v_48 ?v_241)))) (and ?v_76 (and ?v_46 (and ?v_48 (and ?v_226 (and ?v_22 (and ?v_59 (and ?v_73 (and ?v_19 (and ?v_144 (and ?v_228 ?v_238))))))))))) (and ?v_240 (and ?v_76 (and ?v_46 (and ?v_48 (and ?v_226 ?v_239)))))) (and ?v_240 (and ?v_76 (and ?v_46 (and ?v_226 ?v_241))))))))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (and PRED_VAR__p_0 ?v_243) (and ?v_278 (not ?v_243))) (or (and PRED_VAR__p_1 ?v_245) (and ?v_269 (not ?v_245)))) (or (and PRED_VAR__p_2 ?v_146) (and (not PRED_VAR__p_2) (not ?v_146)))) (or (and PRED_VAR__p_3 ?v_145) (and ?v_274 ?v_158))) (or (and PRED_VAR__p_16 ?v_150) (and ?v_271 ?v_154))) (or (and PRED_VAR__p_11 ?v_144) (and (not PRED_VAR__p_11) (not ?v_144)))) (or (and PRED_VAR__p_8 ?v_251) (and ?v_270 (not ?v_251)))) (or (and PRED_VAR__p_9 ?v_257) (and ?v_277 (not ?v_257)))) (or (and PRED_VAR__p_14 ?v_67) (and ?v_273 ?v_153))) (or (and PRED_VAR__p_15 ?v_259) (and (not PRED_VAR__p_15) (not ?v_259)))) (or (and PRED_VAR__p_10 ?v_59) (and (not PRED_VAR__p_10) ?v_260))) (or (and PRED_VAR__p_12 ?v_262) (and (not PRED_VAR__p_12) (not ?v_262)))) (or (and PRED_VAR__p_18 ?v_263) (and ?v_268 (not ?v_263)))) (or (and PRED_VAR__p_19 ?v_143) (and ?v_267 ?v_148))) (or (and PRED_VAR__p_20 ?v_266) (and ?v_281 (not ?v_266)))))) (not (or (or (or (or (or (or (or (or (or (or (or (or (or (and ?v_267 ?v_280) (and ?v_267 ?v_282)) (and ?v_267 (and ?v_268 (and PRED_VAR__p_10 (and ?v_273 (and PRED_VAR__p_8 (and PRED_VAR__p_11 (and PRED_VAR__p_16 ?v_276)))))))) (and ?v_267 (and ?v_268 (and PRED_VAR__p_10 (and ?v_273 (and ?v_270 (and PRED_VAR__p_11 (and ?v_271 ?v_276)))))))) (and PRED_VAR__p_12 (and PRED_VAR__p_20 (and ?v_277 (and PRED_VAR__p_10 (and PRED_VAR__p_14 (and ?v_270 (and PRED_VAR__p_11 (and ?v_271 ?v_283))))))))) (and PRED_VAR__p_12 (and PRED_VAR__p_20 (and ?v_277 (and ?v_267 (and PRED_VAR__p_10 (and ?v_273 (and ?v_270 (and PRED_VAR__p_11 (and ?v_271 ?v_284)))))))))) (and PRED_VAR__p_20 (and PRED_VAR__p_9 ?v_280))) (and ?v_281 (and ?v_277 ?v_280))) (and PRED_VAR__p_20 (and PRED_VAR__p_9 ?v_282))) (and ?v_281 (and ?v_277 ?v_282))) (and PRED_VAR__p_12 (and PRED_VAR__p_20 (and PRED_VAR__p_9 ?v_286)))) (and PRED_VAR__p_12 (and PRED_VAR__p_20 (and PRED_VAR__p_9 (and ?v_267 (and ?v_268 (and PRED_VAR__p_10 (and ?v_273 (and PRED_VAR__p_8 (and PRED_VAR__p_11 (and PRED_VAR__p_16 ?v_284))))))))))) (and PRED_VAR__p_15 (and PRED_VAR__p_12 (and PRED_VAR__p_20 (and PRED_VAR__p_9 (and ?v_267 ?v_285)))))) (and PRED_VAR__p_15 (and PRED_VAR__p_12 (and PRED_VAR__p_20 (and ?v_267 ?v_286)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +(check-sat) +(exit) diff --git a/test/regress/regress1/uflia/speed2_e8_449_e8_517.ec.smt2 b/test/regress/regress1/uflia/speed2_e8_449_e8_517.ec.smt2 new file mode 100644 index 000000000..11fdfa51d --- /dev/null +++ b/test/regress/regress1/uflia/speed2_e8_449_e8_517.ec.smt2 @@ -0,0 +1,747 @@ +(set-logic QF_UFLIA) +(declare-fun _base () Int) +(declare-fun _n () Int) +(assert (let ((.def_5 (<= 0 _n))) +.def_5 +)) +(declare-fun ___z2z___ (Int) Bool) +(declare-fun ___z3z___ (Int) Bool) +(declare-fun ___z4z___ (Int) Bool) +(declare-fun ___z5z___ (Int) Bool) +(declare-fun ___z6z___ (Int) Bool) +(declare-fun ___z7z___ (Int) Int) +(declare-fun ___z8z___ (Int) Int) +(declare-fun ___z9z___ (Int) Int) +(push 1) +(assert (let ((.def_152 (___z4z___ 0))) +(let ((.def_150 (= _base 0))) +(let ((.def_147 (___z6z___ (- 1)))) +(let ((.def_148 (not .def_147))) +(let ((.def_145 (___z5z___ 0))) +(let ((.def_146 (not .def_145))) +(let ((.def_149 (and .def_146 .def_148))) +(let ((.def_151 (or .def_149 .def_150))) +(let ((.def_153 (= .def_151 .def_152))) +.def_153 +)))))))))) +(assert (let ((.def_157 (___z7z___ 0))) +(let ((.def_161 (<= .def_157 (- 10)))) +(let ((.def_155 (___z5z___ (- 1)))) +(let ((.def_162 (or .def_155 .def_161))) +(let ((.def_158 (<= 0 .def_157))) +(let ((.def_159 (not .def_158))) +(let ((.def_156 (not .def_155))) +(let ((.def_160 (or .def_156 .def_159))) +(let ((.def_163 (and .def_160 .def_162))) +(let ((.def_150 (= _base 0))) +(let ((.def_164 (or .def_150 .def_163))) +(let ((.def_154 (not .def_150))) +(let ((.def_165 (and .def_154 .def_164))) +(let ((.def_145 (___z5z___ 0))) +(let ((.def_166 (= .def_145 .def_165))) +.def_166 +)))))))))))))))) +(assert (let ((.def_175 (___z6z___ 0))) +(let ((.def_157 (___z7z___ 0))) +(let ((.def_170 (<= 10 .def_157))) +(let ((.def_147 (___z6z___ (- 1)))) +(let ((.def_171 (or .def_147 .def_170))) +(let ((.def_167 (<= .def_157 0))) +(let ((.def_168 (not .def_167))) +(let ((.def_148 (not .def_147))) +(let ((.def_169 (or .def_148 .def_168))) +(let ((.def_172 (and .def_169 .def_171))) +(let ((.def_150 (= _base 0))) +(let ((.def_173 (or .def_150 .def_172))) +(let ((.def_154 (not .def_150))) +(let ((.def_174 (and .def_154 .def_173))) +(let ((.def_176 (= .def_174 .def_175))) +.def_176 +)))))))))))))))) +(assert (let ((.def_177 (___z9z___ 0))) +(let ((.def_178 (___z8z___ 0))) +(let ((.def_179 (+ .def_177 .def_178))) +(let ((.def_181 (___z2z___ 0))) +(let ((.def_180 (___z3z___ 0))) +(let ((.def_182 (and .def_180 .def_181))) +(let ((.def_183 (ite .def_182 .def_179 .def_177))) +(let ((.def_157 (___z7z___ 0))) +(let ((.def_184 (= .def_157 .def_183))) +.def_184 +)))))))))) +(assert (let ((.def_181 (___z2z___ 0))) +(let ((.def_185 (not .def_181))) +(let ((.def_180 (___z3z___ 0))) +(let ((.def_186 (and .def_180 .def_185))) +(let ((.def_187 (ite .def_186 2 0))) +(let ((.def_188 (not .def_180))) +(let ((.def_189 (and .def_181 .def_188))) +(let ((.def_190 (ite .def_189 1 .def_187))) +(let ((.def_178 (___z8z___ 0))) +(let ((.def_191 (= .def_178 .def_190))) +.def_191 +))))))))))) +(assert (let ((.def_192 (___z7z___ (- 1)))) +(let ((.def_150 (= _base 0))) +(let ((.def_193 (ite .def_150 0 .def_192))) +(let ((.def_177 (___z9z___ 0))) +(let ((.def_194 (= .def_177 .def_193))) +.def_194 +)))))) +(assert (let ((.def_201 (___z4z___ (- 1)))) +(let ((.def_199 (= _base (- 1)))) +(let ((.def_196 (___z6z___ (- 2)))) +(let ((.def_197 (not .def_196))) +(let ((.def_155 (___z5z___ (- 1)))) +(let ((.def_156 (not .def_155))) +(let ((.def_198 (and .def_156 .def_197))) +(let ((.def_200 (or .def_198 .def_199))) +(let ((.def_202 (= .def_200 .def_201))) +.def_202 +)))))))))) +(assert (let ((.def_192 (___z7z___ (- 1)))) +(let ((.def_209 (<= .def_192 (- 10)))) +(let ((.def_204 (___z5z___ (- 2)))) +(let ((.def_210 (or .def_204 .def_209))) +(let ((.def_206 (<= 0 .def_192))) +(let ((.def_207 (not .def_206))) +(let ((.def_205 (not .def_204))) +(let ((.def_208 (or .def_205 .def_207))) +(let ((.def_211 (and .def_208 .def_210))) +(let ((.def_199 (= _base (- 1)))) +(let ((.def_212 (or .def_199 .def_211))) +(let ((.def_203 (not .def_199))) +(let ((.def_213 (and .def_203 .def_212))) +(let ((.def_155 (___z5z___ (- 1)))) +(let ((.def_214 (= .def_155 .def_213))) +.def_214 +)))))))))))))))) +(assert (let ((.def_192 (___z7z___ (- 1)))) +(let ((.def_218 (<= 10 .def_192))) +(let ((.def_196 (___z6z___ (- 2)))) +(let ((.def_219 (or .def_196 .def_218))) +(let ((.def_215 (<= .def_192 0))) +(let ((.def_216 (not .def_215))) +(let ((.def_197 (not .def_196))) +(let ((.def_217 (or .def_197 .def_216))) +(let ((.def_220 (and .def_217 .def_219))) +(let ((.def_199 (= _base (- 1)))) +(let ((.def_221 (or .def_199 .def_220))) +(let ((.def_203 (not .def_199))) +(let ((.def_222 (and .def_203 .def_221))) +(let ((.def_147 (___z6z___ (- 1)))) +(let ((.def_223 (= .def_147 .def_222))) +.def_223 +)))))))))))))))) +(assert (let ((.def_224 (___z9z___ (- 1)))) +(let ((.def_225 (___z8z___ (- 1)))) +(let ((.def_226 (+ .def_224 .def_225))) +(let ((.def_228 (___z2z___ (- 1)))) +(let ((.def_227 (___z3z___ (- 1)))) +(let ((.def_229 (and .def_227 .def_228))) +(let ((.def_230 (ite .def_229 .def_226 .def_224))) +(let ((.def_192 (___z7z___ (- 1)))) +(let ((.def_231 (= .def_192 .def_230))) +.def_231 +)))))))))) +(assert (let ((.def_228 (___z2z___ (- 1)))) +(let ((.def_232 (not .def_228))) +(let ((.def_227 (___z3z___ (- 1)))) +(let ((.def_233 (and .def_227 .def_232))) +(let ((.def_234 (ite .def_233 2 0))) +(let ((.def_235 (not .def_227))) +(let ((.def_236 (and .def_228 .def_235))) +(let ((.def_237 (ite .def_236 1 .def_234))) +(let ((.def_225 (___z8z___ (- 1)))) +(let ((.def_238 (= .def_225 .def_237))) +.def_238 +))))))))))) +(assert (let ((.def_239 (___z7z___ (- 2)))) +(let ((.def_199 (= _base (- 1)))) +(let ((.def_240 (ite .def_199 0 .def_239))) +(let ((.def_224 (___z9z___ (- 1)))) +(let ((.def_241 (= .def_224 .def_240))) +.def_241 +)))))) +(push 1) +(assert (let ((.def_201 (___z4z___ (- 1)))) +(let ((.def_152 (___z4z___ 0))) +(let ((.def_242 (and .def_152 .def_201))) +(let ((.def_199 (= _base (- 1)))) +(let ((.def_203 (not .def_199))) +(let ((.def_243 (or .def_203 .def_242))) +(let ((.def_244 (not .def_243))) +.def_244 +)))))))) +(assert true +) +(check-sat) +(pop 1) +(assert (let ((.def_201 (___z4z___ (- 1)))) +.def_201 +)) +(assert (let ((.def_245 (___z4z___ (- 2)))) +.def_245 +)) +(push 1) +(assert (let ((.def_254 (___z4z___ _n))) +(let ((.def_252 (= _n _base))) +(let ((.def_248 (+ _n (- 1)))) +(let ((.def_249 (___z6z___ .def_248))) +(let ((.def_250 (not .def_249))) +(let ((.def_246 (___z5z___ _n))) +(let ((.def_247 (not .def_246))) +(let ((.def_251 (and .def_247 .def_250))) +(let ((.def_253 (or .def_251 .def_252))) +(let ((.def_255 (= .def_253 .def_254))) +.def_255 +))))))))))) +(assert (let ((.def_259 (___z7z___ _n))) +(let ((.def_263 (<= .def_259 (- 10)))) +(let ((.def_248 (+ _n (- 1)))) +(let ((.def_257 (___z5z___ .def_248))) +(let ((.def_264 (or .def_257 .def_263))) +(let ((.def_260 (<= 0 .def_259))) +(let ((.def_261 (not .def_260))) +(let ((.def_258 (not .def_257))) +(let ((.def_262 (or .def_258 .def_261))) +(let ((.def_265 (and .def_262 .def_264))) +(let ((.def_252 (= _n _base))) +(let ((.def_266 (or .def_252 .def_265))) +(let ((.def_256 (not .def_252))) +(let ((.def_267 (and .def_256 .def_266))) +(let ((.def_246 (___z5z___ _n))) +(let ((.def_268 (= .def_246 .def_267))) +.def_268 +))))))))))))))))) +(assert (let ((.def_277 (___z6z___ _n))) +(let ((.def_259 (___z7z___ _n))) +(let ((.def_272 (<= 10 .def_259))) +(let ((.def_248 (+ _n (- 1)))) +(let ((.def_249 (___z6z___ .def_248))) +(let ((.def_273 (or .def_249 .def_272))) +(let ((.def_269 (<= .def_259 0))) +(let ((.def_270 (not .def_269))) +(let ((.def_250 (not .def_249))) +(let ((.def_271 (or .def_250 .def_270))) +(let ((.def_274 (and .def_271 .def_273))) +(let ((.def_252 (= _n _base))) +(let ((.def_275 (or .def_252 .def_274))) +(let ((.def_256 (not .def_252))) +(let ((.def_276 (and .def_256 .def_275))) +(let ((.def_278 (= .def_276 .def_277))) +.def_278 +))))))))))))))))) +(assert (let ((.def_279 (___z9z___ _n))) +(let ((.def_280 (___z8z___ _n))) +(let ((.def_281 (+ .def_279 .def_280))) +(let ((.def_283 (___z2z___ _n))) +(let ((.def_282 (___z3z___ _n))) +(let ((.def_284 (and .def_282 .def_283))) +(let ((.def_285 (ite .def_284 .def_281 .def_279))) +(let ((.def_259 (___z7z___ _n))) +(let ((.def_286 (= .def_259 .def_285))) +.def_286 +)))))))))) +(assert (let ((.def_283 (___z2z___ _n))) +(let ((.def_287 (not .def_283))) +(let ((.def_282 (___z3z___ _n))) +(let ((.def_288 (and .def_282 .def_287))) +(let ((.def_289 (ite .def_288 2 0))) +(let ((.def_290 (not .def_282))) +(let ((.def_291 (and .def_283 .def_290))) +(let ((.def_292 (ite .def_291 1 .def_289))) +(let ((.def_280 (___z8z___ _n))) +(let ((.def_293 (= .def_280 .def_292))) +.def_293 +))))))))))) +(assert (let ((.def_248 (+ _n (- 1)))) +(let ((.def_294 (___z7z___ .def_248))) +(let ((.def_252 (= _n _base))) +(let ((.def_295 (ite .def_252 0 .def_294))) +(let ((.def_279 (___z9z___ _n))) +(let ((.def_296 (= .def_279 .def_295))) +.def_296 +))))))) +(assert (let ((.def_248 (+ _n (- 1)))) +(let ((.def_305 (___z4z___ .def_248))) +(let ((.def_301 (* (- 1) _base))) +(let ((.def_302 (+ _n .def_301))) +(let ((.def_303 (= .def_302 1))) +(let ((.def_297 (+ (- 1) .def_248))) +(let ((.def_298 (___z6z___ .def_297))) +(let ((.def_299 (not .def_298))) +(let ((.def_257 (___z5z___ .def_248))) +(let ((.def_258 (not .def_257))) +(let ((.def_300 (and .def_258 .def_299))) +(let ((.def_304 (or .def_300 .def_303))) +(let ((.def_306 (= .def_304 .def_305))) +.def_306 +)))))))))))))) +(assert (let ((.def_248 (+ _n (- 1)))) +(let ((.def_294 (___z7z___ .def_248))) +(let ((.def_313 (<= .def_294 (- 10)))) +(let ((.def_297 (+ (- 1) .def_248))) +(let ((.def_308 (___z5z___ .def_297))) +(let ((.def_314 (or .def_308 .def_313))) +(let ((.def_310 (<= 0 .def_294))) +(let ((.def_311 (not .def_310))) +(let ((.def_309 (not .def_308))) +(let ((.def_312 (or .def_309 .def_311))) +(let ((.def_315 (and .def_312 .def_314))) +(let ((.def_301 (* (- 1) _base))) +(let ((.def_302 (+ _n .def_301))) +(let ((.def_303 (= .def_302 1))) +(let ((.def_316 (or .def_303 .def_315))) +(let ((.def_307 (not .def_303))) +(let ((.def_317 (and .def_307 .def_316))) +(let ((.def_257 (___z5z___ .def_248))) +(let ((.def_318 (= .def_257 .def_317))) +.def_318 +)))))))))))))))))))) +(assert (let ((.def_248 (+ _n (- 1)))) +(let ((.def_294 (___z7z___ .def_248))) +(let ((.def_322 (<= 10 .def_294))) +(let ((.def_297 (+ (- 1) .def_248))) +(let ((.def_298 (___z6z___ .def_297))) +(let ((.def_323 (or .def_298 .def_322))) +(let ((.def_319 (<= .def_294 0))) +(let ((.def_320 (not .def_319))) +(let ((.def_299 (not .def_298))) +(let ((.def_321 (or .def_299 .def_320))) +(let ((.def_324 (and .def_321 .def_323))) +(let ((.def_301 (* (- 1) _base))) +(let ((.def_302 (+ _n .def_301))) +(let ((.def_303 (= .def_302 1))) +(let ((.def_325 (or .def_303 .def_324))) +(let ((.def_307 (not .def_303))) +(let ((.def_326 (and .def_307 .def_325))) +(let ((.def_249 (___z6z___ .def_248))) +(let ((.def_327 (= .def_249 .def_326))) +.def_327 +)))))))))))))))))))) +(assert (let ((.def_248 (+ _n (- 1)))) +(let ((.def_328 (___z9z___ .def_248))) +(let ((.def_329 (___z8z___ .def_248))) +(let ((.def_330 (+ .def_328 .def_329))) +(let ((.def_332 (___z2z___ .def_248))) +(let ((.def_331 (___z3z___ .def_248))) +(let ((.def_333 (and .def_331 .def_332))) +(let ((.def_334 (ite .def_333 .def_330 .def_328))) +(let ((.def_294 (___z7z___ .def_248))) +(let ((.def_335 (= .def_294 .def_334))) +.def_335 +))))))))))) +(assert (let ((.def_248 (+ _n (- 1)))) +(let ((.def_332 (___z2z___ .def_248))) +(let ((.def_336 (not .def_332))) +(let ((.def_331 (___z3z___ .def_248))) +(let ((.def_337 (and .def_331 .def_336))) +(let ((.def_338 (ite .def_337 2 0))) +(let ((.def_339 (not .def_331))) +(let ((.def_340 (and .def_332 .def_339))) +(let ((.def_341 (ite .def_340 1 .def_338))) +(let ((.def_329 (___z8z___ .def_248))) +(let ((.def_342 (= .def_329 .def_341))) +.def_342 +)))))))))))) +(assert (let ((.def_248 (+ _n (- 1)))) +(let ((.def_297 (+ (- 1) .def_248))) +(let ((.def_343 (___z7z___ .def_297))) +(let ((.def_301 (* (- 1) _base))) +(let ((.def_302 (+ _n .def_301))) +(let ((.def_303 (= .def_302 1))) +(let ((.def_344 (ite .def_303 0 .def_343))) +(let ((.def_328 (___z9z___ .def_248))) +(let ((.def_345 (= .def_328 .def_344))) +.def_345 +)))))))))) +(assert (let ((.def_248 (+ _n (- 1)))) +(let ((.def_305 (___z4z___ .def_248))) +.def_305 +))) +(assert (let ((.def_254 (___z4z___ _n))) +(let ((.def_199 (= _base (- 1)))) +(let ((.def_203 (not .def_199))) +(let ((.def_346 (or .def_203 .def_254))) +(let ((.def_347 (not .def_346))) +.def_347 +)))))) +(assert true +) +(check-sat) +(pop 1) +(assert (let ((.def_248 (+ _n (- 1)))) +(let ((.def_305 (___z4z___ .def_248))) +.def_305 +))) +(assert (let ((.def_348 (+ _n (- 2)))) +(let ((.def_349 (___z4z___ .def_348))) +.def_349 +))) +(assert (let ((.def_354 (= _base (- 2)))) +(let ((.def_351 (___z6z___ (- 3)))) +(let ((.def_352 (not .def_351))) +(let ((.def_204 (___z5z___ (- 2)))) +(let ((.def_205 (not .def_204))) +(let ((.def_353 (and .def_205 .def_352))) +(let ((.def_355 (or .def_353 .def_354))) +(let ((.def_245 (___z4z___ (- 2)))) +(let ((.def_356 (= .def_245 .def_355))) +.def_356 +)))))))))) +(assert (let ((.def_239 (___z7z___ (- 2)))) +(let ((.def_363 (<= .def_239 (- 10)))) +(let ((.def_358 (___z5z___ (- 3)))) +(let ((.def_364 (or .def_358 .def_363))) +(let ((.def_360 (<= 0 .def_239))) +(let ((.def_361 (not .def_360))) +(let ((.def_359 (not .def_358))) +(let ((.def_362 (or .def_359 .def_361))) +(let ((.def_365 (and .def_362 .def_364))) +(let ((.def_354 (= _base (- 2)))) +(let ((.def_366 (or .def_354 .def_365))) +(let ((.def_357 (not .def_354))) +(let ((.def_367 (and .def_357 .def_366))) +(let ((.def_204 (___z5z___ (- 2)))) +(let ((.def_368 (= .def_204 .def_367))) +.def_368 +)))))))))))))))) +(assert (let ((.def_239 (___z7z___ (- 2)))) +(let ((.def_372 (<= 10 .def_239))) +(let ((.def_351 (___z6z___ (- 3)))) +(let ((.def_373 (or .def_351 .def_372))) +(let ((.def_369 (<= .def_239 0))) +(let ((.def_370 (not .def_369))) +(let ((.def_352 (not .def_351))) +(let ((.def_371 (or .def_352 .def_370))) +(let ((.def_374 (and .def_371 .def_373))) +(let ((.def_354 (= _base (- 2)))) +(let ((.def_375 (or .def_354 .def_374))) +(let ((.def_357 (not .def_354))) +(let ((.def_376 (and .def_357 .def_375))) +(let ((.def_196 (___z6z___ (- 2)))) +(let ((.def_377 (= .def_196 .def_376))) +.def_377 +)))))))))))))))) +(assert (let ((.def_378 (___z9z___ (- 2)))) +(let ((.def_379 (___z8z___ (- 2)))) +(let ((.def_380 (+ .def_378 .def_379))) +(let ((.def_382 (___z2z___ (- 2)))) +(let ((.def_381 (___z3z___ (- 2)))) +(let ((.def_383 (and .def_381 .def_382))) +(let ((.def_384 (ite .def_383 .def_380 .def_378))) +(let ((.def_239 (___z7z___ (- 2)))) +(let ((.def_385 (= .def_239 .def_384))) +.def_385 +)))))))))) +(assert (let ((.def_382 (___z2z___ (- 2)))) +(let ((.def_386 (not .def_382))) +(let ((.def_381 (___z3z___ (- 2)))) +(let ((.def_387 (and .def_381 .def_386))) +(let ((.def_388 (ite .def_387 2 0))) +(let ((.def_389 (not .def_381))) +(let ((.def_390 (and .def_382 .def_389))) +(let ((.def_391 (ite .def_390 1 .def_388))) +(let ((.def_379 (___z8z___ (- 2)))) +(let ((.def_392 (= .def_379 .def_391))) +.def_392 +))))))))))) +(assert (let ((.def_393 (___z7z___ (- 3)))) +(let ((.def_354 (= _base (- 2)))) +(let ((.def_394 (ite .def_354 0 .def_393))) +(let ((.def_378 (___z9z___ (- 2)))) +(let ((.def_395 (= .def_378 .def_394))) +.def_395 +)))))) +(assert (let ((.def_254 (___z4z___ _n))) +(let ((.def_252 (= _n _base))) +(let ((.def_248 (+ _n (- 1)))) +(let ((.def_249 (___z6z___ .def_248))) +(let ((.def_250 (not .def_249))) +(let ((.def_246 (___z5z___ _n))) +(let ((.def_247 (not .def_246))) +(let ((.def_251 (and .def_247 .def_250))) +(let ((.def_253 (or .def_251 .def_252))) +(let ((.def_255 (= .def_253 .def_254))) +.def_255 +))))))))))) +(assert (let ((.def_259 (___z7z___ _n))) +(let ((.def_263 (<= .def_259 (- 10)))) +(let ((.def_248 (+ _n (- 1)))) +(let ((.def_257 (___z5z___ .def_248))) +(let ((.def_264 (or .def_257 .def_263))) +(let ((.def_260 (<= 0 .def_259))) +(let ((.def_261 (not .def_260))) +(let ((.def_258 (not .def_257))) +(let ((.def_262 (or .def_258 .def_261))) +(let ((.def_265 (and .def_262 .def_264))) +(let ((.def_252 (= _n _base))) +(let ((.def_266 (or .def_252 .def_265))) +(let ((.def_256 (not .def_252))) +(let ((.def_267 (and .def_256 .def_266))) +(let ((.def_246 (___z5z___ _n))) +(let ((.def_268 (= .def_246 .def_267))) +.def_268 +))))))))))))))))) +(assert (let ((.def_277 (___z6z___ _n))) +(let ((.def_259 (___z7z___ _n))) +(let ((.def_272 (<= 10 .def_259))) +(let ((.def_248 (+ _n (- 1)))) +(let ((.def_249 (___z6z___ .def_248))) +(let ((.def_273 (or .def_249 .def_272))) +(let ((.def_269 (<= .def_259 0))) +(let ((.def_270 (not .def_269))) +(let ((.def_250 (not .def_249))) +(let ((.def_271 (or .def_250 .def_270))) +(let ((.def_274 (and .def_271 .def_273))) +(let ((.def_252 (= _n _base))) +(let ((.def_275 (or .def_252 .def_274))) +(let ((.def_256 (not .def_252))) +(let ((.def_276 (and .def_256 .def_275))) +(let ((.def_278 (= .def_276 .def_277))) +.def_278 +))))))))))))))))) +(assert (let ((.def_279 (___z9z___ _n))) +(let ((.def_280 (___z8z___ _n))) +(let ((.def_281 (+ .def_279 .def_280))) +(let ((.def_283 (___z2z___ _n))) +(let ((.def_282 (___z3z___ _n))) +(let ((.def_284 (and .def_282 .def_283))) +(let ((.def_285 (ite .def_284 .def_281 .def_279))) +(let ((.def_259 (___z7z___ _n))) +(let ((.def_286 (= .def_259 .def_285))) +.def_286 +)))))))))) +(assert (let ((.def_283 (___z2z___ _n))) +(let ((.def_287 (not .def_283))) +(let ((.def_282 (___z3z___ _n))) +(let ((.def_288 (and .def_282 .def_287))) +(let ((.def_289 (ite .def_288 2 0))) +(let ((.def_290 (not .def_282))) +(let ((.def_291 (and .def_283 .def_290))) +(let ((.def_292 (ite .def_291 1 .def_289))) +(let ((.def_280 (___z8z___ _n))) +(let ((.def_293 (= .def_280 .def_292))) +.def_293 +))))))))))) +(assert (let ((.def_248 (+ _n (- 1)))) +(let ((.def_294 (___z7z___ .def_248))) +(let ((.def_252 (= _n _base))) +(let ((.def_295 (ite .def_252 0 .def_294))) +(let ((.def_279 (___z9z___ _n))) +(let ((.def_296 (= .def_279 .def_295))) +.def_296 +))))))) +(push 1) +(assert (let ((.def_354 (= _base (- 2)))) +(let ((.def_357 (not .def_354))) +(let ((.def_152 (___z4z___ 0))) +(let ((.def_396 (or .def_152 .def_357))) +(let ((.def_397 (not .def_396))) +.def_397 +)))))) +(assert true +) +(check-sat) +(pop 1) +(assert (let ((.def_399 (___z4z___ (- 3)))) +.def_399 +)) +(push 1) +(assert (let ((.def_248 (+ _n (- 1)))) +(let ((.def_305 (___z4z___ .def_248))) +(let ((.def_301 (* (- 1) _base))) +(let ((.def_302 (+ _n .def_301))) +(let ((.def_303 (= .def_302 1))) +(let ((.def_297 (+ (- 1) .def_248))) +(let ((.def_298 (___z6z___ .def_297))) +(let ((.def_299 (not .def_298))) +(let ((.def_257 (___z5z___ .def_248))) +(let ((.def_258 (not .def_257))) +(let ((.def_300 (and .def_258 .def_299))) +(let ((.def_304 (or .def_300 .def_303))) +(let ((.def_306 (= .def_304 .def_305))) +.def_306 +)))))))))))))) +(assert (let ((.def_248 (+ _n (- 1)))) +(let ((.def_294 (___z7z___ .def_248))) +(let ((.def_313 (<= .def_294 (- 10)))) +(let ((.def_297 (+ (- 1) .def_248))) +(let ((.def_308 (___z5z___ .def_297))) +(let ((.def_314 (or .def_308 .def_313))) +(let ((.def_310 (<= 0 .def_294))) +(let ((.def_311 (not .def_310))) +(let ((.def_309 (not .def_308))) +(let ((.def_312 (or .def_309 .def_311))) +(let ((.def_315 (and .def_312 .def_314))) +(let ((.def_301 (* (- 1) _base))) +(let ((.def_302 (+ _n .def_301))) +(let ((.def_303 (= .def_302 1))) +(let ((.def_316 (or .def_303 .def_315))) +(let ((.def_307 (not .def_303))) +(let ((.def_317 (and .def_307 .def_316))) +(let ((.def_257 (___z5z___ .def_248))) +(let ((.def_318 (= .def_257 .def_317))) +.def_318 +)))))))))))))))))))) +(assert (let ((.def_248 (+ _n (- 1)))) +(let ((.def_294 (___z7z___ .def_248))) +(let ((.def_322 (<= 10 .def_294))) +(let ((.def_297 (+ (- 1) .def_248))) +(let ((.def_298 (___z6z___ .def_297))) +(let ((.def_323 (or .def_298 .def_322))) +(let ((.def_319 (<= .def_294 0))) +(let ((.def_320 (not .def_319))) +(let ((.def_299 (not .def_298))) +(let ((.def_321 (or .def_299 .def_320))) +(let ((.def_324 (and .def_321 .def_323))) +(let ((.def_301 (* (- 1) _base))) +(let ((.def_302 (+ _n .def_301))) +(let ((.def_303 (= .def_302 1))) +(let ((.def_325 (or .def_303 .def_324))) +(let ((.def_307 (not .def_303))) +(let ((.def_326 (and .def_307 .def_325))) +(let ((.def_249 (___z6z___ .def_248))) +(let ((.def_327 (= .def_249 .def_326))) +.def_327 +)))))))))))))))))))) +(assert (let ((.def_248 (+ _n (- 1)))) +(let ((.def_328 (___z9z___ .def_248))) +(let ((.def_329 (___z8z___ .def_248))) +(let ((.def_330 (+ .def_328 .def_329))) +(let ((.def_332 (___z2z___ .def_248))) +(let ((.def_331 (___z3z___ .def_248))) +(let ((.def_333 (and .def_331 .def_332))) +(let ((.def_334 (ite .def_333 .def_330 .def_328))) +(let ((.def_294 (___z7z___ .def_248))) +(let ((.def_335 (= .def_294 .def_334))) +.def_335 +))))))))))) +(assert (let ((.def_248 (+ _n (- 1)))) +(let ((.def_332 (___z2z___ .def_248))) +(let ((.def_336 (not .def_332))) +(let ((.def_331 (___z3z___ .def_248))) +(let ((.def_337 (and .def_331 .def_336))) +(let ((.def_338 (ite .def_337 2 0))) +(let ((.def_339 (not .def_331))) +(let ((.def_340 (and .def_332 .def_339))) +(let ((.def_341 (ite .def_340 1 .def_338))) +(let ((.def_329 (___z8z___ .def_248))) +(let ((.def_342 (= .def_329 .def_341))) +.def_342 +)))))))))))) +(assert (let ((.def_248 (+ _n (- 1)))) +(let ((.def_297 (+ (- 1) .def_248))) +(let ((.def_343 (___z7z___ .def_297))) +(let ((.def_301 (* (- 1) _base))) +(let ((.def_302 (+ _n .def_301))) +(let ((.def_303 (= .def_302 1))) +(let ((.def_344 (ite .def_303 0 .def_343))) +(let ((.def_328 (___z9z___ .def_248))) +(let ((.def_345 (= .def_328 .def_344))) +.def_345 +)))))))))) +(assert (let ((.def_301 (* (- 1) _base))) +(let ((.def_302 (+ _n .def_301))) +(let ((.def_406 (= .def_302 2))) +(let ((.def_348 (+ _n (- 2)))) +(let ((.def_402 (+ (- 1) .def_348))) +(let ((.def_403 (___z6z___ .def_402))) +(let ((.def_404 (not .def_403))) +(let ((.def_400 (___z5z___ .def_348))) +(let ((.def_401 (not .def_400))) +(let ((.def_405 (and .def_401 .def_404))) +(let ((.def_407 (or .def_405 .def_406))) +(let ((.def_349 (___z4z___ .def_348))) +(let ((.def_408 (= .def_349 .def_407))) +.def_408 +)))))))))))))) +(assert (let ((.def_348 (+ _n (- 2)))) +(let ((.def_412 (___z7z___ .def_348))) +(let ((.def_416 (<= .def_412 (- 10)))) +(let ((.def_402 (+ (- 1) .def_348))) +(let ((.def_410 (___z5z___ .def_402))) +(let ((.def_417 (or .def_410 .def_416))) +(let ((.def_413 (<= 0 .def_412))) +(let ((.def_414 (not .def_413))) +(let ((.def_411 (not .def_410))) +(let ((.def_415 (or .def_411 .def_414))) +(let ((.def_418 (and .def_415 .def_417))) +(let ((.def_301 (* (- 1) _base))) +(let ((.def_302 (+ _n .def_301))) +(let ((.def_406 (= .def_302 2))) +(let ((.def_419 (or .def_406 .def_418))) +(let ((.def_409 (not .def_406))) +(let ((.def_420 (and .def_409 .def_419))) +(let ((.def_400 (___z5z___ .def_348))) +(let ((.def_421 (= .def_400 .def_420))) +.def_421 +)))))))))))))))))))) +(assert (let ((.def_348 (+ _n (- 2)))) +(let ((.def_430 (___z6z___ .def_348))) +(let ((.def_412 (___z7z___ .def_348))) +(let ((.def_425 (<= 10 .def_412))) +(let ((.def_402 (+ (- 1) .def_348))) +(let ((.def_403 (___z6z___ .def_402))) +(let ((.def_426 (or .def_403 .def_425))) +(let ((.def_422 (<= .def_412 0))) +(let ((.def_423 (not .def_422))) +(let ((.def_404 (not .def_403))) +(let ((.def_424 (or .def_404 .def_423))) +(let ((.def_427 (and .def_424 .def_426))) +(let ((.def_301 (* (- 1) _base))) +(let ((.def_302 (+ _n .def_301))) +(let ((.def_406 (= .def_302 2))) +(let ((.def_428 (or .def_406 .def_427))) +(let ((.def_409 (not .def_406))) +(let ((.def_429 (and .def_409 .def_428))) +(let ((.def_431 (= .def_429 .def_430))) +.def_431 +)))))))))))))))))))) +(assert (let ((.def_348 (+ _n (- 2)))) +(let ((.def_432 (___z9z___ .def_348))) +(let ((.def_433 (___z8z___ .def_348))) +(let ((.def_434 (+ .def_432 .def_433))) +(let ((.def_436 (___z2z___ .def_348))) +(let ((.def_435 (___z3z___ .def_348))) +(let ((.def_437 (and .def_435 .def_436))) +(let ((.def_438 (ite .def_437 .def_434 .def_432))) +(let ((.def_412 (___z7z___ .def_348))) +(let ((.def_439 (= .def_412 .def_438))) +.def_439 +))))))))))) +(assert (let ((.def_348 (+ _n (- 2)))) +(let ((.def_436 (___z2z___ .def_348))) +(let ((.def_440 (not .def_436))) +(let ((.def_435 (___z3z___ .def_348))) +(let ((.def_441 (and .def_435 .def_440))) +(let ((.def_442 (ite .def_441 2 0))) +(let ((.def_443 (not .def_435))) +(let ((.def_444 (and .def_436 .def_443))) +(let ((.def_445 (ite .def_444 1 .def_442))) +(let ((.def_433 (___z8z___ .def_348))) +(let ((.def_446 (= .def_433 .def_445))) +.def_446 +)))))))))))) +(assert (let ((.def_348 (+ _n (- 2)))) +(let ((.def_402 (+ (- 1) .def_348))) +(let ((.def_447 (___z7z___ .def_402))) +(let ((.def_301 (* (- 1) _base))) +(let ((.def_302 (+ _n .def_301))) +(let ((.def_406 (= .def_302 2))) +(let ((.def_448 (ite .def_406 0 .def_447))) +(let ((.def_432 (___z9z___ .def_348))) +(let ((.def_449 (= .def_432 .def_448))) +.def_449 +)))))))))) +(assert (let ((.def_354 (= _base (- 2)))) +(let ((.def_357 (not .def_354))) +(let ((.def_254 (___z4z___ _n))) +(let ((.def_450 (or .def_254 .def_357))) +(let ((.def_451 (not .def_450))) +.def_451 +)))))) +(assert true +) +(check-sat) diff --git a/test/regress/regress1/uflia/speed2_e8_449_e8_517.ec.smt2.expect b/test/regress/regress1/uflia/speed2_e8_449_e8_517.ec.smt2.expect new file mode 100644 index 000000000..65fb9b33f --- /dev/null +++ b/test/regress/regress1/uflia/speed2_e8_449_e8_517.ec.smt2.expect @@ -0,0 +1,5 @@ +% COMMAND-LINE: --incremental +% EXPECT: unsat +% EXPECT: sat +% EXPECT: unsat +% EXPECT: unsat diff --git a/test/regress/regress1/uflia/stalmark_e7_27_e7_31.ec.smt2 b/test/regress/regress1/uflia/stalmark_e7_27_e7_31.ec.smt2 new file mode 100644 index 000000000..381eb740b --- /dev/null +++ b/test/regress/regress1/uflia/stalmark_e7_27_e7_31.ec.smt2 @@ -0,0 +1,772 @@ +(set-logic QF_UFLIA) +(declare-fun _base () Int) +(declare-fun _n () Int) +(assert (let ((.def_5 (<= 0 _n))) +.def_5 +)) +(declare-fun ___z3z___ (Int) Bool) +(declare-fun ___z4z___ (Int) Bool) +(declare-fun ___z5z___ (Int) Bool) +(declare-fun ___z6z___ (Int) Bool) +(push 1) +(assert (let ((.def_117 (___z3z___ 0))) +(let ((.def_99 (___z4z___ 0))) +(let ((.def_108 (not .def_99))) +(let ((.def_98 (___z5z___ 0))) +(let ((.def_104 (not .def_98))) +(let ((.def_111 (or .def_104 .def_108))) +(let ((.def_101 (___z6z___ 0))) +(let ((.def_112 (or .def_101 .def_111))) +(let ((.def_109 (and .def_98 .def_108))) +(let ((.def_106 (not .def_101))) +(let ((.def_110 (and .def_106 .def_109))) +(let ((.def_113 (or .def_110 .def_112))) +(let ((.def_105 (and .def_99 .def_104))) +(let ((.def_107 (and .def_105 .def_106))) +(let ((.def_114 (or .def_107 .def_113))) +(let ((.def_100 (and .def_98 .def_99))) +(let ((.def_102 (and .def_100 .def_101))) +(let ((.def_115 (or .def_102 .def_114))) +(let ((.def_103 (not .def_102))) +(let ((.def_116 (and .def_103 .def_115))) +(let ((.def_118 (= .def_116 .def_117))) +.def_118 +)))))))))))))))))))))) +(assert (let ((.def_120 (= _base 0))) +(let ((.def_119 (___z6z___ (- 1)))) +(let ((.def_121 (or .def_119 .def_120))) +(let ((.def_99 (___z4z___ 0))) +(let ((.def_122 (= .def_99 .def_121))) +.def_122 +)))))) +(assert (let ((.def_124 (___z4z___ (- 1)))) +(let ((.def_120 (= _base 0))) +(let ((.def_125 (or .def_120 .def_124))) +(let ((.def_123 (not .def_120))) +(let ((.def_126 (and .def_123 .def_125))) +(let ((.def_98 (___z5z___ 0))) +(let ((.def_127 (= .def_98 .def_126))) +.def_127 +)))))))) +(assert (let ((.def_128 (___z5z___ (- 1)))) +(let ((.def_120 (= _base 0))) +(let ((.def_129 (or .def_120 .def_128))) +(let ((.def_123 (not .def_120))) +(let ((.def_130 (and .def_123 .def_129))) +(let ((.def_101 (___z6z___ 0))) +(let ((.def_131 (= .def_101 .def_130))) +.def_131 +)))))))) +(assert (let ((.def_148 (___z3z___ (- 1)))) +(let ((.def_124 (___z4z___ (- 1)))) +(let ((.def_139 (not .def_124))) +(let ((.def_128 (___z5z___ (- 1)))) +(let ((.def_135 (not .def_128))) +(let ((.def_142 (or .def_135 .def_139))) +(let ((.def_119 (___z6z___ (- 1)))) +(let ((.def_143 (or .def_119 .def_142))) +(let ((.def_140 (and .def_128 .def_139))) +(let ((.def_137 (not .def_119))) +(let ((.def_141 (and .def_137 .def_140))) +(let ((.def_144 (or .def_141 .def_143))) +(let ((.def_136 (and .def_124 .def_135))) +(let ((.def_138 (and .def_136 .def_137))) +(let ((.def_145 (or .def_138 .def_144))) +(let ((.def_132 (and .def_124 .def_128))) +(let ((.def_133 (and .def_119 .def_132))) +(let ((.def_146 (or .def_133 .def_145))) +(let ((.def_134 (not .def_133))) +(let ((.def_147 (and .def_134 .def_146))) +(let ((.def_149 (= .def_147 .def_148))) +.def_149 +)))))))))))))))))))))) +(assert (let ((.def_152 (= _base (- 1)))) +(let ((.def_151 (___z6z___ (- 2)))) +(let ((.def_153 (or .def_151 .def_152))) +(let ((.def_124 (___z4z___ (- 1)))) +(let ((.def_154 (= .def_124 .def_153))) +.def_154 +)))))) +(assert (let ((.def_156 (___z4z___ (- 2)))) +(let ((.def_152 (= _base (- 1)))) +(let ((.def_157 (or .def_152 .def_156))) +(let ((.def_155 (not .def_152))) +(let ((.def_158 (and .def_155 .def_157))) +(let ((.def_128 (___z5z___ (- 1)))) +(let ((.def_159 (= .def_128 .def_158))) +.def_159 +)))))))) +(assert (let ((.def_160 (___z5z___ (- 2)))) +(let ((.def_152 (= _base (- 1)))) +(let ((.def_161 (or .def_152 .def_160))) +(let ((.def_155 (not .def_152))) +(let ((.def_162 (and .def_155 .def_161))) +(let ((.def_119 (___z6z___ (- 1)))) +(let ((.def_163 (= .def_119 .def_162))) +.def_163 +)))))))) +(push 1) +(assert (let ((.def_148 (___z3z___ (- 1)))) +(let ((.def_117 (___z3z___ 0))) +(let ((.def_164 (and .def_117 .def_148))) +(let ((.def_152 (= _base (- 1)))) +(let ((.def_155 (not .def_152))) +(let ((.def_165 (or .def_155 .def_164))) +(let ((.def_166 (not .def_165))) +.def_166 +)))))))) +(assert true +) +(check-sat) +(pop 1) +(assert (let ((.def_148 (___z3z___ (- 1)))) +.def_148 +)) +(assert (let ((.def_168 (___z3z___ (- 2)))) +.def_168 +)) +(push 1) +(assert (let ((.def_188 (___z3z___ _n))) +(let ((.def_170 (___z4z___ _n))) +(let ((.def_179 (not .def_170))) +(let ((.def_169 (___z5z___ _n))) +(let ((.def_175 (not .def_169))) +(let ((.def_182 (or .def_175 .def_179))) +(let ((.def_172 (___z6z___ _n))) +(let ((.def_183 (or .def_172 .def_182))) +(let ((.def_180 (and .def_169 .def_179))) +(let ((.def_177 (not .def_172))) +(let ((.def_181 (and .def_177 .def_180))) +(let ((.def_184 (or .def_181 .def_183))) +(let ((.def_176 (and .def_170 .def_175))) +(let ((.def_178 (and .def_176 .def_177))) +(let ((.def_185 (or .def_178 .def_184))) +(let ((.def_171 (and .def_169 .def_170))) +(let ((.def_173 (and .def_171 .def_172))) +(let ((.def_186 (or .def_173 .def_185))) +(let ((.def_174 (not .def_173))) +(let ((.def_187 (and .def_174 .def_186))) +(let ((.def_189 (= .def_187 .def_188))) +.def_189 +)))))))))))))))))))))) +(assert (let ((.def_192 (= _n _base))) +(let ((.def_190 (+ _n (- 1)))) +(let ((.def_191 (___z6z___ .def_190))) +(let ((.def_193 (or .def_191 .def_192))) +(let ((.def_170 (___z4z___ _n))) +(let ((.def_194 (= .def_170 .def_193))) +.def_194 +))))))) +(assert (let ((.def_190 (+ _n (- 1)))) +(let ((.def_196 (___z4z___ .def_190))) +(let ((.def_192 (= _n _base))) +(let ((.def_197 (or .def_192 .def_196))) +(let ((.def_195 (not .def_192))) +(let ((.def_198 (and .def_195 .def_197))) +(let ((.def_169 (___z5z___ _n))) +(let ((.def_199 (= .def_169 .def_198))) +.def_199 +))))))))) +(assert (let ((.def_190 (+ _n (- 1)))) +(let ((.def_200 (___z5z___ .def_190))) +(let ((.def_192 (= _n _base))) +(let ((.def_201 (or .def_192 .def_200))) +(let ((.def_195 (not .def_192))) +(let ((.def_202 (and .def_195 .def_201))) +(let ((.def_172 (___z6z___ _n))) +(let ((.def_203 (= .def_172 .def_202))) +.def_203 +))))))))) +(assert (let ((.def_190 (+ _n (- 1)))) +(let ((.def_220 (___z3z___ .def_190))) +(let ((.def_196 (___z4z___ .def_190))) +(let ((.def_211 (not .def_196))) +(let ((.def_200 (___z5z___ .def_190))) +(let ((.def_207 (not .def_200))) +(let ((.def_214 (or .def_207 .def_211))) +(let ((.def_191 (___z6z___ .def_190))) +(let ((.def_215 (or .def_191 .def_214))) +(let ((.def_212 (and .def_200 .def_211))) +(let ((.def_209 (not .def_191))) +(let ((.def_213 (and .def_209 .def_212))) +(let ((.def_216 (or .def_213 .def_215))) +(let ((.def_208 (and .def_196 .def_207))) +(let ((.def_210 (and .def_208 .def_209))) +(let ((.def_217 (or .def_210 .def_216))) +(let ((.def_204 (and .def_196 .def_200))) +(let ((.def_205 (and .def_191 .def_204))) +(let ((.def_218 (or .def_205 .def_217))) +(let ((.def_206 (not .def_205))) +(let ((.def_219 (and .def_206 .def_218))) +(let ((.def_221 (= .def_219 .def_220))) +.def_221 +))))))))))))))))))))))) +(assert (let ((.def_224 (* (- 1) _base))) +(let ((.def_225 (+ _n .def_224))) +(let ((.def_226 (= .def_225 1))) +(let ((.def_190 (+ _n (- 1)))) +(let ((.def_222 (+ (- 1) .def_190))) +(let ((.def_223 (___z6z___ .def_222))) +(let ((.def_227 (or .def_223 .def_226))) +(let ((.def_196 (___z4z___ .def_190))) +(let ((.def_228 (= .def_196 .def_227))) +.def_228 +)))))))))) +(assert (let ((.def_190 (+ _n (- 1)))) +(let ((.def_222 (+ (- 1) .def_190))) +(let ((.def_230 (___z4z___ .def_222))) +(let ((.def_224 (* (- 1) _base))) +(let ((.def_225 (+ _n .def_224))) +(let ((.def_226 (= .def_225 1))) +(let ((.def_231 (or .def_226 .def_230))) +(let ((.def_229 (not .def_226))) +(let ((.def_232 (and .def_229 .def_231))) +(let ((.def_200 (___z5z___ .def_190))) +(let ((.def_233 (= .def_200 .def_232))) +.def_233 +)))))))))))) +(assert (let ((.def_190 (+ _n (- 1)))) +(let ((.def_222 (+ (- 1) .def_190))) +(let ((.def_234 (___z5z___ .def_222))) +(let ((.def_224 (* (- 1) _base))) +(let ((.def_225 (+ _n .def_224))) +(let ((.def_226 (= .def_225 1))) +(let ((.def_235 (or .def_226 .def_234))) +(let ((.def_229 (not .def_226))) +(let ((.def_236 (and .def_229 .def_235))) +(let ((.def_191 (___z6z___ .def_190))) +(let ((.def_237 (= .def_191 .def_236))) +.def_237 +)))))))))))) +(assert (let ((.def_190 (+ _n (- 1)))) +(let ((.def_220 (___z3z___ .def_190))) +.def_220 +))) +(assert (let ((.def_188 (___z3z___ _n))) +(let ((.def_152 (= _base (- 1)))) +(let ((.def_155 (not .def_152))) +(let ((.def_238 (or .def_155 .def_188))) +(let ((.def_239 (not .def_238))) +.def_239 +)))))) +(assert true +) +(check-sat) +(pop 1) +(assert (let ((.def_190 (+ _n (- 1)))) +(let ((.def_220 (___z3z___ .def_190))) +.def_220 +))) +(assert (let ((.def_240 (+ _n (- 2)))) +(let ((.def_241 (___z3z___ .def_240))) +.def_241 +))) +(assert (let ((.def_156 (___z4z___ (- 2)))) +(let ((.def_249 (not .def_156))) +(let ((.def_160 (___z5z___ (- 2)))) +(let ((.def_245 (not .def_160))) +(let ((.def_252 (or .def_245 .def_249))) +(let ((.def_151 (___z6z___ (- 2)))) +(let ((.def_253 (or .def_151 .def_252))) +(let ((.def_250 (and .def_160 .def_249))) +(let ((.def_247 (not .def_151))) +(let ((.def_251 (and .def_247 .def_250))) +(let ((.def_254 (or .def_251 .def_253))) +(let ((.def_246 (and .def_156 .def_245))) +(let ((.def_248 (and .def_246 .def_247))) +(let ((.def_255 (or .def_248 .def_254))) +(let ((.def_242 (and .def_156 .def_160))) +(let ((.def_243 (and .def_151 .def_242))) +(let ((.def_256 (or .def_243 .def_255))) +(let ((.def_244 (not .def_243))) +(let ((.def_257 (and .def_244 .def_256))) +(let ((.def_168 (___z3z___ (- 2)))) +(let ((.def_258 (= .def_168 .def_257))) +.def_258 +)))))))))))))))))))))) +(assert (let ((.def_261 (= _base (- 2)))) +(let ((.def_260 (___z6z___ (- 3)))) +(let ((.def_262 (or .def_260 .def_261))) +(let ((.def_156 (___z4z___ (- 2)))) +(let ((.def_263 (= .def_156 .def_262))) +.def_263 +)))))) +(assert (let ((.def_265 (___z4z___ (- 3)))) +(let ((.def_261 (= _base (- 2)))) +(let ((.def_266 (or .def_261 .def_265))) +(let ((.def_264 (not .def_261))) +(let ((.def_267 (and .def_264 .def_266))) +(let ((.def_160 (___z5z___ (- 2)))) +(let ((.def_268 (= .def_160 .def_267))) +.def_268 +)))))))) +(assert (let ((.def_269 (___z5z___ (- 3)))) +(let ((.def_261 (= _base (- 2)))) +(let ((.def_270 (or .def_261 .def_269))) +(let ((.def_264 (not .def_261))) +(let ((.def_271 (and .def_264 .def_270))) +(let ((.def_151 (___z6z___ (- 2)))) +(let ((.def_272 (= .def_151 .def_271))) +.def_272 +)))))))) +(assert (let ((.def_188 (___z3z___ _n))) +(let ((.def_170 (___z4z___ _n))) +(let ((.def_179 (not .def_170))) +(let ((.def_169 (___z5z___ _n))) +(let ((.def_175 (not .def_169))) +(let ((.def_182 (or .def_175 .def_179))) +(let ((.def_172 (___z6z___ _n))) +(let ((.def_183 (or .def_172 .def_182))) +(let ((.def_180 (and .def_169 .def_179))) +(let ((.def_177 (not .def_172))) +(let ((.def_181 (and .def_177 .def_180))) +(let ((.def_184 (or .def_181 .def_183))) +(let ((.def_176 (and .def_170 .def_175))) +(let ((.def_178 (and .def_176 .def_177))) +(let ((.def_185 (or .def_178 .def_184))) +(let ((.def_171 (and .def_169 .def_170))) +(let ((.def_173 (and .def_171 .def_172))) +(let ((.def_186 (or .def_173 .def_185))) +(let ((.def_174 (not .def_173))) +(let ((.def_187 (and .def_174 .def_186))) +(let ((.def_189 (= .def_187 .def_188))) +.def_189 +)))))))))))))))))))))) +(assert (let ((.def_192 (= _n _base))) +(let ((.def_190 (+ _n (- 1)))) +(let ((.def_191 (___z6z___ .def_190))) +(let ((.def_193 (or .def_191 .def_192))) +(let ((.def_170 (___z4z___ _n))) +(let ((.def_194 (= .def_170 .def_193))) +.def_194 +))))))) +(assert (let ((.def_190 (+ _n (- 1)))) +(let ((.def_196 (___z4z___ .def_190))) +(let ((.def_192 (= _n _base))) +(let ((.def_197 (or .def_192 .def_196))) +(let ((.def_195 (not .def_192))) +(let ((.def_198 (and .def_195 .def_197))) +(let ((.def_169 (___z5z___ _n))) +(let ((.def_199 (= .def_169 .def_198))) +.def_199 +))))))))) +(assert (let ((.def_190 (+ _n (- 1)))) +(let ((.def_200 (___z5z___ .def_190))) +(let ((.def_192 (= _n _base))) +(let ((.def_201 (or .def_192 .def_200))) +(let ((.def_195 (not .def_192))) +(let ((.def_202 (and .def_195 .def_201))) +(let ((.def_172 (___z6z___ _n))) +(let ((.def_203 (= .def_172 .def_202))) +.def_203 +))))))))) +(push 1) +(assert (let ((.def_261 (= _base (- 2)))) +(let ((.def_264 (not .def_261))) +(let ((.def_117 (___z3z___ 0))) +(let ((.def_273 (or .def_117 .def_264))) +(let ((.def_274 (not .def_273))) +.def_274 +)))))) +(assert true +) +(check-sat) +(pop 1) +(assert (let ((.def_276 (___z3z___ (- 3)))) +.def_276 +)) +(push 1) +(assert (let ((.def_190 (+ _n (- 1)))) +(let ((.def_220 (___z3z___ .def_190))) +(let ((.def_196 (___z4z___ .def_190))) +(let ((.def_211 (not .def_196))) +(let ((.def_200 (___z5z___ .def_190))) +(let ((.def_207 (not .def_200))) +(let ((.def_214 (or .def_207 .def_211))) +(let ((.def_191 (___z6z___ .def_190))) +(let ((.def_215 (or .def_191 .def_214))) +(let ((.def_212 (and .def_200 .def_211))) +(let ((.def_209 (not .def_191))) +(let ((.def_213 (and .def_209 .def_212))) +(let ((.def_216 (or .def_213 .def_215))) +(let ((.def_208 (and .def_196 .def_207))) +(let ((.def_210 (and .def_208 .def_209))) +(let ((.def_217 (or .def_210 .def_216))) +(let ((.def_204 (and .def_196 .def_200))) +(let ((.def_205 (and .def_191 .def_204))) +(let ((.def_218 (or .def_205 .def_217))) +(let ((.def_206 (not .def_205))) +(let ((.def_219 (and .def_206 .def_218))) +(let ((.def_221 (= .def_219 .def_220))) +.def_221 +))))))))))))))))))))))) +(assert (let ((.def_224 (* (- 1) _base))) +(let ((.def_225 (+ _n .def_224))) +(let ((.def_226 (= .def_225 1))) +(let ((.def_190 (+ _n (- 1)))) +(let ((.def_222 (+ (- 1) .def_190))) +(let ((.def_223 (___z6z___ .def_222))) +(let ((.def_227 (or .def_223 .def_226))) +(let ((.def_196 (___z4z___ .def_190))) +(let ((.def_228 (= .def_196 .def_227))) +.def_228 +)))))))))) +(assert (let ((.def_190 (+ _n (- 1)))) +(let ((.def_222 (+ (- 1) .def_190))) +(let ((.def_230 (___z4z___ .def_222))) +(let ((.def_224 (* (- 1) _base))) +(let ((.def_225 (+ _n .def_224))) +(let ((.def_226 (= .def_225 1))) +(let ((.def_231 (or .def_226 .def_230))) +(let ((.def_229 (not .def_226))) +(let ((.def_232 (and .def_229 .def_231))) +(let ((.def_200 (___z5z___ .def_190))) +(let ((.def_233 (= .def_200 .def_232))) +.def_233 +)))))))))))) +(assert (let ((.def_190 (+ _n (- 1)))) +(let ((.def_222 (+ (- 1) .def_190))) +(let ((.def_234 (___z5z___ .def_222))) +(let ((.def_224 (* (- 1) _base))) +(let ((.def_225 (+ _n .def_224))) +(let ((.def_226 (= .def_225 1))) +(let ((.def_235 (or .def_226 .def_234))) +(let ((.def_229 (not .def_226))) +(let ((.def_236 (and .def_229 .def_235))) +(let ((.def_191 (___z6z___ .def_190))) +(let ((.def_237 (= .def_191 .def_236))) +.def_237 +)))))))))))) +(assert (let ((.def_240 (+ _n (- 2)))) +(let ((.def_278 (___z4z___ .def_240))) +(let ((.def_287 (not .def_278))) +(let ((.def_277 (___z5z___ .def_240))) +(let ((.def_283 (not .def_277))) +(let ((.def_290 (or .def_283 .def_287))) +(let ((.def_280 (___z6z___ .def_240))) +(let ((.def_291 (or .def_280 .def_290))) +(let ((.def_288 (and .def_277 .def_287))) +(let ((.def_285 (not .def_280))) +(let ((.def_289 (and .def_285 .def_288))) +(let ((.def_292 (or .def_289 .def_291))) +(let ((.def_284 (and .def_278 .def_283))) +(let ((.def_286 (and .def_284 .def_285))) +(let ((.def_293 (or .def_286 .def_292))) +(let ((.def_279 (and .def_277 .def_278))) +(let ((.def_281 (and .def_279 .def_280))) +(let ((.def_294 (or .def_281 .def_293))) +(let ((.def_282 (not .def_281))) +(let ((.def_295 (and .def_282 .def_294))) +(let ((.def_241 (___z3z___ .def_240))) +(let ((.def_296 (= .def_241 .def_295))) +.def_296 +))))))))))))))))))))))) +(assert (let ((.def_224 (* (- 1) _base))) +(let ((.def_225 (+ _n .def_224))) +(let ((.def_299 (= .def_225 2))) +(let ((.def_240 (+ _n (- 2)))) +(let ((.def_297 (+ (- 1) .def_240))) +(let ((.def_298 (___z6z___ .def_297))) +(let ((.def_300 (or .def_298 .def_299))) +(let ((.def_278 (___z4z___ .def_240))) +(let ((.def_301 (= .def_278 .def_300))) +.def_301 +)))))))))) +(assert (let ((.def_240 (+ _n (- 2)))) +(let ((.def_297 (+ (- 1) .def_240))) +(let ((.def_303 (___z4z___ .def_297))) +(let ((.def_224 (* (- 1) _base))) +(let ((.def_225 (+ _n .def_224))) +(let ((.def_299 (= .def_225 2))) +(let ((.def_304 (or .def_299 .def_303))) +(let ((.def_302 (not .def_299))) +(let ((.def_305 (and .def_302 .def_304))) +(let ((.def_277 (___z5z___ .def_240))) +(let ((.def_306 (= .def_277 .def_305))) +.def_306 +)))))))))))) +(assert (let ((.def_240 (+ _n (- 2)))) +(let ((.def_297 (+ (- 1) .def_240))) +(let ((.def_307 (___z5z___ .def_297))) +(let ((.def_224 (* (- 1) _base))) +(let ((.def_225 (+ _n .def_224))) +(let ((.def_299 (= .def_225 2))) +(let ((.def_308 (or .def_299 .def_307))) +(let ((.def_302 (not .def_299))) +(let ((.def_309 (and .def_302 .def_308))) +(let ((.def_280 (___z6z___ .def_240))) +(let ((.def_310 (= .def_280 .def_309))) +.def_310 +)))))))))))) +(assert (let ((.def_261 (= _base (- 2)))) +(let ((.def_264 (not .def_261))) +(let ((.def_188 (___z3z___ _n))) +(let ((.def_311 (or .def_188 .def_264))) +(let ((.def_312 (not .def_311))) +.def_312 +)))))) +(assert true +) +(check-sat) +(pop 1) +(assert (let ((.def_313 (+ _n (- 3)))) +(let ((.def_314 (___z3z___ .def_313))) +.def_314 +))) +(assert (let ((.def_265 (___z4z___ (- 3)))) +(let ((.def_322 (not .def_265))) +(let ((.def_269 (___z5z___ (- 3)))) +(let ((.def_318 (not .def_269))) +(let ((.def_325 (or .def_318 .def_322))) +(let ((.def_260 (___z6z___ (- 3)))) +(let ((.def_326 (or .def_260 .def_325))) +(let ((.def_323 (and .def_269 .def_322))) +(let ((.def_320 (not .def_260))) +(let ((.def_324 (and .def_320 .def_323))) +(let ((.def_327 (or .def_324 .def_326))) +(let ((.def_319 (and .def_265 .def_318))) +(let ((.def_321 (and .def_319 .def_320))) +(let ((.def_328 (or .def_321 .def_327))) +(let ((.def_315 (and .def_265 .def_269))) +(let ((.def_316 (and .def_260 .def_315))) +(let ((.def_329 (or .def_316 .def_328))) +(let ((.def_317 (not .def_316))) +(let ((.def_330 (and .def_317 .def_329))) +(let ((.def_276 (___z3z___ (- 3)))) +(let ((.def_331 (= .def_276 .def_330))) +.def_331 +)))))))))))))))))))))) +(assert (let ((.def_334 (= _base (- 3)))) +(let ((.def_333 (___z6z___ (- 4)))) +(let ((.def_335 (or .def_333 .def_334))) +(let ((.def_265 (___z4z___ (- 3)))) +(let ((.def_336 (= .def_265 .def_335))) +.def_336 +)))))) +(assert (let ((.def_338 (___z4z___ (- 4)))) +(let ((.def_334 (= _base (- 3)))) +(let ((.def_339 (or .def_334 .def_338))) +(let ((.def_337 (not .def_334))) +(let ((.def_340 (and .def_337 .def_339))) +(let ((.def_269 (___z5z___ (- 3)))) +(let ((.def_341 (= .def_269 .def_340))) +.def_341 +)))))))) +(assert (let ((.def_342 (___z5z___ (- 4)))) +(let ((.def_334 (= _base (- 3)))) +(let ((.def_343 (or .def_334 .def_342))) +(let ((.def_337 (not .def_334))) +(let ((.def_344 (and .def_337 .def_343))) +(let ((.def_260 (___z6z___ (- 3)))) +(let ((.def_345 (= .def_260 .def_344))) +.def_345 +)))))))) +(assert (let ((.def_190 (+ _n (- 1)))) +(let ((.def_220 (___z3z___ .def_190))) +(let ((.def_196 (___z4z___ .def_190))) +(let ((.def_211 (not .def_196))) +(let ((.def_200 (___z5z___ .def_190))) +(let ((.def_207 (not .def_200))) +(let ((.def_214 (or .def_207 .def_211))) +(let ((.def_191 (___z6z___ .def_190))) +(let ((.def_215 (or .def_191 .def_214))) +(let ((.def_212 (and .def_200 .def_211))) +(let ((.def_209 (not .def_191))) +(let ((.def_213 (and .def_209 .def_212))) +(let ((.def_216 (or .def_213 .def_215))) +(let ((.def_208 (and .def_196 .def_207))) +(let ((.def_210 (and .def_208 .def_209))) +(let ((.def_217 (or .def_210 .def_216))) +(let ((.def_204 (and .def_196 .def_200))) +(let ((.def_205 (and .def_191 .def_204))) +(let ((.def_218 (or .def_205 .def_217))) +(let ((.def_206 (not .def_205))) +(let ((.def_219 (and .def_206 .def_218))) +(let ((.def_221 (= .def_219 .def_220))) +.def_221 +))))))))))))))))))))))) +(assert (let ((.def_224 (* (- 1) _base))) +(let ((.def_225 (+ _n .def_224))) +(let ((.def_226 (= .def_225 1))) +(let ((.def_190 (+ _n (- 1)))) +(let ((.def_222 (+ (- 1) .def_190))) +(let ((.def_223 (___z6z___ .def_222))) +(let ((.def_227 (or .def_223 .def_226))) +(let ((.def_196 (___z4z___ .def_190))) +(let ((.def_228 (= .def_196 .def_227))) +.def_228 +)))))))))) +(assert (let ((.def_190 (+ _n (- 1)))) +(let ((.def_222 (+ (- 1) .def_190))) +(let ((.def_230 (___z4z___ .def_222))) +(let ((.def_224 (* (- 1) _base))) +(let ((.def_225 (+ _n .def_224))) +(let ((.def_226 (= .def_225 1))) +(let ((.def_231 (or .def_226 .def_230))) +(let ((.def_229 (not .def_226))) +(let ((.def_232 (and .def_229 .def_231))) +(let ((.def_200 (___z5z___ .def_190))) +(let ((.def_233 (= .def_200 .def_232))) +.def_233 +)))))))))))) +(assert (let ((.def_190 (+ _n (- 1)))) +(let ((.def_222 (+ (- 1) .def_190))) +(let ((.def_234 (___z5z___ .def_222))) +(let ((.def_224 (* (- 1) _base))) +(let ((.def_225 (+ _n .def_224))) +(let ((.def_226 (= .def_225 1))) +(let ((.def_235 (or .def_226 .def_234))) +(let ((.def_229 (not .def_226))) +(let ((.def_236 (and .def_229 .def_235))) +(let ((.def_191 (___z6z___ .def_190))) +(let ((.def_237 (= .def_191 .def_236))) +.def_237 +)))))))))))) +(push 1) +(assert (let ((.def_334 (= _base (- 3)))) +(let ((.def_337 (not .def_334))) +(let ((.def_117 (___z3z___ 0))) +(let ((.def_346 (or .def_117 .def_337))) +(let ((.def_347 (not .def_346))) +.def_347 +)))))) +(assert true +) +(check-sat) +(pop 1) +(assert (let ((.def_349 (___z3z___ (- 4)))) +.def_349 +)) +(push 1) +(assert (let ((.def_240 (+ _n (- 2)))) +(let ((.def_278 (___z4z___ .def_240))) +(let ((.def_287 (not .def_278))) +(let ((.def_277 (___z5z___ .def_240))) +(let ((.def_283 (not .def_277))) +(let ((.def_290 (or .def_283 .def_287))) +(let ((.def_280 (___z6z___ .def_240))) +(let ((.def_291 (or .def_280 .def_290))) +(let ((.def_288 (and .def_277 .def_287))) +(let ((.def_285 (not .def_280))) +(let ((.def_289 (and .def_285 .def_288))) +(let ((.def_292 (or .def_289 .def_291))) +(let ((.def_284 (and .def_278 .def_283))) +(let ((.def_286 (and .def_284 .def_285))) +(let ((.def_293 (or .def_286 .def_292))) +(let ((.def_279 (and .def_277 .def_278))) +(let ((.def_281 (and .def_279 .def_280))) +(let ((.def_294 (or .def_281 .def_293))) +(let ((.def_282 (not .def_281))) +(let ((.def_295 (and .def_282 .def_294))) +(let ((.def_241 (___z3z___ .def_240))) +(let ((.def_296 (= .def_241 .def_295))) +.def_296 +))))))))))))))))))))))) +(assert (let ((.def_224 (* (- 1) _base))) +(let ((.def_225 (+ _n .def_224))) +(let ((.def_299 (= .def_225 2))) +(let ((.def_240 (+ _n (- 2)))) +(let ((.def_297 (+ (- 1) .def_240))) +(let ((.def_298 (___z6z___ .def_297))) +(let ((.def_300 (or .def_298 .def_299))) +(let ((.def_278 (___z4z___ .def_240))) +(let ((.def_301 (= .def_278 .def_300))) +.def_301 +)))))))))) +(assert (let ((.def_240 (+ _n (- 2)))) +(let ((.def_297 (+ (- 1) .def_240))) +(let ((.def_303 (___z4z___ .def_297))) +(let ((.def_224 (* (- 1) _base))) +(let ((.def_225 (+ _n .def_224))) +(let ((.def_299 (= .def_225 2))) +(let ((.def_304 (or .def_299 .def_303))) +(let ((.def_302 (not .def_299))) +(let ((.def_305 (and .def_302 .def_304))) +(let ((.def_277 (___z5z___ .def_240))) +(let ((.def_306 (= .def_277 .def_305))) +.def_306 +)))))))))))) +(assert (let ((.def_240 (+ _n (- 2)))) +(let ((.def_297 (+ (- 1) .def_240))) +(let ((.def_307 (___z5z___ .def_297))) +(let ((.def_224 (* (- 1) _base))) +(let ((.def_225 (+ _n .def_224))) +(let ((.def_299 (= .def_225 2))) +(let ((.def_308 (or .def_299 .def_307))) +(let ((.def_302 (not .def_299))) +(let ((.def_309 (and .def_302 .def_308))) +(let ((.def_280 (___z6z___ .def_240))) +(let ((.def_310 (= .def_280 .def_309))) +.def_310 +)))))))))))) +(assert (let ((.def_313 (+ _n (- 3)))) +(let ((.def_351 (___z4z___ .def_313))) +(let ((.def_360 (not .def_351))) +(let ((.def_350 (___z5z___ .def_313))) +(let ((.def_356 (not .def_350))) +(let ((.def_363 (or .def_356 .def_360))) +(let ((.def_353 (___z6z___ .def_313))) +(let ((.def_364 (or .def_353 .def_363))) +(let ((.def_361 (and .def_350 .def_360))) +(let ((.def_358 (not .def_353))) +(let ((.def_362 (and .def_358 .def_361))) +(let ((.def_365 (or .def_362 .def_364))) +(let ((.def_357 (and .def_351 .def_356))) +(let ((.def_359 (and .def_357 .def_358))) +(let ((.def_366 (or .def_359 .def_365))) +(let ((.def_352 (and .def_350 .def_351))) +(let ((.def_354 (and .def_352 .def_353))) +(let ((.def_367 (or .def_354 .def_366))) +(let ((.def_355 (not .def_354))) +(let ((.def_368 (and .def_355 .def_367))) +(let ((.def_314 (___z3z___ .def_313))) +(let ((.def_369 (= .def_314 .def_368))) +.def_369 +))))))))))))))))))))))) +(assert (let ((.def_224 (* (- 1) _base))) +(let ((.def_225 (+ _n .def_224))) +(let ((.def_372 (= .def_225 3))) +(let ((.def_313 (+ _n (- 3)))) +(let ((.def_370 (+ (- 1) .def_313))) +(let ((.def_371 (___z6z___ .def_370))) +(let ((.def_373 (or .def_371 .def_372))) +(let ((.def_351 (___z4z___ .def_313))) +(let ((.def_374 (= .def_351 .def_373))) +.def_374 +)))))))))) +(assert (let ((.def_313 (+ _n (- 3)))) +(let ((.def_370 (+ (- 1) .def_313))) +(let ((.def_376 (___z4z___ .def_370))) +(let ((.def_224 (* (- 1) _base))) +(let ((.def_225 (+ _n .def_224))) +(let ((.def_372 (= .def_225 3))) +(let ((.def_377 (or .def_372 .def_376))) +(let ((.def_375 (not .def_372))) +(let ((.def_378 (and .def_375 .def_377))) +(let ((.def_350 (___z5z___ .def_313))) +(let ((.def_379 (= .def_350 .def_378))) +.def_379 +)))))))))))) +(assert (let ((.def_313 (+ _n (- 3)))) +(let ((.def_370 (+ (- 1) .def_313))) +(let ((.def_380 (___z5z___ .def_370))) +(let ((.def_224 (* (- 1) _base))) +(let ((.def_225 (+ _n .def_224))) +(let ((.def_372 (= .def_225 3))) +(let ((.def_381 (or .def_372 .def_380))) +(let ((.def_375 (not .def_372))) +(let ((.def_382 (and .def_375 .def_381))) +(let ((.def_353 (___z6z___ .def_313))) +(let ((.def_383 (= .def_353 .def_382))) +.def_383 +)))))))))))) +(assert (let ((.def_334 (= _base (- 3)))) +(let ((.def_337 (not .def_334))) +(let ((.def_188 (___z3z___ _n))) +(let ((.def_384 (or .def_188 .def_337))) +(let ((.def_385 (not .def_384))) +.def_385 +)))))) +(assert true +) +(check-sat) diff --git a/test/regress/regress1/uflia/stalmark_e7_27_e7_31.ec.smt2.expect b/test/regress/regress1/uflia/stalmark_e7_27_e7_31.ec.smt2.expect new file mode 100644 index 000000000..70b8fa26d --- /dev/null +++ b/test/regress/regress1/uflia/stalmark_e7_27_e7_31.ec.smt2.expect @@ -0,0 +1,7 @@ +% COMMAND-LINE: --incremental +% EXPECT: unsat +% EXPECT: sat +% EXPECT: unsat +% EXPECT: sat +% EXPECT: unsat +% EXPECT: unsat |