From: Morgan Deters Date: Tue, 21 Aug 2012 22:13:12 +0000 (+0000) Subject: add some incremental in-tree regressions X-Git-Tag: cvc5-1.0.0~7856 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c2fa4e991c3ba17857019da9becd185e90cc0ee0;p=cvc5.git add some incremental in-tree regressions --- diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 6dfc9f22d..7cf356d2c 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -874,7 +874,7 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, // If sending to the shared terms database, it's also simple if (toTheoryId == THEORY_BUILTIN) { - Assert(atom.getKind() == kind::EQUAL); + Assert(atom.getKind() == kind::EQUAL, "atom should be an EQUALity, not `%s'", atom.toString().c_str()); if (markPropagation(assertion, assertion, toTheoryId, fromTheoryId)) { d_sharedTerms.assertEquality(atom, polarity, assertion); } diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index c11d16729..6d7e7d4d5 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -84,7 +84,8 @@ CVC_TESTS = \ wiki.19.cvc \ wiki.20.cvc \ wiki.21.cvc \ - simplification_bug3.cvc + simplification_bug3.cvc \ + queries0.cvc # Regression tests for TPTP inputs TPTP_TESTS = \ @@ -108,6 +109,7 @@ BUG_TESTS = \ bug167.smt \ bug168.smt \ bug187.smt2 \ + bug216.smt2 \ bug220.smt2 \ bug239.smt \ bug288.smt \ @@ -124,7 +126,8 @@ BUG_TESTS = \ TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) EXTRA_DIST = $(TESTS) \ - simplification_bug4.smt2.expect + simplification_bug4.smt2.expect \ + bug216.smt2.expect if CVC4_BUILD_PROFILE_COMPETITION else diff --git a/test/regress/regress0/bug216.smt2 b/test/regress/regress0/bug216.smt2 new file mode 100644 index 000000000..78e0f716c --- /dev/null +++ b/test/regress/regress0/bug216.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_UF) +(declare-fun x () Bool) +(declare-fun y () Bool) +(assert (=> x y)) +(check-sat) ; returns sat +(assert (=> y x)) +(assert (and x (not y))) +(check-sat) ; returns sat --> ERROR diff --git a/test/regress/regress0/bug216.smt2.expect b/test/regress/regress0/bug216.smt2.expect new file mode 100644 index 000000000..9a8435b2d --- /dev/null +++ b/test/regress/regress0/bug216.smt2.expect @@ -0,0 +1,4 @@ +% COMMAND-LINE: --incremental +% EXPECT: sat +% EXPECT: unsat +% EXIT: 20 diff --git a/test/regress/regress0/queries0.cvc b/test/regress/regress0/queries0.cvc new file mode 100644 index 000000000..c951aaf2e --- /dev/null +++ b/test/regress/regress0/queries0.cvc @@ -0,0 +1,12 @@ +% Tests the invariants for multiple queries. +% COMMAND-LINE: --incremental + +a, b: BOOLEAN; + +% EXPECT: valid +QUERY (a AND b) OR NOT (a AND b); + +% EXPECT: invalid +QUERY (a OR b); + +% EXIT: 10 diff --git a/test/regress/regress0/uflia/DRAGON_11_e1_2450.ec.minimized.smt2 b/test/regress/regress0/uflia/DRAGON_11_e1_2450.ec.minimized.smt2 new file mode 100644 index 000000000..ab8e5d1da --- /dev/null +++ b/test/regress/regress0/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/regress0/uflia/DRAGON_11_e1_2450.ec.minimized.smt2.expect b/test/regress/regress0/uflia/DRAGON_11_e1_2450.ec.minimized.smt2.expect new file mode 100644 index 000000000..917440603 --- /dev/null +++ b/test/regress/regress0/uflia/DRAGON_11_e1_2450.ec.minimized.smt2.expect @@ -0,0 +1,4 @@ +% COMMAND-LINE: --incremental +% EXPECT: sat +% EXPECT: sat +% EXIT: 10 diff --git a/test/regress/regress0/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2 b/test/regress/regress0/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2 new file mode 100644 index 000000000..0274e4390 --- /dev/null +++ b/test/regress/regress0/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/regress0/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2.expect b/test/regress/regress0/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2.expect new file mode 100644 index 000000000..bd24c606e --- /dev/null +++ b/test/regress/regress0/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2.expect @@ -0,0 +1,3 @@ +% COMMAND-LINE: --incremental +% EXPECT: sat +% EXIT: 10 diff --git a/test/regress/regress0/uflia/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 b/test/regress/regress0/uflia/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 new file mode 100644 index 000000000..25f006d30 --- /dev/null +++ b/test/regress/regress0/uflia/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 @@ -0,0 +1,1356 @@ +(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) 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 ___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) Bool) +(declare-fun ___z26z___ (Int) Int) +(declare-fun ___z27z___ (Int) Bool) +(push 1) +(assert (let ((.def_531 (___z20z___ 0))) +(let ((.def_528 (___z12z___ (- 1)))) +(let ((.def_529 (<= 1 .def_528))) +(let ((.def_525 (___z15z___ (- 1)))) +(let ((.def_524 (___z14z___ (- 1)))) +(let ((.def_526 (+ .def_524 .def_525))) +(let ((.def_527 (<= 1 .def_526))) +(let ((.def_530 (and .def_527 .def_529))) +(let ((.def_532 (= .def_530 .def_531))) +.def_532 +)))))))))) +(assert (let ((.def_538 (___z11z___ 0))) +(let ((.def_535 (___z15z___ 0))) +(let ((.def_536 (<= 0 .def_535))) +(let ((.def_533 (___z16z___ 0))) +(let ((.def_534 (not .def_533))) +(let ((.def_537 (or .def_534 .def_536))) +(let ((.def_539 (= .def_537 .def_538))) +.def_539 +)))))))) +(assert (let ((.def_541 (___z21z___ 0))) +(let ((.def_524 (___z14z___ (- 1)))) +(let ((.def_540 (<= 1 .def_524))) +(let ((.def_542 (= .def_540 .def_541))) +.def_542 +))))) +(assert (let ((.def_570 (___z12z___ 0))) +(let ((.def_528 (___z12z___ (- 1)))) +(let ((.def_543 (+ (- 1) .def_528))) +(let ((.def_544 (___z25z___ 0))) +(let ((.def_545 (ite .def_544 .def_543 .def_528))) +(let ((.def_546 (___z9z___ 0))) +(let ((.def_547 (ite .def_546 .def_545 .def_528))) +(let ((.def_548 (___z24z___ 0))) +(let ((.def_549 (ite .def_548 .def_543 .def_528))) +(let ((.def_550 (___z8z___ 0))) +(let ((.def_551 (ite .def_550 .def_549 .def_547))) +(let ((.def_552 (___z23z___ 0))) +(let ((.def_553 (ite .def_552 .def_543 .def_528))) +(let ((.def_554 (___z7z___ 0))) +(let ((.def_555 (ite .def_554 .def_553 .def_551))) +(let ((.def_531 (___z20z___ 0))) +(let ((.def_556 (ite .def_531 .def_543 .def_528))) +(let ((.def_557 (___z4z___ 0))) +(let ((.def_558 (ite .def_557 .def_556 .def_555))) +(let ((.def_559 (___z19z___ 0))) +(let ((.def_560 (ite .def_559 .def_543 .def_528))) +(let ((.def_561 (___z3z___ 0))) +(let ((.def_562 (ite .def_561 .def_560 .def_558))) +(let ((.def_563 (___z18z___ 0))) +(let ((.def_564 (ite .def_563 .def_543 .def_528))) +(let ((.def_565 (___z2z___ 0))) +(let ((.def_566 (ite .def_565 .def_564 .def_562))) +(let ((.def_567 (___z26z___ 0))) +(let ((.def_568 (= _base 0))) +(let ((.def_569 (ite .def_568 .def_567 .def_566))) +(let ((.def_571 (= .def_569 .def_570))) +.def_571 +)))))))))))))))))))))))))))))))) +(assert (let ((.def_573 (___z22z___ 0))) +(let ((.def_525 (___z15z___ (- 1)))) +(let ((.def_572 (= .def_525 1))) +(let ((.def_574 (= .def_572 .def_573))) +.def_574 +))))) +(assert (let ((.def_588 (___z13z___ 0))) +(let ((.def_575 (___z13z___ (- 1)))) +(let ((.def_576 (+ (- 1) .def_575))) +(let ((.def_548 (___z24z___ 0))) +(let ((.def_577 (ite .def_548 .def_576 .def_575))) +(let ((.def_550 (___z8z___ 0))) +(let ((.def_578 (ite .def_550 .def_577 .def_575))) +(let ((.def_552 (___z23z___ 0))) +(let ((.def_579 (ite .def_552 1 .def_575))) +(let ((.def_554 (___z7z___ 0))) +(let ((.def_580 (ite .def_554 .def_579 .def_578))) +(let ((.def_581 (+ 1 .def_575))) +(let ((.def_541 (___z21z___ 0))) +(let ((.def_582 (ite .def_541 .def_581 .def_575))) +(let ((.def_583 (___z5z___ 0))) +(let ((.def_584 (ite .def_583 .def_582 .def_580))) +(let ((.def_559 (___z19z___ 0))) +(let ((.def_585 (ite .def_559 .def_576 .def_575))) +(let ((.def_561 (___z3z___ 0))) +(let ((.def_586 (ite .def_561 .def_585 .def_584))) +(let ((.def_568 (= _base 0))) +(let ((.def_587 (ite .def_568 0 .def_586))) +(let ((.def_589 (= .def_587 .def_588))) +.def_589 +)))))))))))))))))))))))) +(assert (let ((.def_575 (___z13z___ (- 1)))) +(let ((.def_592 (= .def_575 0))) +(let ((.def_528 (___z12z___ (- 1)))) +(let ((.def_529 (<= 1 .def_528))) +(let ((.def_593 (and .def_529 .def_592))) +(let ((.def_525 (___z15z___ (- 1)))) +(let ((.def_591 (= .def_525 0))) +(let ((.def_594 (and .def_591 .def_593))) +(let ((.def_524 (___z14z___ (- 1)))) +(let ((.def_590 (= .def_524 0))) +(let ((.def_595 (and .def_590 .def_594))) +(let ((.def_552 (___z23z___ 0))) +(let ((.def_596 (= .def_552 .def_595))) +.def_596 +)))))))))))))) +(assert (let ((.def_611 (___z14z___ 0))) +(let ((.def_524 (___z14z___ (- 1)))) +(let ((.def_544 (___z25z___ 0))) +(let ((.def_597 (ite .def_544 0 .def_524))) +(let ((.def_546 (___z9z___ 0))) +(let ((.def_598 (ite .def_546 .def_597 .def_524))) +(let ((.def_599 (+ 1 .def_524))) +(let ((.def_573 (___z22z___ 0))) +(let ((.def_600 (ite .def_573 .def_599 .def_524))) +(let ((.def_601 (___z6z___ 0))) +(let ((.def_602 (ite .def_601 .def_600 .def_598))) +(let ((.def_603 (+ (- 1) .def_524))) +(let ((.def_541 (___z21z___ 0))) +(let ((.def_604 (ite .def_541 .def_603 .def_524))) +(let ((.def_583 (___z5z___ 0))) +(let ((.def_605 (ite .def_583 .def_604 .def_602))) +(let ((.def_531 (___z20z___ 0))) +(let ((.def_606 (ite .def_531 0 .def_524))) +(let ((.def_557 (___z4z___ 0))) +(let ((.def_607 (ite .def_557 .def_606 .def_605))) +(let ((.def_563 (___z18z___ 0))) +(let ((.def_608 (ite .def_563 .def_599 .def_524))) +(let ((.def_565 (___z2z___ 0))) +(let ((.def_609 (ite .def_565 .def_608 .def_607))) +(let ((.def_568 (= _base 0))) +(let ((.def_610 (ite .def_568 0 .def_609))) +(let ((.def_612 (= .def_610 .def_611))) +.def_612 +)))))))))))))))))))))))))))) +(assert (let ((.def_575 (___z13z___ (- 1)))) +(let ((.def_613 (<= 1 .def_575))) +(let ((.def_528 (___z12z___ (- 1)))) +(let ((.def_529 (<= 1 .def_528))) +(let ((.def_614 (and .def_529 .def_613))) +(let ((.def_548 (___z24z___ 0))) +(let ((.def_615 (= .def_548 .def_614))) +.def_615 +)))))))) +(assert (let ((.def_525 (___z15z___ (- 1)))) +(let ((.def_524 (___z14z___ (- 1)))) +(let ((.def_526 (+ .def_524 .def_525))) +(let ((.def_616 (+ 1 .def_526))) +(let ((.def_544 (___z25z___ 0))) +(let ((.def_617 (ite .def_544 .def_616 .def_525))) +(let ((.def_546 (___z9z___ 0))) +(let ((.def_618 (ite .def_546 .def_617 .def_525))) +(let ((.def_619 (+ 2 .def_525))) +(let ((.def_548 (___z24z___ 0))) +(let ((.def_620 (ite .def_548 .def_619 .def_525))) +(let ((.def_550 (___z8z___ 0))) +(let ((.def_621 (ite .def_550 .def_620 .def_618))) +(let ((.def_573 (___z22z___ 0))) +(let ((.def_622 (ite .def_573 0 .def_525))) +(let ((.def_601 (___z6z___ 0))) +(let ((.def_623 (ite .def_601 .def_622 .def_621))) +(let ((.def_624 (+ (- 1) .def_525))) +(let ((.def_625 (+ .def_524 .def_624))) +(let ((.def_626 (+ 1 .def_625))) +(let ((.def_531 (___z20z___ 0))) +(let ((.def_627 (ite .def_531 .def_626 .def_525))) +(let ((.def_557 (___z4z___ 0))) +(let ((.def_628 (ite .def_557 .def_627 .def_623))) +(let ((.def_559 (___z19z___ 0))) +(let ((.def_629 (ite .def_559 .def_619 .def_525))) +(let ((.def_561 (___z3z___ 0))) +(let ((.def_630 (ite .def_561 .def_629 .def_628))) +(let ((.def_568 (= _base 0))) +(let ((.def_631 (ite .def_568 0 .def_630))) +(let ((.def_535 (___z15z___ 0))) +(let ((.def_632 (= .def_535 .def_631))) +.def_632 +))))))))))))))))))))))))))))))))) +(assert (let ((.def_544 (___z25z___ 0))) +(let ((.def_528 (___z12z___ (- 1)))) +(let ((.def_529 (<= 1 .def_528))) +(let ((.def_525 (___z15z___ (- 1)))) +(let ((.def_524 (___z14z___ (- 1)))) +(let ((.def_526 (+ .def_524 .def_525))) +(let ((.def_527 (<= 1 .def_526))) +(let ((.def_530 (and .def_527 .def_529))) +(let ((.def_633 (= .def_530 .def_544))) +.def_633 +)))))))))) +(assert (let ((.def_637 (___z16z___ (- 1)))) +(let ((.def_635 (___z27z___ 0))) +(let ((.def_638 (or .def_635 .def_637))) +(let ((.def_568 (= _base 0))) +(let ((.def_639 (or .def_568 .def_638))) +(let ((.def_634 (not .def_568))) +(let ((.def_636 (or .def_634 .def_635))) +(let ((.def_640 (and .def_636 .def_639))) +(let ((.def_533 (___z16z___ 0))) +(let ((.def_641 (= .def_533 .def_640))) +.def_641 +))))))))))) +(assert (let ((.def_642 (___z26z___ (- 1)))) +(let ((.def_643 (___z10z___ 0))) +(let ((.def_568 (= _base 0))) +(let ((.def_644 (ite .def_568 .def_643 .def_642))) +(let ((.def_567 (___z26z___ 0))) +(let ((.def_645 (= .def_567 .def_644))) +.def_645 +))))))) +(assert (let ((.def_546 (___z9z___ 0))) +(let ((.def_664 (not .def_546))) +(let ((.def_565 (___z2z___ 0))) +(let ((.def_655 (not .def_565))) +(let ((.def_561 (___z3z___ 0))) +(let ((.def_654 (not .def_561))) +(let ((.def_656 (and .def_654 .def_655))) +(let ((.def_557 (___z4z___ 0))) +(let ((.def_653 (not .def_557))) +(let ((.def_657 (and .def_653 .def_656))) +(let ((.def_583 (___z5z___ 0))) +(let ((.def_652 (not .def_583))) +(let ((.def_658 (and .def_652 .def_657))) +(let ((.def_601 (___z6z___ 0))) +(let ((.def_651 (not .def_601))) +(let ((.def_659 (and .def_651 .def_658))) +(let ((.def_554 (___z7z___ 0))) +(let ((.def_650 (not .def_554))) +(let ((.def_660 (and .def_650 .def_659))) +(let ((.def_550 (___z8z___ 0))) +(let ((.def_649 (not .def_550))) +(let ((.def_661 (and .def_649 .def_660))) +(let ((.def_698 (and .def_661 .def_664))) +(let ((.def_691 (and .def_565 .def_654))) +(let ((.def_692 (and .def_653 .def_691))) +(let ((.def_693 (and .def_652 .def_692))) +(let ((.def_694 (and .def_651 .def_693))) +(let ((.def_695 (and .def_650 .def_694))) +(let ((.def_696 (and .def_649 .def_695))) +(let ((.def_697 (and .def_664 .def_696))) +(let ((.def_699 (or .def_697 .def_698))) +(let ((.def_684 (and .def_561 .def_655))) +(let ((.def_685 (and .def_653 .def_684))) +(let ((.def_686 (and .def_652 .def_685))) +(let ((.def_687 (and .def_651 .def_686))) +(let ((.def_688 (and .def_650 .def_687))) +(let ((.def_689 (and .def_649 .def_688))) +(let ((.def_690 (and .def_664 .def_689))) +(let ((.def_700 (or .def_690 .def_699))) +(let ((.def_678 (and .def_557 .def_656))) +(let ((.def_679 (and .def_652 .def_678))) +(let ((.def_680 (and .def_651 .def_679))) +(let ((.def_681 (and .def_650 .def_680))) +(let ((.def_682 (and .def_649 .def_681))) +(let ((.def_683 (and .def_664 .def_682))) +(let ((.def_701 (or .def_683 .def_700))) +(let ((.def_673 (and .def_583 .def_657))) +(let ((.def_674 (and .def_651 .def_673))) +(let ((.def_675 (and .def_650 .def_674))) +(let ((.def_676 (and .def_649 .def_675))) +(let ((.def_677 (and .def_664 .def_676))) +(let ((.def_702 (or .def_677 .def_701))) +(let ((.def_669 (and .def_601 .def_658))) +(let ((.def_670 (and .def_650 .def_669))) +(let ((.def_671 (and .def_649 .def_670))) +(let ((.def_672 (and .def_664 .def_671))) +(let ((.def_703 (or .def_672 .def_702))) +(let ((.def_666 (and .def_554 .def_659))) +(let ((.def_667 (and .def_649 .def_666))) +(let ((.def_668 (and .def_664 .def_667))) +(let ((.def_704 (or .def_668 .def_703))) +(let ((.def_663 (and .def_550 .def_660))) +(let ((.def_665 (and .def_663 .def_664))) +(let ((.def_705 (or .def_665 .def_704))) +(let ((.def_662 (and .def_546 .def_661))) +(let ((.def_706 (or .def_662 .def_705))) +(let ((.def_643 (___z10z___ 0))) +(let ((.def_648 (<= 0 .def_643))) +(let ((.def_707 (and .def_648 .def_706))) +(let ((.def_646 (<= 5 .def_643))) +(let ((.def_647 (not .def_646))) +(let ((.def_708 (and .def_647 .def_707))) +(let ((.def_635 (___z27z___ 0))) +(let ((.def_709 (= .def_635 .def_708))) +.def_709 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +(assert (let ((.def_575 (___z13z___ (- 1)))) +(let ((.def_592 (= .def_575 0))) +(let ((.def_528 (___z12z___ (- 1)))) +(let ((.def_529 (<= 1 .def_528))) +(let ((.def_593 (and .def_529 .def_592))) +(let ((.def_525 (___z15z___ (- 1)))) +(let ((.def_591 (= .def_525 0))) +(let ((.def_594 (and .def_591 .def_593))) +(let ((.def_524 (___z14z___ (- 1)))) +(let ((.def_590 (= .def_524 0))) +(let ((.def_595 (and .def_590 .def_594))) +(let ((.def_563 (___z18z___ 0))) +(let ((.def_710 (= .def_563 .def_595))) +.def_710 +)))))))))))))) +(assert (let ((.def_575 (___z13z___ (- 1)))) +(let ((.def_613 (<= 1 .def_575))) +(let ((.def_528 (___z12z___ (- 1)))) +(let ((.def_529 (<= 1 .def_528))) +(let ((.def_614 (and .def_529 .def_613))) +(let ((.def_559 (___z19z___ 0))) +(let ((.def_711 (= .def_559 .def_614))) +.def_711 +)))))))) +(assert (let ((.def_720 (___z20z___ (- 1)))) +(let ((.def_717 (___z12z___ (- 2)))) +(let ((.def_718 (<= 1 .def_717))) +(let ((.def_714 (___z15z___ (- 2)))) +(let ((.def_713 (___z14z___ (- 2)))) +(let ((.def_715 (+ .def_713 .def_714))) +(let ((.def_716 (<= 1 .def_715))) +(let ((.def_719 (and .def_716 .def_718))) +(let ((.def_721 (= .def_719 .def_720))) +.def_721 +)))))))))) +(assert (let ((.def_725 (___z11z___ (- 1)))) +(let ((.def_525 (___z15z___ (- 1)))) +(let ((.def_723 (<= 0 .def_525))) +(let ((.def_637 (___z16z___ (- 1)))) +(let ((.def_722 (not .def_637))) +(let ((.def_724 (or .def_722 .def_723))) +(let ((.def_726 (= .def_724 .def_725))) +.def_726 +)))))))) +(assert (let ((.def_728 (___z21z___ (- 1)))) +(let ((.def_713 (___z14z___ (- 2)))) +(let ((.def_727 (<= 1 .def_713))) +(let ((.def_729 (= .def_727 .def_728))) +.def_729 +))))) +(assert (let ((.def_717 (___z12z___ (- 2)))) +(let ((.def_730 (+ (- 1) .def_717))) +(let ((.def_731 (___z25z___ (- 1)))) +(let ((.def_732 (ite .def_731 .def_730 .def_717))) +(let ((.def_733 (___z9z___ (- 1)))) +(let ((.def_734 (ite .def_733 .def_732 .def_717))) +(let ((.def_735 (___z24z___ (- 1)))) +(let ((.def_736 (ite .def_735 .def_730 .def_717))) +(let ((.def_737 (___z8z___ (- 1)))) +(let ((.def_738 (ite .def_737 .def_736 .def_734))) +(let ((.def_739 (___z23z___ (- 1)))) +(let ((.def_740 (ite .def_739 .def_730 .def_717))) +(let ((.def_741 (___z7z___ (- 1)))) +(let ((.def_742 (ite .def_741 .def_740 .def_738))) +(let ((.def_720 (___z20z___ (- 1)))) +(let ((.def_743 (ite .def_720 .def_730 .def_717))) +(let ((.def_744 (___z4z___ (- 1)))) +(let ((.def_745 (ite .def_744 .def_743 .def_742))) +(let ((.def_746 (___z19z___ (- 1)))) +(let ((.def_747 (ite .def_746 .def_730 .def_717))) +(let ((.def_748 (___z3z___ (- 1)))) +(let ((.def_749 (ite .def_748 .def_747 .def_745))) +(let ((.def_750 (___z18z___ (- 1)))) +(let ((.def_751 (ite .def_750 .def_730 .def_717))) +(let ((.def_752 (___z2z___ (- 1)))) +(let ((.def_753 (ite .def_752 .def_751 .def_749))) +(let ((.def_642 (___z26z___ (- 1)))) +(let ((.def_754 (= _base (- 1)))) +(let ((.def_755 (ite .def_754 .def_642 .def_753))) +(let ((.def_528 (___z12z___ (- 1)))) +(let ((.def_756 (= .def_528 .def_755))) +.def_756 +)))))))))))))))))))))))))))))))) +(assert (let ((.def_758 (___z22z___ (- 1)))) +(let ((.def_714 (___z15z___ (- 2)))) +(let ((.def_757 (= .def_714 1))) +(let ((.def_759 (= .def_757 .def_758))) +.def_759 +))))) +(assert (let ((.def_760 (___z13z___ (- 2)))) +(let ((.def_761 (+ (- 1) .def_760))) +(let ((.def_735 (___z24z___ (- 1)))) +(let ((.def_762 (ite .def_735 .def_761 .def_760))) +(let ((.def_737 (___z8z___ (- 1)))) +(let ((.def_763 (ite .def_737 .def_762 .def_760))) +(let ((.def_739 (___z23z___ (- 1)))) +(let ((.def_764 (ite .def_739 1 .def_760))) +(let ((.def_741 (___z7z___ (- 1)))) +(let ((.def_765 (ite .def_741 .def_764 .def_763))) +(let ((.def_766 (+ 1 .def_760))) +(let ((.def_728 (___z21z___ (- 1)))) +(let ((.def_767 (ite .def_728 .def_766 .def_760))) +(let ((.def_768 (___z5z___ (- 1)))) +(let ((.def_769 (ite .def_768 .def_767 .def_765))) +(let ((.def_746 (___z19z___ (- 1)))) +(let ((.def_770 (ite .def_746 .def_761 .def_760))) +(let ((.def_748 (___z3z___ (- 1)))) +(let ((.def_771 (ite .def_748 .def_770 .def_769))) +(let ((.def_754 (= _base (- 1)))) +(let ((.def_772 (ite .def_754 0 .def_771))) +(let ((.def_575 (___z13z___ (- 1)))) +(let ((.def_773 (= .def_575 .def_772))) +.def_773 +)))))))))))))))))))))))) +(assert (let ((.def_760 (___z13z___ (- 2)))) +(let ((.def_776 (= .def_760 0))) +(let ((.def_717 (___z12z___ (- 2)))) +(let ((.def_718 (<= 1 .def_717))) +(let ((.def_777 (and .def_718 .def_776))) +(let ((.def_714 (___z15z___ (- 2)))) +(let ((.def_775 (= .def_714 0))) +(let ((.def_778 (and .def_775 .def_777))) +(let ((.def_713 (___z14z___ (- 2)))) +(let ((.def_774 (= .def_713 0))) +(let ((.def_779 (and .def_774 .def_778))) +(let ((.def_739 (___z23z___ (- 1)))) +(let ((.def_780 (= .def_739 .def_779))) +.def_780 +)))))))))))))) +(assert (let ((.def_713 (___z14z___ (- 2)))) +(let ((.def_731 (___z25z___ (- 1)))) +(let ((.def_781 (ite .def_731 0 .def_713))) +(let ((.def_733 (___z9z___ (- 1)))) +(let ((.def_782 (ite .def_733 .def_781 .def_713))) +(let ((.def_783 (+ 1 .def_713))) +(let ((.def_758 (___z22z___ (- 1)))) +(let ((.def_784 (ite .def_758 .def_783 .def_713))) +(let ((.def_785 (___z6z___ (- 1)))) +(let ((.def_786 (ite .def_785 .def_784 .def_782))) +(let ((.def_787 (+ (- 1) .def_713))) +(let ((.def_728 (___z21z___ (- 1)))) +(let ((.def_788 (ite .def_728 .def_787 .def_713))) +(let ((.def_768 (___z5z___ (- 1)))) +(let ((.def_789 (ite .def_768 .def_788 .def_786))) +(let ((.def_720 (___z20z___ (- 1)))) +(let ((.def_790 (ite .def_720 0 .def_713))) +(let ((.def_744 (___z4z___ (- 1)))) +(let ((.def_791 (ite .def_744 .def_790 .def_789))) +(let ((.def_750 (___z18z___ (- 1)))) +(let ((.def_792 (ite .def_750 .def_783 .def_713))) +(let ((.def_752 (___z2z___ (- 1)))) +(let ((.def_793 (ite .def_752 .def_792 .def_791))) +(let ((.def_754 (= _base (- 1)))) +(let ((.def_794 (ite .def_754 0 .def_793))) +(let ((.def_524 (___z14z___ (- 1)))) +(let ((.def_795 (= .def_524 .def_794))) +.def_795 +)))))))))))))))))))))))))))) +(assert (let ((.def_760 (___z13z___ (- 2)))) +(let ((.def_796 (<= 1 .def_760))) +(let ((.def_717 (___z12z___ (- 2)))) +(let ((.def_718 (<= 1 .def_717))) +(let ((.def_797 (and .def_718 .def_796))) +(let ((.def_735 (___z24z___ (- 1)))) +(let ((.def_798 (= .def_735 .def_797))) +.def_798 +)))))))) +(assert (let ((.def_714 (___z15z___ (- 2)))) +(let ((.def_713 (___z14z___ (- 2)))) +(let ((.def_715 (+ .def_713 .def_714))) +(let ((.def_799 (+ 1 .def_715))) +(let ((.def_731 (___z25z___ (- 1)))) +(let ((.def_800 (ite .def_731 .def_799 .def_714))) +(let ((.def_733 (___z9z___ (- 1)))) +(let ((.def_801 (ite .def_733 .def_800 .def_714))) +(let ((.def_802 (+ 2 .def_714))) +(let ((.def_735 (___z24z___ (- 1)))) +(let ((.def_803 (ite .def_735 .def_802 .def_714))) +(let ((.def_737 (___z8z___ (- 1)))) +(let ((.def_804 (ite .def_737 .def_803 .def_801))) +(let ((.def_758 (___z22z___ (- 1)))) +(let ((.def_805 (ite .def_758 0 .def_714))) +(let ((.def_785 (___z6z___ (- 1)))) +(let ((.def_806 (ite .def_785 .def_805 .def_804))) +(let ((.def_807 (+ (- 1) .def_714))) +(let ((.def_808 (+ .def_713 .def_807))) +(let ((.def_809 (+ 1 .def_808))) +(let ((.def_720 (___z20z___ (- 1)))) +(let ((.def_810 (ite .def_720 .def_809 .def_714))) +(let ((.def_744 (___z4z___ (- 1)))) +(let ((.def_811 (ite .def_744 .def_810 .def_806))) +(let ((.def_746 (___z19z___ (- 1)))) +(let ((.def_812 (ite .def_746 .def_802 .def_714))) +(let ((.def_748 (___z3z___ (- 1)))) +(let ((.def_813 (ite .def_748 .def_812 .def_811))) +(let ((.def_754 (= _base (- 1)))) +(let ((.def_814 (ite .def_754 0 .def_813))) +(let ((.def_525 (___z15z___ (- 1)))) +(let ((.def_815 (= .def_525 .def_814))) +.def_815 +))))))))))))))))))))))))))))))))) +(assert (let ((.def_731 (___z25z___ (- 1)))) +(let ((.def_717 (___z12z___ (- 2)))) +(let ((.def_718 (<= 1 .def_717))) +(let ((.def_714 (___z15z___ (- 2)))) +(let ((.def_713 (___z14z___ (- 2)))) +(let ((.def_715 (+ .def_713 .def_714))) +(let ((.def_716 (<= 1 .def_715))) +(let ((.def_719 (and .def_716 .def_718))) +(let ((.def_816 (= .def_719 .def_731))) +.def_816 +)))))))))) +(assert (let ((.def_820 (___z16z___ (- 2)))) +(let ((.def_818 (___z27z___ (- 1)))) +(let ((.def_821 (or .def_818 .def_820))) +(let ((.def_754 (= _base (- 1)))) +(let ((.def_822 (or .def_754 .def_821))) +(let ((.def_817 (not .def_754))) +(let ((.def_819 (or .def_817 .def_818))) +(let ((.def_823 (and .def_819 .def_822))) +(let ((.def_637 (___z16z___ (- 1)))) +(let ((.def_824 (= .def_637 .def_823))) +.def_824 +))))))))))) +(assert (let ((.def_825 (___z26z___ (- 2)))) +(let ((.def_826 (___z10z___ (- 1)))) +(let ((.def_754 (= _base (- 1)))) +(let ((.def_827 (ite .def_754 .def_826 .def_825))) +(let ((.def_642 (___z26z___ (- 1)))) +(let ((.def_828 (= .def_642 .def_827))) +.def_828 +))))))) +(assert (let ((.def_733 (___z9z___ (- 1)))) +(let ((.def_847 (not .def_733))) +(let ((.def_752 (___z2z___ (- 1)))) +(let ((.def_838 (not .def_752))) +(let ((.def_748 (___z3z___ (- 1)))) +(let ((.def_837 (not .def_748))) +(let ((.def_839 (and .def_837 .def_838))) +(let ((.def_744 (___z4z___ (- 1)))) +(let ((.def_836 (not .def_744))) +(let ((.def_840 (and .def_836 .def_839))) +(let ((.def_768 (___z5z___ (- 1)))) +(let ((.def_835 (not .def_768))) +(let ((.def_841 (and .def_835 .def_840))) +(let ((.def_785 (___z6z___ (- 1)))) +(let ((.def_834 (not .def_785))) +(let ((.def_842 (and .def_834 .def_841))) +(let ((.def_741 (___z7z___ (- 1)))) +(let ((.def_833 (not .def_741))) +(let ((.def_843 (and .def_833 .def_842))) +(let ((.def_737 (___z8z___ (- 1)))) +(let ((.def_832 (not .def_737))) +(let ((.def_844 (and .def_832 .def_843))) +(let ((.def_881 (and .def_844 .def_847))) +(let ((.def_874 (and .def_752 .def_837))) +(let ((.def_875 (and .def_836 .def_874))) +(let ((.def_876 (and .def_835 .def_875))) +(let ((.def_877 (and .def_834 .def_876))) +(let ((.def_878 (and .def_833 .def_877))) +(let ((.def_879 (and .def_832 .def_878))) +(let ((.def_880 (and .def_847 .def_879))) +(let ((.def_882 (or .def_880 .def_881))) +(let ((.def_867 (and .def_748 .def_838))) +(let ((.def_868 (and .def_836 .def_867))) +(let ((.def_869 (and .def_835 .def_868))) +(let ((.def_870 (and .def_834 .def_869))) +(let ((.def_871 (and .def_833 .def_870))) +(let ((.def_872 (and .def_832 .def_871))) +(let ((.def_873 (and .def_847 .def_872))) +(let ((.def_883 (or .def_873 .def_882))) +(let ((.def_861 (and .def_744 .def_839))) +(let ((.def_862 (and .def_835 .def_861))) +(let ((.def_863 (and .def_834 .def_862))) +(let ((.def_864 (and .def_833 .def_863))) +(let ((.def_865 (and .def_832 .def_864))) +(let ((.def_866 (and .def_847 .def_865))) +(let ((.def_884 (or .def_866 .def_883))) +(let ((.def_856 (and .def_768 .def_840))) +(let ((.def_857 (and .def_834 .def_856))) +(let ((.def_858 (and .def_833 .def_857))) +(let ((.def_859 (and .def_832 .def_858))) +(let ((.def_860 (and .def_847 .def_859))) +(let ((.def_885 (or .def_860 .def_884))) +(let ((.def_852 (and .def_785 .def_841))) +(let ((.def_853 (and .def_833 .def_852))) +(let ((.def_854 (and .def_832 .def_853))) +(let ((.def_855 (and .def_847 .def_854))) +(let ((.def_886 (or .def_855 .def_885))) +(let ((.def_849 (and .def_741 .def_842))) +(let ((.def_850 (and .def_832 .def_849))) +(let ((.def_851 (and .def_847 .def_850))) +(let ((.def_887 (or .def_851 .def_886))) +(let ((.def_846 (and .def_737 .def_843))) +(let ((.def_848 (and .def_846 .def_847))) +(let ((.def_888 (or .def_848 .def_887))) +(let ((.def_845 (and .def_733 .def_844))) +(let ((.def_889 (or .def_845 .def_888))) +(let ((.def_826 (___z10z___ (- 1)))) +(let ((.def_831 (<= 0 .def_826))) +(let ((.def_890 (and .def_831 .def_889))) +(let ((.def_829 (<= 5 .def_826))) +(let ((.def_830 (not .def_829))) +(let ((.def_891 (and .def_830 .def_890))) +(let ((.def_818 (___z27z___ (- 1)))) +(let ((.def_892 (= .def_818 .def_891))) +.def_892 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +(assert (let ((.def_760 (___z13z___ (- 2)))) +(let ((.def_776 (= .def_760 0))) +(let ((.def_717 (___z12z___ (- 2)))) +(let ((.def_718 (<= 1 .def_717))) +(let ((.def_777 (and .def_718 .def_776))) +(let ((.def_714 (___z15z___ (- 2)))) +(let ((.def_775 (= .def_714 0))) +(let ((.def_778 (and .def_775 .def_777))) +(let ((.def_713 (___z14z___ (- 2)))) +(let ((.def_774 (= .def_713 0))) +(let ((.def_779 (and .def_774 .def_778))) +(let ((.def_750 (___z18z___ (- 1)))) +(let ((.def_893 (= .def_750 .def_779))) +.def_893 +)))))))))))))) +(assert (let ((.def_760 (___z13z___ (- 2)))) +(let ((.def_796 (<= 1 .def_760))) +(let ((.def_717 (___z12z___ (- 2)))) +(let ((.def_718 (<= 1 .def_717))) +(let ((.def_797 (and .def_718 .def_796))) +(let ((.def_746 (___z19z___ (- 1)))) +(let ((.def_894 (= .def_746 .def_797))) +.def_894 +)))))))) +(push 1) +(assert (let ((.def_725 (___z11z___ (- 1)))) +(let ((.def_538 (___z11z___ 0))) +(let ((.def_895 (and .def_538 .def_725))) +(let ((.def_754 (= _base (- 1)))) +(let ((.def_817 (not .def_754))) +(let ((.def_896 (or .def_817 .def_895))) +(let ((.def_897 (not .def_896))) +.def_897 +)))))))) +(assert true +) +(check-sat) +(pop 1) +(assert (let ((.def_725 (___z11z___ (- 1)))) +.def_725 +)) +(assert (let ((.def_898 (___z11z___ (- 2)))) +.def_898 +)) +(push 1) +(assert (let ((.def_907 (___z20z___ _n))) +(let ((.def_899 (+ _n (- 1)))) +(let ((.def_904 (___z12z___ .def_899))) +(let ((.def_905 (<= 1 .def_904))) +(let ((.def_901 (___z15z___ .def_899))) +(let ((.def_900 (___z14z___ .def_899))) +(let ((.def_902 (+ .def_900 .def_901))) +(let ((.def_903 (<= 1 .def_902))) +(let ((.def_906 (and .def_903 .def_905))) +(let ((.def_908 (= .def_906 .def_907))) +.def_908 +))))))))))) +(assert (let ((.def_914 (___z11z___ _n))) +(let ((.def_911 (___z15z___ _n))) +(let ((.def_912 (<= 0 .def_911))) +(let ((.def_909 (___z16z___ _n))) +(let ((.def_910 (not .def_909))) +(let ((.def_913 (or .def_910 .def_912))) +(let ((.def_915 (= .def_913 .def_914))) +.def_915 +)))))))) +(assert (let ((.def_917 (___z21z___ _n))) +(let ((.def_899 (+ _n (- 1)))) +(let ((.def_900 (___z14z___ .def_899))) +(let ((.def_916 (<= 1 .def_900))) +(let ((.def_918 (= .def_916 .def_917))) +.def_918 +)))))) +(assert (let ((.def_946 (___z12z___ _n))) +(let ((.def_899 (+ _n (- 1)))) +(let ((.def_904 (___z12z___ .def_899))) +(let ((.def_919 (+ (- 1) .def_904))) +(let ((.def_920 (___z25z___ _n))) +(let ((.def_921 (ite .def_920 .def_919 .def_904))) +(let ((.def_922 (___z9z___ _n))) +(let ((.def_923 (ite .def_922 .def_921 .def_904))) +(let ((.def_924 (___z24z___ _n))) +(let ((.def_925 (ite .def_924 .def_919 .def_904))) +(let ((.def_926 (___z8z___ _n))) +(let ((.def_927 (ite .def_926 .def_925 .def_923))) +(let ((.def_928 (___z23z___ _n))) +(let ((.def_929 (ite .def_928 .def_919 .def_904))) +(let ((.def_930 (___z7z___ _n))) +(let ((.def_931 (ite .def_930 .def_929 .def_927))) +(let ((.def_907 (___z20z___ _n))) +(let ((.def_932 (ite .def_907 .def_919 .def_904))) +(let ((.def_933 (___z4z___ _n))) +(let ((.def_934 (ite .def_933 .def_932 .def_931))) +(let ((.def_935 (___z19z___ _n))) +(let ((.def_936 (ite .def_935 .def_919 .def_904))) +(let ((.def_937 (___z3z___ _n))) +(let ((.def_938 (ite .def_937 .def_936 .def_934))) +(let ((.def_939 (___z18z___ _n))) +(let ((.def_940 (ite .def_939 .def_919 .def_904))) +(let ((.def_941 (___z2z___ _n))) +(let ((.def_942 (ite .def_941 .def_940 .def_938))) +(let ((.def_943 (___z26z___ _n))) +(let ((.def_944 (= _n _base))) +(let ((.def_945 (ite .def_944 .def_943 .def_942))) +(let ((.def_947 (= .def_945 .def_946))) +.def_947 +))))))))))))))))))))))))))))))))) +(assert (let ((.def_949 (___z22z___ _n))) +(let ((.def_899 (+ _n (- 1)))) +(let ((.def_901 (___z15z___ .def_899))) +(let ((.def_948 (= .def_901 1))) +(let ((.def_950 (= .def_948 .def_949))) +.def_950 +)))))) +(assert (let ((.def_964 (___z13z___ _n))) +(let ((.def_899 (+ _n (- 1)))) +(let ((.def_951 (___z13z___ .def_899))) +(let ((.def_952 (+ (- 1) .def_951))) +(let ((.def_924 (___z24z___ _n))) +(let ((.def_953 (ite .def_924 .def_952 .def_951))) +(let ((.def_926 (___z8z___ _n))) +(let ((.def_954 (ite .def_926 .def_953 .def_951))) +(let ((.def_928 (___z23z___ _n))) +(let ((.def_955 (ite .def_928 1 .def_951))) +(let ((.def_930 (___z7z___ _n))) +(let ((.def_956 (ite .def_930 .def_955 .def_954))) +(let ((.def_957 (+ 1 .def_951))) +(let ((.def_917 (___z21z___ _n))) +(let ((.def_958 (ite .def_917 .def_957 .def_951))) +(let ((.def_959 (___z5z___ _n))) +(let ((.def_960 (ite .def_959 .def_958 .def_956))) +(let ((.def_935 (___z19z___ _n))) +(let ((.def_961 (ite .def_935 .def_952 .def_951))) +(let ((.def_937 (___z3z___ _n))) +(let ((.def_962 (ite .def_937 .def_961 .def_960))) +(let ((.def_944 (= _n _base))) +(let ((.def_963 (ite .def_944 0 .def_962))) +(let ((.def_965 (= .def_963 .def_964))) +.def_965 +))))))))))))))))))))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_951 (___z13z___ .def_899))) +(let ((.def_968 (= .def_951 0))) +(let ((.def_904 (___z12z___ .def_899))) +(let ((.def_905 (<= 1 .def_904))) +(let ((.def_969 (and .def_905 .def_968))) +(let ((.def_901 (___z15z___ .def_899))) +(let ((.def_967 (= .def_901 0))) +(let ((.def_970 (and .def_967 .def_969))) +(let ((.def_900 (___z14z___ .def_899))) +(let ((.def_966 (= .def_900 0))) +(let ((.def_971 (and .def_966 .def_970))) +(let ((.def_928 (___z23z___ _n))) +(let ((.def_972 (= .def_928 .def_971))) +.def_972 +))))))))))))))) +(assert (let ((.def_987 (___z14z___ _n))) +(let ((.def_899 (+ _n (- 1)))) +(let ((.def_900 (___z14z___ .def_899))) +(let ((.def_920 (___z25z___ _n))) +(let ((.def_973 (ite .def_920 0 .def_900))) +(let ((.def_922 (___z9z___ _n))) +(let ((.def_974 (ite .def_922 .def_973 .def_900))) +(let ((.def_975 (+ 1 .def_900))) +(let ((.def_949 (___z22z___ _n))) +(let ((.def_976 (ite .def_949 .def_975 .def_900))) +(let ((.def_977 (___z6z___ _n))) +(let ((.def_978 (ite .def_977 .def_976 .def_974))) +(let ((.def_979 (+ (- 1) .def_900))) +(let ((.def_917 (___z21z___ _n))) +(let ((.def_980 (ite .def_917 .def_979 .def_900))) +(let ((.def_959 (___z5z___ _n))) +(let ((.def_981 (ite .def_959 .def_980 .def_978))) +(let ((.def_907 (___z20z___ _n))) +(let ((.def_982 (ite .def_907 0 .def_900))) +(let ((.def_933 (___z4z___ _n))) +(let ((.def_983 (ite .def_933 .def_982 .def_981))) +(let ((.def_939 (___z18z___ _n))) +(let ((.def_984 (ite .def_939 .def_975 .def_900))) +(let ((.def_941 (___z2z___ _n))) +(let ((.def_985 (ite .def_941 .def_984 .def_983))) +(let ((.def_944 (= _n _base))) +(let ((.def_986 (ite .def_944 0 .def_985))) +(let ((.def_988 (= .def_986 .def_987))) +.def_988 +))))))))))))))))))))))))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_951 (___z13z___ .def_899))) +(let ((.def_989 (<= 1 .def_951))) +(let ((.def_904 (___z12z___ .def_899))) +(let ((.def_905 (<= 1 .def_904))) +(let ((.def_990 (and .def_905 .def_989))) +(let ((.def_924 (___z24z___ _n))) +(let ((.def_991 (= .def_924 .def_990))) +.def_991 +))))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_901 (___z15z___ .def_899))) +(let ((.def_900 (___z14z___ .def_899))) +(let ((.def_902 (+ .def_900 .def_901))) +(let ((.def_992 (+ 1 .def_902))) +(let ((.def_920 (___z25z___ _n))) +(let ((.def_993 (ite .def_920 .def_992 .def_901))) +(let ((.def_922 (___z9z___ _n))) +(let ((.def_994 (ite .def_922 .def_993 .def_901))) +(let ((.def_995 (+ 2 .def_901))) +(let ((.def_924 (___z24z___ _n))) +(let ((.def_996 (ite .def_924 .def_995 .def_901))) +(let ((.def_926 (___z8z___ _n))) +(let ((.def_997 (ite .def_926 .def_996 .def_994))) +(let ((.def_949 (___z22z___ _n))) +(let ((.def_998 (ite .def_949 0 .def_901))) +(let ((.def_977 (___z6z___ _n))) +(let ((.def_999 (ite .def_977 .def_998 .def_997))) +(let ((.def_1000 (+ (- 1) .def_901))) +(let ((.def_1001 (+ .def_900 .def_1000))) +(let ((.def_1002 (+ 1 .def_1001))) +(let ((.def_907 (___z20z___ _n))) +(let ((.def_1003 (ite .def_907 .def_1002 .def_901))) +(let ((.def_933 (___z4z___ _n))) +(let ((.def_1004 (ite .def_933 .def_1003 .def_999))) +(let ((.def_935 (___z19z___ _n))) +(let ((.def_1005 (ite .def_935 .def_995 .def_901))) +(let ((.def_937 (___z3z___ _n))) +(let ((.def_1006 (ite .def_937 .def_1005 .def_1004))) +(let ((.def_944 (= _n _base))) +(let ((.def_1007 (ite .def_944 0 .def_1006))) +(let ((.def_911 (___z15z___ _n))) +(let ((.def_1008 (= .def_911 .def_1007))) +.def_1008 +)))))))))))))))))))))))))))))))))) +(assert (let ((.def_920 (___z25z___ _n))) +(let ((.def_899 (+ _n (- 1)))) +(let ((.def_904 (___z12z___ .def_899))) +(let ((.def_905 (<= 1 .def_904))) +(let ((.def_901 (___z15z___ .def_899))) +(let ((.def_900 (___z14z___ .def_899))) +(let ((.def_902 (+ .def_900 .def_901))) +(let ((.def_903 (<= 1 .def_902))) +(let ((.def_906 (and .def_903 .def_905))) +(let ((.def_1009 (= .def_906 .def_920))) +.def_1009 +))))))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_1013 (___z16z___ .def_899))) +(let ((.def_1011 (___z27z___ _n))) +(let ((.def_1014 (or .def_1011 .def_1013))) +(let ((.def_944 (= _n _base))) +(let ((.def_1015 (or .def_944 .def_1014))) +(let ((.def_1010 (not .def_944))) +(let ((.def_1012 (or .def_1010 .def_1011))) +(let ((.def_1016 (and .def_1012 .def_1015))) +(let ((.def_909 (___z16z___ _n))) +(let ((.def_1017 (= .def_909 .def_1016))) +.def_1017 +)))))))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_1018 (___z26z___ .def_899))) +(let ((.def_1019 (___z10z___ _n))) +(let ((.def_944 (= _n _base))) +(let ((.def_1020 (ite .def_944 .def_1019 .def_1018))) +(let ((.def_943 (___z26z___ _n))) +(let ((.def_1021 (= .def_943 .def_1020))) +.def_1021 +)))))))) +(assert (let ((.def_922 (___z9z___ _n))) +(let ((.def_1040 (not .def_922))) +(let ((.def_941 (___z2z___ _n))) +(let ((.def_1031 (not .def_941))) +(let ((.def_937 (___z3z___ _n))) +(let ((.def_1030 (not .def_937))) +(let ((.def_1032 (and .def_1030 .def_1031))) +(let ((.def_933 (___z4z___ _n))) +(let ((.def_1029 (not .def_933))) +(let ((.def_1033 (and .def_1029 .def_1032))) +(let ((.def_959 (___z5z___ _n))) +(let ((.def_1028 (not .def_959))) +(let ((.def_1034 (and .def_1028 .def_1033))) +(let ((.def_977 (___z6z___ _n))) +(let ((.def_1027 (not .def_977))) +(let ((.def_1035 (and .def_1027 .def_1034))) +(let ((.def_930 (___z7z___ _n))) +(let ((.def_1026 (not .def_930))) +(let ((.def_1036 (and .def_1026 .def_1035))) +(let ((.def_926 (___z8z___ _n))) +(let ((.def_1025 (not .def_926))) +(let ((.def_1037 (and .def_1025 .def_1036))) +(let ((.def_1074 (and .def_1037 .def_1040))) +(let ((.def_1067 (and .def_941 .def_1030))) +(let ((.def_1068 (and .def_1029 .def_1067))) +(let ((.def_1069 (and .def_1028 .def_1068))) +(let ((.def_1070 (and .def_1027 .def_1069))) +(let ((.def_1071 (and .def_1026 .def_1070))) +(let ((.def_1072 (and .def_1025 .def_1071))) +(let ((.def_1073 (and .def_1040 .def_1072))) +(let ((.def_1075 (or .def_1073 .def_1074))) +(let ((.def_1060 (and .def_937 .def_1031))) +(let ((.def_1061 (and .def_1029 .def_1060))) +(let ((.def_1062 (and .def_1028 .def_1061))) +(let ((.def_1063 (and .def_1027 .def_1062))) +(let ((.def_1064 (and .def_1026 .def_1063))) +(let ((.def_1065 (and .def_1025 .def_1064))) +(let ((.def_1066 (and .def_1040 .def_1065))) +(let ((.def_1076 (or .def_1066 .def_1075))) +(let ((.def_1054 (and .def_933 .def_1032))) +(let ((.def_1055 (and .def_1028 .def_1054))) +(let ((.def_1056 (and .def_1027 .def_1055))) +(let ((.def_1057 (and .def_1026 .def_1056))) +(let ((.def_1058 (and .def_1025 .def_1057))) +(let ((.def_1059 (and .def_1040 .def_1058))) +(let ((.def_1077 (or .def_1059 .def_1076))) +(let ((.def_1049 (and .def_959 .def_1033))) +(let ((.def_1050 (and .def_1027 .def_1049))) +(let ((.def_1051 (and .def_1026 .def_1050))) +(let ((.def_1052 (and .def_1025 .def_1051))) +(let ((.def_1053 (and .def_1040 .def_1052))) +(let ((.def_1078 (or .def_1053 .def_1077))) +(let ((.def_1045 (and .def_977 .def_1034))) +(let ((.def_1046 (and .def_1026 .def_1045))) +(let ((.def_1047 (and .def_1025 .def_1046))) +(let ((.def_1048 (and .def_1040 .def_1047))) +(let ((.def_1079 (or .def_1048 .def_1078))) +(let ((.def_1042 (and .def_930 .def_1035))) +(let ((.def_1043 (and .def_1025 .def_1042))) +(let ((.def_1044 (and .def_1040 .def_1043))) +(let ((.def_1080 (or .def_1044 .def_1079))) +(let ((.def_1039 (and .def_926 .def_1036))) +(let ((.def_1041 (and .def_1039 .def_1040))) +(let ((.def_1081 (or .def_1041 .def_1080))) +(let ((.def_1038 (and .def_922 .def_1037))) +(let ((.def_1082 (or .def_1038 .def_1081))) +(let ((.def_1019 (___z10z___ _n))) +(let ((.def_1024 (<= 0 .def_1019))) +(let ((.def_1083 (and .def_1024 .def_1082))) +(let ((.def_1022 (<= 5 .def_1019))) +(let ((.def_1023 (not .def_1022))) +(let ((.def_1084 (and .def_1023 .def_1083))) +(let ((.def_1011 (___z27z___ _n))) +(let ((.def_1085 (= .def_1011 .def_1084))) +.def_1085 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_951 (___z13z___ .def_899))) +(let ((.def_968 (= .def_951 0))) +(let ((.def_904 (___z12z___ .def_899))) +(let ((.def_905 (<= 1 .def_904))) +(let ((.def_969 (and .def_905 .def_968))) +(let ((.def_901 (___z15z___ .def_899))) +(let ((.def_967 (= .def_901 0))) +(let ((.def_970 (and .def_967 .def_969))) +(let ((.def_900 (___z14z___ .def_899))) +(let ((.def_966 (= .def_900 0))) +(let ((.def_971 (and .def_966 .def_970))) +(let ((.def_939 (___z18z___ _n))) +(let ((.def_1086 (= .def_939 .def_971))) +.def_1086 +))))))))))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_951 (___z13z___ .def_899))) +(let ((.def_989 (<= 1 .def_951))) +(let ((.def_904 (___z12z___ .def_899))) +(let ((.def_905 (<= 1 .def_904))) +(let ((.def_990 (and .def_905 .def_989))) +(let ((.def_935 (___z19z___ _n))) +(let ((.def_1087 (= .def_935 .def_990))) +.def_1087 +))))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_1096 (___z20z___ .def_899))) +(let ((.def_1088 (+ (- 1) .def_899))) +(let ((.def_1093 (___z12z___ .def_1088))) +(let ((.def_1094 (<= 1 .def_1093))) +(let ((.def_1090 (___z15z___ .def_1088))) +(let ((.def_1089 (___z14z___ .def_1088))) +(let ((.def_1091 (+ .def_1089 .def_1090))) +(let ((.def_1092 (<= 1 .def_1091))) +(let ((.def_1095 (and .def_1092 .def_1094))) +(let ((.def_1097 (= .def_1095 .def_1096))) +.def_1097 +)))))))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_1101 (___z11z___ .def_899))) +(let ((.def_901 (___z15z___ .def_899))) +(let ((.def_1099 (<= 0 .def_901))) +(let ((.def_1013 (___z16z___ .def_899))) +(let ((.def_1098 (not .def_1013))) +(let ((.def_1100 (or .def_1098 .def_1099))) +(let ((.def_1102 (= .def_1100 .def_1101))) +.def_1102 +))))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_1104 (___z21z___ .def_899))) +(let ((.def_1088 (+ (- 1) .def_899))) +(let ((.def_1089 (___z14z___ .def_1088))) +(let ((.def_1103 (<= 1 .def_1089))) +(let ((.def_1105 (= .def_1103 .def_1104))) +.def_1105 +))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_1088 (+ (- 1) .def_899))) +(let ((.def_1093 (___z12z___ .def_1088))) +(let ((.def_1106 (+ (- 1) .def_1093))) +(let ((.def_1107 (___z25z___ .def_899))) +(let ((.def_1108 (ite .def_1107 .def_1106 .def_1093))) +(let ((.def_1109 (___z9z___ .def_899))) +(let ((.def_1110 (ite .def_1109 .def_1108 .def_1093))) +(let ((.def_1111 (___z24z___ .def_899))) +(let ((.def_1112 (ite .def_1111 .def_1106 .def_1093))) +(let ((.def_1113 (___z8z___ .def_899))) +(let ((.def_1114 (ite .def_1113 .def_1112 .def_1110))) +(let ((.def_1115 (___z23z___ .def_899))) +(let ((.def_1116 (ite .def_1115 .def_1106 .def_1093))) +(let ((.def_1117 (___z7z___ .def_899))) +(let ((.def_1118 (ite .def_1117 .def_1116 .def_1114))) +(let ((.def_1096 (___z20z___ .def_899))) +(let ((.def_1119 (ite .def_1096 .def_1106 .def_1093))) +(let ((.def_1120 (___z4z___ .def_899))) +(let ((.def_1121 (ite .def_1120 .def_1119 .def_1118))) +(let ((.def_1122 (___z19z___ .def_899))) +(let ((.def_1123 (ite .def_1122 .def_1106 .def_1093))) +(let ((.def_1124 (___z3z___ .def_899))) +(let ((.def_1125 (ite .def_1124 .def_1123 .def_1121))) +(let ((.def_1126 (___z18z___ .def_899))) +(let ((.def_1127 (ite .def_1126 .def_1106 .def_1093))) +(let ((.def_1128 (___z2z___ .def_899))) +(let ((.def_1129 (ite .def_1128 .def_1127 .def_1125))) +(let ((.def_1018 (___z26z___ .def_899))) +(let ((.def_1130 (* (- 1) _base))) +(let ((.def_1131 (+ _n .def_1130))) +(let ((.def_1132 (= .def_1131 1))) +(let ((.def_1133 (ite .def_1132 .def_1018 .def_1129))) +(let ((.def_904 (___z12z___ .def_899))) +(let ((.def_1134 (= .def_904 .def_1133))) +.def_1134 +)))))))))))))))))))))))))))))))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_1136 (___z22z___ .def_899))) +(let ((.def_1088 (+ (- 1) .def_899))) +(let ((.def_1090 (___z15z___ .def_1088))) +(let ((.def_1135 (= .def_1090 1))) +(let ((.def_1137 (= .def_1135 .def_1136))) +.def_1137 +))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_1088 (+ (- 1) .def_899))) +(let ((.def_1138 (___z13z___ .def_1088))) +(let ((.def_1139 (+ (- 1) .def_1138))) +(let ((.def_1111 (___z24z___ .def_899))) +(let ((.def_1140 (ite .def_1111 .def_1139 .def_1138))) +(let ((.def_1113 (___z8z___ .def_899))) +(let ((.def_1141 (ite .def_1113 .def_1140 .def_1138))) +(let ((.def_1115 (___z23z___ .def_899))) +(let ((.def_1142 (ite .def_1115 1 .def_1138))) +(let ((.def_1117 (___z7z___ .def_899))) +(let ((.def_1143 (ite .def_1117 .def_1142 .def_1141))) +(let ((.def_1144 (+ 1 .def_1138))) +(let ((.def_1104 (___z21z___ .def_899))) +(let ((.def_1145 (ite .def_1104 .def_1144 .def_1138))) +(let ((.def_1146 (___z5z___ .def_899))) +(let ((.def_1147 (ite .def_1146 .def_1145 .def_1143))) +(let ((.def_1122 (___z19z___ .def_899))) +(let ((.def_1148 (ite .def_1122 .def_1139 .def_1138))) +(let ((.def_1124 (___z3z___ .def_899))) +(let ((.def_1149 (ite .def_1124 .def_1148 .def_1147))) +(let ((.def_1130 (* (- 1) _base))) +(let ((.def_1131 (+ _n .def_1130))) +(let ((.def_1132 (= .def_1131 1))) +(let ((.def_1150 (ite .def_1132 0 .def_1149))) +(let ((.def_951 (___z13z___ .def_899))) +(let ((.def_1151 (= .def_951 .def_1150))) +.def_1151 +)))))))))))))))))))))))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_1088 (+ (- 1) .def_899))) +(let ((.def_1138 (___z13z___ .def_1088))) +(let ((.def_1154 (= .def_1138 0))) +(let ((.def_1093 (___z12z___ .def_1088))) +(let ((.def_1094 (<= 1 .def_1093))) +(let ((.def_1155 (and .def_1094 .def_1154))) +(let ((.def_1090 (___z15z___ .def_1088))) +(let ((.def_1153 (= .def_1090 0))) +(let ((.def_1156 (and .def_1153 .def_1155))) +(let ((.def_1089 (___z14z___ .def_1088))) +(let ((.def_1152 (= .def_1089 0))) +(let ((.def_1157 (and .def_1152 .def_1156))) +(let ((.def_1115 (___z23z___ .def_899))) +(let ((.def_1158 (= .def_1115 .def_1157))) +.def_1158 +)))))))))))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_1088 (+ (- 1) .def_899))) +(let ((.def_1089 (___z14z___ .def_1088))) +(let ((.def_1107 (___z25z___ .def_899))) +(let ((.def_1159 (ite .def_1107 0 .def_1089))) +(let ((.def_1109 (___z9z___ .def_899))) +(let ((.def_1160 (ite .def_1109 .def_1159 .def_1089))) +(let ((.def_1161 (+ 1 .def_1089))) +(let ((.def_1136 (___z22z___ .def_899))) +(let ((.def_1162 (ite .def_1136 .def_1161 .def_1089))) +(let ((.def_1163 (___z6z___ .def_899))) +(let ((.def_1164 (ite .def_1163 .def_1162 .def_1160))) +(let ((.def_1165 (+ (- 1) .def_1089))) +(let ((.def_1104 (___z21z___ .def_899))) +(let ((.def_1166 (ite .def_1104 .def_1165 .def_1089))) +(let ((.def_1146 (___z5z___ .def_899))) +(let ((.def_1167 (ite .def_1146 .def_1166 .def_1164))) +(let ((.def_1096 (___z20z___ .def_899))) +(let ((.def_1168 (ite .def_1096 0 .def_1089))) +(let ((.def_1120 (___z4z___ .def_899))) +(let ((.def_1169 (ite .def_1120 .def_1168 .def_1167))) +(let ((.def_1126 (___z18z___ .def_899))) +(let ((.def_1170 (ite .def_1126 .def_1161 .def_1089))) +(let ((.def_1128 (___z2z___ .def_899))) +(let ((.def_1171 (ite .def_1128 .def_1170 .def_1169))) +(let ((.def_1130 (* (- 1) _base))) +(let ((.def_1131 (+ _n .def_1130))) +(let ((.def_1132 (= .def_1131 1))) +(let ((.def_1172 (ite .def_1132 0 .def_1171))) +(let ((.def_900 (___z14z___ .def_899))) +(let ((.def_1173 (= .def_900 .def_1172))) +.def_1173 +)))))))))))))))))))))))))))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_1088 (+ (- 1) .def_899))) +(let ((.def_1138 (___z13z___ .def_1088))) +(let ((.def_1174 (<= 1 .def_1138))) +(let ((.def_1093 (___z12z___ .def_1088))) +(let ((.def_1094 (<= 1 .def_1093))) +(let ((.def_1175 (and .def_1094 .def_1174))) +(let ((.def_1111 (___z24z___ .def_899))) +(let ((.def_1176 (= .def_1111 .def_1175))) +.def_1176 +)))))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_1088 (+ (- 1) .def_899))) +(let ((.def_1090 (___z15z___ .def_1088))) +(let ((.def_1089 (___z14z___ .def_1088))) +(let ((.def_1091 (+ .def_1089 .def_1090))) +(let ((.def_1177 (+ 1 .def_1091))) +(let ((.def_1107 (___z25z___ .def_899))) +(let ((.def_1178 (ite .def_1107 .def_1177 .def_1090))) +(let ((.def_1109 (___z9z___ .def_899))) +(let ((.def_1179 (ite .def_1109 .def_1178 .def_1090))) +(let ((.def_1180 (+ 2 .def_1090))) +(let ((.def_1111 (___z24z___ .def_899))) +(let ((.def_1181 (ite .def_1111 .def_1180 .def_1090))) +(let ((.def_1113 (___z8z___ .def_899))) +(let ((.def_1182 (ite .def_1113 .def_1181 .def_1179))) +(let ((.def_1136 (___z22z___ .def_899))) +(let ((.def_1183 (ite .def_1136 0 .def_1090))) +(let ((.def_1163 (___z6z___ .def_899))) +(let ((.def_1184 (ite .def_1163 .def_1183 .def_1182))) +(let ((.def_1185 (+ (- 1) .def_1090))) +(let ((.def_1186 (+ .def_1089 .def_1185))) +(let ((.def_1187 (+ 1 .def_1186))) +(let ((.def_1096 (___z20z___ .def_899))) +(let ((.def_1188 (ite .def_1096 .def_1187 .def_1090))) +(let ((.def_1120 (___z4z___ .def_899))) +(let ((.def_1189 (ite .def_1120 .def_1188 .def_1184))) +(let ((.def_1122 (___z19z___ .def_899))) +(let ((.def_1190 (ite .def_1122 .def_1180 .def_1090))) +(let ((.def_1124 (___z3z___ .def_899))) +(let ((.def_1191 (ite .def_1124 .def_1190 .def_1189))) +(let ((.def_1130 (* (- 1) _base))) +(let ((.def_1131 (+ _n .def_1130))) +(let ((.def_1132 (= .def_1131 1))) +(let ((.def_1192 (ite .def_1132 0 .def_1191))) +(let ((.def_901 (___z15z___ .def_899))) +(let ((.def_1193 (= .def_901 .def_1192))) +.def_1193 +))))))))))))))))))))))))))))))))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_1107 (___z25z___ .def_899))) +(let ((.def_1088 (+ (- 1) .def_899))) +(let ((.def_1093 (___z12z___ .def_1088))) +(let ((.def_1094 (<= 1 .def_1093))) +(let ((.def_1090 (___z15z___ .def_1088))) +(let ((.def_1089 (___z14z___ .def_1088))) +(let ((.def_1091 (+ .def_1089 .def_1090))) +(let ((.def_1092 (<= 1 .def_1091))) +(let ((.def_1095 (and .def_1092 .def_1094))) +(let ((.def_1194 (= .def_1095 .def_1107))) +.def_1194 +)))))))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_1088 (+ (- 1) .def_899))) +(let ((.def_1198 (___z16z___ .def_1088))) +(let ((.def_1196 (___z27z___ .def_899))) +(let ((.def_1199 (or .def_1196 .def_1198))) +(let ((.def_1130 (* (- 1) _base))) +(let ((.def_1131 (+ _n .def_1130))) +(let ((.def_1132 (= .def_1131 1))) +(let ((.def_1200 (or .def_1132 .def_1199))) +(let ((.def_1195 (not .def_1132))) +(let ((.def_1197 (or .def_1195 .def_1196))) +(let ((.def_1201 (and .def_1197 .def_1200))) +(let ((.def_1013 (___z16z___ .def_899))) +(let ((.def_1202 (= .def_1013 .def_1201))) +.def_1202 +))))))))))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_1088 (+ (- 1) .def_899))) +(let ((.def_1203 (___z26z___ .def_1088))) +(let ((.def_1204 (___z10z___ .def_899))) +(let ((.def_1130 (* (- 1) _base))) +(let ((.def_1131 (+ _n .def_1130))) +(let ((.def_1132 (= .def_1131 1))) +(let ((.def_1205 (ite .def_1132 .def_1204 .def_1203))) +(let ((.def_1018 (___z26z___ .def_899))) +(let ((.def_1206 (= .def_1018 .def_1205))) +.def_1206 +))))))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_1109 (___z9z___ .def_899))) +(let ((.def_1225 (not .def_1109))) +(let ((.def_1128 (___z2z___ .def_899))) +(let ((.def_1216 (not .def_1128))) +(let ((.def_1124 (___z3z___ .def_899))) +(let ((.def_1215 (not .def_1124))) +(let ((.def_1217 (and .def_1215 .def_1216))) +(let ((.def_1120 (___z4z___ .def_899))) +(let ((.def_1214 (not .def_1120))) +(let ((.def_1218 (and .def_1214 .def_1217))) +(let ((.def_1146 (___z5z___ .def_899))) +(let ((.def_1213 (not .def_1146))) +(let ((.def_1219 (and .def_1213 .def_1218))) +(let ((.def_1163 (___z6z___ .def_899))) +(let ((.def_1212 (not .def_1163))) +(let ((.def_1220 (and .def_1212 .def_1219))) +(let ((.def_1117 (___z7z___ .def_899))) +(let ((.def_1211 (not .def_1117))) +(let ((.def_1221 (and .def_1211 .def_1220))) +(let ((.def_1113 (___z8z___ .def_899))) +(let ((.def_1210 (not .def_1113))) +(let ((.def_1222 (and .def_1210 .def_1221))) +(let ((.def_1259 (and .def_1222 .def_1225))) +(let ((.def_1252 (and .def_1128 .def_1215))) +(let ((.def_1253 (and .def_1214 .def_1252))) +(let ((.def_1254 (and .def_1213 .def_1253))) +(let ((.def_1255 (and .def_1212 .def_1254))) +(let ((.def_1256 (and .def_1211 .def_1255))) +(let ((.def_1257 (and .def_1210 .def_1256))) +(let ((.def_1258 (and .def_1225 .def_1257))) +(let ((.def_1260 (or .def_1258 .def_1259))) +(let ((.def_1245 (and .def_1124 .def_1216))) +(let ((.def_1246 (and .def_1214 .def_1245))) +(let ((.def_1247 (and .def_1213 .def_1246))) +(let ((.def_1248 (and .def_1212 .def_1247))) +(let ((.def_1249 (and .def_1211 .def_1248))) +(let ((.def_1250 (and .def_1210 .def_1249))) +(let ((.def_1251 (and .def_1225 .def_1250))) +(let ((.def_1261 (or .def_1251 .def_1260))) +(let ((.def_1239 (and .def_1120 .def_1217))) +(let ((.def_1240 (and .def_1213 .def_1239))) +(let ((.def_1241 (and .def_1212 .def_1240))) +(let ((.def_1242 (and .def_1211 .def_1241))) +(let ((.def_1243 (and .def_1210 .def_1242))) +(let ((.def_1244 (and .def_1225 .def_1243))) +(let ((.def_1262 (or .def_1244 .def_1261))) +(let ((.def_1234 (and .def_1146 .def_1218))) +(let ((.def_1235 (and .def_1212 .def_1234))) +(let ((.def_1236 (and .def_1211 .def_1235))) +(let ((.def_1237 (and .def_1210 .def_1236))) +(let ((.def_1238 (and .def_1225 .def_1237))) +(let ((.def_1263 (or .def_1238 .def_1262))) +(let ((.def_1230 (and .def_1163 .def_1219))) +(let ((.def_1231 (and .def_1211 .def_1230))) +(let ((.def_1232 (and .def_1210 .def_1231))) +(let ((.def_1233 (and .def_1225 .def_1232))) +(let ((.def_1264 (or .def_1233 .def_1263))) +(let ((.def_1227 (and .def_1117 .def_1220))) +(let ((.def_1228 (and .def_1210 .def_1227))) +(let ((.def_1229 (and .def_1225 .def_1228))) +(let ((.def_1265 (or .def_1229 .def_1264))) +(let ((.def_1224 (and .def_1113 .def_1221))) +(let ((.def_1226 (and .def_1224 .def_1225))) +(let ((.def_1266 (or .def_1226 .def_1265))) +(let ((.def_1223 (and .def_1109 .def_1222))) +(let ((.def_1267 (or .def_1223 .def_1266))) +(let ((.def_1204 (___z10z___ .def_899))) +(let ((.def_1209 (<= 0 .def_1204))) +(let ((.def_1268 (and .def_1209 .def_1267))) +(let ((.def_1207 (<= 5 .def_1204))) +(let ((.def_1208 (not .def_1207))) +(let ((.def_1269 (and .def_1208 .def_1268))) +(let ((.def_1196 (___z27z___ .def_899))) +(let ((.def_1270 (= .def_1196 .def_1269))) +.def_1270 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_1088 (+ (- 1) .def_899))) +(let ((.def_1138 (___z13z___ .def_1088))) +(let ((.def_1154 (= .def_1138 0))) +(let ((.def_1093 (___z12z___ .def_1088))) +(let ((.def_1094 (<= 1 .def_1093))) +(let ((.def_1155 (and .def_1094 .def_1154))) +(let ((.def_1090 (___z15z___ .def_1088))) +(let ((.def_1153 (= .def_1090 0))) +(let ((.def_1156 (and .def_1153 .def_1155))) +(let ((.def_1089 (___z14z___ .def_1088))) +(let ((.def_1152 (= .def_1089 0))) +(let ((.def_1157 (and .def_1152 .def_1156))) +(let ((.def_1126 (___z18z___ .def_899))) +(let ((.def_1271 (= .def_1126 .def_1157))) +.def_1271 +)))))))))))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_1088 (+ (- 1) .def_899))) +(let ((.def_1138 (___z13z___ .def_1088))) +(let ((.def_1174 (<= 1 .def_1138))) +(let ((.def_1093 (___z12z___ .def_1088))) +(let ((.def_1094 (<= 1 .def_1093))) +(let ((.def_1175 (and .def_1094 .def_1174))) +(let ((.def_1122 (___z19z___ .def_899))) +(let ((.def_1272 (= .def_1122 .def_1175))) +.def_1272 +)))))))))) +(assert (let ((.def_899 (+ _n (- 1)))) +(let ((.def_1101 (___z11z___ .def_899))) +.def_1101 +))) +(assert (let ((.def_914 (___z11z___ _n))) +(let ((.def_754 (= _base (- 1)))) +(let ((.def_817 (not .def_754))) +(let ((.def_1273 (or .def_817 .def_914))) +(let ((.def_1274 (not .def_1273))) +.def_1274 +)))))) +(assert true +) +(check-sat) +(pop 1) diff --git a/test/regress/regress0/uflia/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect b/test/regress/regress0/uflia/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect new file mode 100644 index 000000000..a06e9864e --- /dev/null +++ b/test/regress/regress0/uflia/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect @@ -0,0 +1,4 @@ +% COMMAND-LINE: --incremental +% EXPECT: unsat +% EXPECT: sat +% EXIT: 10 diff --git a/test/regress/regress0/uflia/FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2 b/test/regress/regress0/uflia/FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2 new file mode 100644 index 000000000..248a056d3 --- /dev/null +++ b/test/regress/regress0/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/regress0/uflia/Makefile.am b/test/regress/regress0/uflia/Makefile.am index 21479bac5..e9516d383 100644 --- a/test/regress/regress0/uflia/Makefile.am +++ b/test/regress/regress0/uflia/Makefile.am @@ -25,11 +25,25 @@ SMT_TESTS = \ error30.smt # Regression tests for SMT2 inputs -SMT2_TESTS = +SMT2_TESTS = \ + check01.smt2 \ + check02.smt2 \ + check03.smt2 \ + check04.smt2 \ + DRAGON_11_e1_2450.ec.minimized.smt2 \ + FIREFLY_3_e2_2236_e7_3681.ec.core.smt2 \ + FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 \ + FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2 \ + stalmark_e7_27_e7_31.ec.minimized.smt2 \ + stalmark_e7_27_e7_31.ec.smt2 \ + tiny.smt2 # simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2 -# javafe.ast.StandardPrettyPrint.319_no_forall.smt2 \ +# javafe.ast.StandardPrettyPrint.319_no_forall.smt2 # javafe.ast.WhileStmt.447_no_forall.smt2 +# CURRENTLY FAILING: +# speed2_e8_449_e8_517.ec.smt2 +# microwave21.ec.minimized.smt2 # Regression tests for PL inputs CVC_TESTS = @@ -41,7 +55,17 @@ TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) # Necessary to get automake's attention when splitting TESTS into # SMT_TESTS, SMT2_TESTS, etc.. -EXTRA_DIST = $(TESTS) +EXTRA_DIST = $(TESTS) \ + check02.smt2.expect \ + check03.smt2.expect \ + check04.smt2.expect \ + DRAGON_11_e1_2450.ec.minimized.smt2.expect \ + FIREFLY_3_e2_2236_e7_3681.ec.core.smt2.expect \ + FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect \ + speed2_e8_449_e8_517.ec.smt2.expect \ + stalmark_e7_27_e7_31.ec.minimized.smt2.expect \ + stalmark_e7_27_e7_31.ec.smt2.expect \ + tiny.smt2.expect # synonyms for "check" in this directory .PHONY: regress regress0 test diff --git a/test/regress/regress0/uflia/check01.smt2 b/test/regress/regress0/uflia/check01.smt2 new file mode 100644 index 000000000..9d7236b52 --- /dev/null +++ b/test/regress/regress0/uflia/check01.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXIT: 10 +(set-logic QF_UFLIA) +(set-info :smt-lib-version 2.0) +(set-info :status sat) + +(declare-fun f (Int) Bool) + +(assert (f 0)) + +(push 1) +(assert (not (f 0))) +(pop 1) +(check-sat) diff --git a/test/regress/regress0/uflia/check02.smt2 b/test/regress/regress0/uflia/check02.smt2 new file mode 100644 index 000000000..0920170c6 --- /dev/null +++ b/test/regress/regress0/uflia/check02.smt2 @@ -0,0 +1,33 @@ +(set-logic QF_UFLIA) +(declare-fun b () Int) +(declare-fun n () Int) +(declare-fun f (Int) Bool) +(declare-fun g (Int) Bool) + +(assert (<= 0 n)) +(push 1) + +(assert (or (g (- 1)) (= b 0))) + +(assert (or (= (- n b) 1) (not (or (= (- n b) 1) (f (- n 2)))))) + +(check-sat) +(pop 1) + +(push 1) +(assert (or (g (- n 1)) (= n b))) +(assert (or (not (f n)) (not (= n b)))) + +(assert (not (f (- n 2)))) + + +(assert (or (not (g (- n 1))) (not (= (- n b) 1)))) + +(assert (or (not (g (- n 1))) (or (= (- n b) 1) (f (- n 2))))) + + + +(assert (or (f n) (and (not (f n)) (f n)))) + +(check-sat) +(pop 1) \ No newline at end of file diff --git a/test/regress/regress0/uflia/check02.smt2.expect b/test/regress/regress0/uflia/check02.smt2.expect new file mode 100644 index 000000000..9a8435b2d --- /dev/null +++ b/test/regress/regress0/uflia/check02.smt2.expect @@ -0,0 +1,4 @@ +% COMMAND-LINE: --incremental +% EXPECT: sat +% EXPECT: unsat +% EXIT: 20 diff --git a/test/regress/regress0/uflia/check03.smt2 b/test/regress/regress0/uflia/check03.smt2 new file mode 100644 index 000000000..f561e1964 --- /dev/null +++ b/test/regress/regress0/uflia/check03.smt2 @@ -0,0 +1,24 @@ +(set-logic QF_UFLIA) + +(declare-fun _n () Int) +(declare-fun _f (Int) Bool) +(declare-fun _g (Int) Bool) + +(assert (not (= _n 0))) + +(push 1) +(assert (or (_g 1) (or (not (_g _n)) (not (_f _n))))) +(check-sat) +(pop 1) + + +(assert + (or (and (_g _n) (_f _n)) + (not (or (not (_g _n)) (not (_f _n)))))) + + + +(assert (or (not (_g _n)) (not (_g 0)))) +(assert (or (not (_g _n)) (_g 0))) + +(check-sat) diff --git a/test/regress/regress0/uflia/check03.smt2.expect b/test/regress/regress0/uflia/check03.smt2.expect new file mode 100644 index 000000000..9a8435b2d --- /dev/null +++ b/test/regress/regress0/uflia/check03.smt2.expect @@ -0,0 +1,4 @@ +% COMMAND-LINE: --incremental +% EXPECT: sat +% EXPECT: unsat +% EXIT: 20 diff --git a/test/regress/regress0/uflia/check04.smt2 b/test/regress/regress0/uflia/check04.smt2 new file mode 100644 index 000000000..61bc8a5d6 --- /dev/null +++ b/test/regress/regress0/uflia/check04.smt2 @@ -0,0 +1,18 @@ +(set-logic QF_LIA) +(declare-fun _b () Int) +(declare-fun _n () Int) +(declare-fun _x () Bool) + +(assert (<= 2 _n)) +(assert (not (= _b 0))) + +(push 1) +(assert (or (= _n 1) (or _x (= _b 0)))) +(check-sat) +(pop 1) + +(assert (or (= _n 1) (or _x (= _b 0)))) + +(assert (or (not _x) (= _n 1))) + +(check-sat) diff --git a/test/regress/regress0/uflia/check04.smt2.expect b/test/regress/regress0/uflia/check04.smt2.expect new file mode 100644 index 000000000..9a8435b2d --- /dev/null +++ b/test/regress/regress0/uflia/check04.smt2.expect @@ -0,0 +1,4 @@ +% COMMAND-LINE: --incremental +% EXPECT: sat +% EXPECT: unsat +% EXIT: 20 diff --git a/test/regress/regress0/uflia/microwave21.ec.minimized.smt2 b/test/regress/regress0/uflia/microwave21.ec.minimized.smt2 new file mode 100644 index 000000000..0d9accb91 --- /dev/null +++ b/test/regress/regress0/uflia/microwave21.ec.minimized.smt2 @@ -0,0 +1,444 @@ +; initialize_defs +; PROPERTY DEFGEN +(set-logic QF_UFNIA) +(set-info :status sat) +(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) \ No newline at end of file diff --git a/test/regress/regress0/uflia/speed2_e8_449_e8_517.ec.smt2 b/test/regress/regress0/uflia/speed2_e8_449_e8_517.ec.smt2 new file mode 100644 index 000000000..11fdfa51d --- /dev/null +++ b/test/regress/regress0/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/regress0/uflia/speed2_e8_449_e8_517.ec.smt2.expect b/test/regress/regress0/uflia/speed2_e8_449_e8_517.ec.smt2.expect new file mode 100644 index 000000000..fd57f4ec9 --- /dev/null +++ b/test/regress/regress0/uflia/speed2_e8_449_e8_517.ec.smt2.expect @@ -0,0 +1,6 @@ +% COMMAND-LINE: --incremental +% EXPECT: unsat +% EXPECT: sat +% EXPECT: unsat +% EXPECT: unsat +% EXIT: 20 diff --git a/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2 b/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2 new file mode 100644 index 000000000..019d70de9 --- /dev/null +++ b/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2 @@ -0,0 +1,161 @@ +(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_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_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 +)))))))))))) +(check-sat) +(pop 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_313 (+ _n (- 3)))) +(let ((.def_314 (___z3z___ .def_313))) +.def_314 +))) +(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_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_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_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 +)))))) +(check-sat) diff --git a/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2.expect b/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2.expect new file mode 100644 index 000000000..9a8435b2d --- /dev/null +++ b/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2.expect @@ -0,0 +1,4 @@ +% COMMAND-LINE: --incremental +% EXPECT: sat +% EXPECT: unsat +% EXIT: 20 diff --git a/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.smt2 b/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.smt2 new file mode 100644 index 000000000..381eb740b --- /dev/null +++ b/test/regress/regress0/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/regress0/uflia/stalmark_e7_27_e7_31.ec.smt2.expect b/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.smt2.expect new file mode 100644 index 000000000..7a97d0f21 --- /dev/null +++ b/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.smt2.expect @@ -0,0 +1,8 @@ +% COMMAND-LINE: --incremental +% EXPECT: unsat +% EXPECT: sat +% EXPECT: unsat +% EXPECT: sat +% EXPECT: unsat +% EXPECT: unsat +% EXIT: 20 diff --git a/test/regress/regress0/uflia/tiny.smt2 b/test/regress/regress0/uflia/tiny.smt2 new file mode 100644 index 000000000..fc0251a55 --- /dev/null +++ b/test/regress/regress0/uflia/tiny.smt2 @@ -0,0 +1,23 @@ +(set-logic QF_UFLIA) +(declare-fun base () Int) +(declare-fun n () Int) + +(declare-fun g (Int) Bool) +(declare-fun f (Int) Bool) + +(push 1) +(assert (<= 0 n)) +(assert (f n)) +(assert (= (f n) (or (= (- n base) 1) (g n)))) +(check-sat) +(pop 1) + +(push 1) +(assert (<= 0 n)) + +(assert (or (= (- n base) 1) (g n))) +(assert (not (g n))) +(assert (= base (- 2))) + +(check-sat) +(pop 1) \ No newline at end of file diff --git a/test/regress/regress0/uflia/tiny.smt2.expect b/test/regress/regress0/uflia/tiny.smt2.expect new file mode 100644 index 000000000..767e8af23 --- /dev/null +++ b/test/regress/regress0/uflia/tiny.smt2.expect @@ -0,0 +1,4 @@ +% COMMAND-LINE: --incremental --simplification=none +% EXPECT: sat +% EXPECT: unsat +% EXIT: 20