Refactor regressions (#1581)

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