smtinterpol-AssertionError-ArrayTheory-merge.smt2

(set-option :random-seed 42)
(set-option :produce-interpolants true)
(set-option :produce-models true)
(set-option :produce-unsat-cores true)
(set-logic QF_AUFLIRA)
(declare-fun Integer__*_ (Int Int) Int)
(declare-fun Integer__/_ (Int Int) Int)
(declare-fun Integer__%_ (Int Int) Int)
(declare-fun _&_ (Int Int) Int)
(declare-fun _!!_ (Int Int) Int)
(declare-fun _^_ (Int Int) Int)
(declare-fun _~_ (Int) Int)
(declare-fun _<<_ (Int Int) Int)
(declare-fun _>>_ (Int Int) Int)
(declare-fun Rational__*_ (Real Real) Real)
(declare-fun Rational__/_ (Real Real) Real)
(declare-fun Rational__%_ (Real Real) Real)
(declare-fun __isSubnormal__ (Real) Bool)
(declare-fun __NaN__ () Real)
(declare-fun __+Infinity__ () Real)
(declare-fun __-Infinity__ () Real)
(get-info :name)
(get-info :version)
(declare-fun __string__ (Int) Int)
(declare-fun |__ADDRESS_OF_main::a| () Int)
(declare-fun |main::i@2| () Int)
(declare-fun |main::x@3| () Int)
(declare-fun |main::__retval__@2| () Int)
(declare-fun |main::y@3| () Int)
(declare-fun |main::x@4| () Int)
(declare-fun *signed_int@2 () (Array Int Int))
(declare-fun |__VERIFIER_assert::cond@2| () Int)
(declare-fun __VERIFIER_error () Int)
(push 1)
(assert (and (< |main::y@3| 100000) (= |__VERIFIER_assert::cond@2| (ite (<= (select *signed_int@2 (+ |__ADDRESS_OF_main::a| (* 4 |main::x@3|))) (select *signed_int@2 (+ |__ADDRESS_OF_main::a| (* 4 |main::y@3|)))) 1 0)) (= |__VERIFIER_assert::cond@2| 0)))
(check-sat)
(pop 1)
(get-option :random-seed)
(push 1)
(assert (! (and (= |main::i@2| 0) (> |__ADDRESS_OF_main::a| 0)) :named term_0))
(push 1)
(assert (! (and (not (< |main::i@2| 100000)) (= |main::x@3| 0)) :named term_1))
(push 1)
(assert (! (and (< |main::x@3| 100000) (= |main::y@3| (+ |main::x@3| 1))) :named term_2))
(push 1)
(assert (! (and (< |main::y@3| 100000) (= |__VERIFIER_assert::cond@2| (ite (<= (select *signed_int@2 (+ |__ADDRESS_OF_main::a| (* 4 |main::x@3|))) (select *signed_int@2 (+ |__ADDRESS_OF_main::a| (* 4 |main::y@3|)))) 1 0)) (= |__VERIFIER_assert::cond@2| 0)) :named term_3))
(check-sat)
(pop 4)
(declare-fun |__VERIFIER_assert::cond@1| () Int)
(declare-fun |__VERIFIER_assert::cond| () Int)
(declare-fun PRED0 () Bool)
(get-option :random-seed)
(push 1)
(assert (! (and (= |main::i@2| 0) (> |__ADDRESS_OF_main::a| 0)) :named term_4))
(push 1)
(assert (! (and (not (< |main::i@2| 100000)) (= |main::x@3| 0)) :named term_5))
(push 1)
(assert (! (and (< |main::x@3| 100000) (= |main::y@3| (+ |main::x@3| 1))) :named term_6))
(push 1)
(assert (! (and (< |main::y@3| 100000) (= |__VERIFIER_assert::cond@2| (ite (<= (select *signed_int@2 (+ |__ADDRESS_OF_main::a| (* 4 |main::x@3|))) (select *signed_int@2 (+ |__ADDRESS_OF_main::a| (* 4 |main::y@3|)))) 1 0)) (= |__VERIFIER_assert::cond@2| 0)) :named term_7))
(check-sat)
(get-interpolants term_4 (and term_5 term_6 term_7))
(get-interpolants (and term_5 term_4) (and term_6 term_7))
(get-interpolants (and term_6 term_5 term_4) term_7)
(pop 4)
(declare-fun |main::i| () Int)
(declare-fun PRED1 () Bool)
(declare-fun PRED2 () Bool)
(push 1)
(assert (and (= |main::i@2| 0) (> |__ADDRESS_OF_main::a| 0)))
(push 1)
(assert (= PRED1 (<= |main::i@2| 0)))
(check-allsat (PRED1))
(pop 2)
(push 1)
(assert (and (<= |main::i@2| 0) (not (< |main::i@2| 100000)) (= |main::x@3| 0)))
(check-sat)
(pop 1)
(declare-fun |main::k@2| () Int)
(declare-fun |main::s@2| () Int)
(declare-fun |main::tmp@2| () Int)
(declare-fun *signed_int@3 () (Array Int Int))
(declare-fun *signed_int@4 () (Array Int Int))
(declare-fun |main::tmp@1| () Int)
(declare-fun |main::i@3| () Int)
(push 1)
(assert (and (not (< |main::x@4| 100000)) (= |main::i@3| (+ |main::i@2| 1))))
(push 1)
(assert (= PRED1 (<= |main::i@3| 0)))
(check-allsat (PRED1))
(pop 2)
(declare-fun |main::x@5| () Int)
(push 1)
(assert (and (not (< |main::i@3| 100000)) (= |main::x@5| 0)))
(check-sat)
(pop 1)
(declare-fun |main::x@6| () Int)
(push 1)
(assert (and (not (< |main::y@3| 100000)) (= |main::x@6| (+ |main::x@5| 1))))
(check-sat)
(pop 1)
(push 1)
(assert (and (< |main::y@3| 100000) (= |__VERIFIER_assert::cond@2| (ite (<= (select *signed_int@4 (+ |__ADDRESS_OF_main::a| (* 4 |main::x@5|))) (select *signed_int@4 (+ |__ADDRESS_OF_main::a| (* 4 |main::y@3|)))) 1 0)) (= |__VERIFIER_assert::cond@2| 0)))
(check-sat)
(pop 1)
(get-option :random-seed)
(push 1)
(assert (! (and (= |main::i@2| 0) (> |__ADDRESS_OF_main::a| 0)) :named term_8))
(push 1)
(assert (! (and (< |main::i@2| 100000) (= |main::k@2| |main::i@2|) (= |main::s@2| (+ |main::i@2| 1))) :named term_9))
(push 1)
(assert (! (and (let ((.cse0 (not (< |main::k@2| 100000))) (.cse1 (= |main::s@2| |main::i@2|))) (or (let ((.cse2 (+ |__ADDRESS_OF_main::a| (* 4 |main::s@2|))) (.cse3 (+ |__ADDRESS_OF_main::a| (* 4 |main::i@2|)))) (and .cse0 (not .cse1) (= |main::tmp@2| (select *signed_int@2 .cse2)) (= *signed_int@3 (store *signed_int@2 .cse2 (select *signed_int@2 .cse3))) (= *signed_int@4 (store *signed_int@3 .cse3 |main::tmp@2|)))) (and .cse0 .cse1 (= *signed_int@4 *signed_int@2) (= |main::tmp@2| |main::tmp@1|)))) (= |main::x@3| 0)) :named term_10))
(push 1)
(assert (! (and (not (< |main::x@3| |main::i@2|)) (= |main::x@4| (+ |main::i@2| 1))) :named term_11))
(push 1)
(assert (! (and (not (< |main::x@4| 100000)) (= |main::i@3| (+ |main::i@2| 1))) :named term_12))
(push 1)
(assert (! (and (not (< |main::i@3| 100000)) (= |main::x@5| 0)) :named term_13))
(push 1)
(assert (! (and (< |main::x@5| 100000) (= |main::y@3| (+ |main::x@5| 1))) :named term_14))
(push 1)
(assert (! (and (< |main::y@3| 100000) (= |__VERIFIER_assert::cond@2| (ite (<= (select *signed_int@4 (+ |__ADDRESS_OF_main::a| (* 4 |main::x@5|))) (select *signed_int@4 (+ |__ADDRESS_OF_main::a| (* 4 |main::y@3|)))) 1 0)) (= |__VERIFIER_assert::cond@2| 0)) :named term_15))
(check-sat)
(get-interpolants term_8 (and term_9 term_10 term_11 term_12 term_13 term_14 term_15))
(get-interpolants (and term_9 term_8) (and term_10 term_11 term_12 term_13 term_14 term_15))
(get-interpolants (and term_10 term_9 term_8) (and term_11 term_12 term_13 term_14 term_15))
(get-interpolants (and term_10 term_11 term_9 term_8) (and term_12 term_13 term_14 term_15))
(get-interpolants (and term_12 term_10 term_11 term_9 term_8) (and term_13 term_14 term_15))
(get-interpolants (and term_12 term_13 term_10 term_11 term_9 term_8) (and term_14 term_15))
(get-interpolants (and term_14 term_12 term_13 term_10 term_11 term_9 term_8) term_15)
(pop 8)
(declare-fun |main::x| () Int)
(declare-fun PRED3 () Bool)
(push 1)
(assert (and (<= |main::i@2| 0) (< |main::i@2| 100000) (= |main::k@2| |main::i@2|) (= |main::s@2| (+ |main::i@2| 1))))
(push 1)
(assert (= PRED1 (<= |main::i@2| 0)))
(check-allsat (PRED1))
(pop 2)
(push 1)
(assert (and (<= |main::i@2| 0) (let ((.cse0 (not (< |main::k@2| 100000))) (.cse1 (= |main::s@2| |main::i@2|))) (or (let ((.cse2 (+ |__ADDRESS_OF_main::a| (* 4 |main::s@2|))) (.cse3 (+ |__ADDRESS_OF_main::a| (* 4 |main::i@2|)))) (and .cse0 (not .cse1) (= |main::tmp@2| (select *signed_int@2 .cse2)) (= *signed_int@3 (store *signed_int@2 .cse2 (select *signed_int@2 .cse3))) (= *signed_int@4 (store *signed_int@3 .cse3 |main::tmp@2|)))) (and .cse0 .cse1 (= *signed_int@4 *signed_int@2) (= |main::tmp@2| |main::tmp@1|)))) (= |main::x@3| 0)))
(push 1)
(assert (= PRED1 (<= |main::i@2| 0)))
(check-allsat (PRED1))
(pop 2)