// 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);
}
wiki.19.cvc \
wiki.20.cvc \
wiki.21.cvc \
- simplification_bug3.cvc
+ simplification_bug3.cvc \
+ queries0.cvc
# Regression tests for TPTP inputs
TPTP_TESTS = \
bug167.smt \
bug168.smt \
bug187.smt2 \
+ bug216.smt2 \
bug220.smt2 \
bug239.smt \
bug288.smt \
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
--- /dev/null
+(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
--- /dev/null
+% COMMAND-LINE: --incremental
+% EXPECT: sat
+% EXPECT: unsat
+% EXIT: 20
--- /dev/null
+% 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
--- /dev/null
+(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)
--- /dev/null
+% COMMAND-LINE: --incremental
+% EXPECT: sat
+% EXPECT: sat
+% EXIT: 10
--- /dev/null
+(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)
--- /dev/null
+% COMMAND-LINE: --incremental
+% EXPECT: sat
+% EXIT: 10
--- /dev/null
+(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)
--- /dev/null
+% COMMAND-LINE: --incremental
+% EXPECT: unsat
+% EXPECT: sat
+% EXIT: 10
--- /dev/null
+(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)
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 =
# 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
--- /dev/null
+; 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)
--- /dev/null
+(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
--- /dev/null
+% COMMAND-LINE: --incremental
+% EXPECT: sat
+% EXPECT: unsat
+% EXIT: 20
--- /dev/null
+(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)
--- /dev/null
+% COMMAND-LINE: --incremental
+% EXPECT: sat
+% EXPECT: unsat
+% EXIT: 20
--- /dev/null
+(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)
--- /dev/null
+% COMMAND-LINE: --incremental
+% EXPECT: sat
+% EXPECT: unsat
+% EXIT: 20
--- /dev/null
+; 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
--- /dev/null
+(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)
--- /dev/null
+% COMMAND-LINE: --incremental
+% EXPECT: unsat
+% EXPECT: sat
+% EXPECT: unsat
+% EXPECT: unsat
+% EXIT: 20
--- /dev/null
+(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)
--- /dev/null
+% COMMAND-LINE: --incremental
+% EXPECT: sat
+% EXPECT: unsat
+% EXIT: 20
--- /dev/null
+(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)
--- /dev/null
+% COMMAND-LINE: --incremental
+% EXPECT: unsat
+% EXPECT: sat
+% EXPECT: unsat
+% EXPECT: sat
+% EXPECT: unsat
+% EXPECT: unsat
+% EXIT: 20
--- /dev/null
+(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
--- /dev/null
+% COMMAND-LINE: --incremental --simplification=none
+% EXPECT: sat
+% EXPECT: unsat
+% EXIT: 20
projects / cvc5.git / commitdiff