Commit 3dbc21af authored by Pascal Fontaine's avatar Pascal Fontaine
Browse files

Adding benchmarks from pending

parent d9d67f15
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
(set-info :smt-lib-version 2.6)
(set-logic BV)
(set-info :source |
Generated by the tool Ultimate Automizer [1,2] which implements
an automata theoretic approach [3] to software verification.
This SMT script belongs to a set of SMT scripts that was generated by
applying Ultimate Automizer to benchmarks [4] from the SV-COMP 2017 [5,6].
This script might _not_ contain all SMT commands that are used by
Ultimate Automizer. In order to satisfy the restrictions of
the SMT-COMP we have to drop e.g., the commands for getting
values (resp. models), unsatisfiable cores and interpolants.
2017-05-01, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Wen Chen, Daniel Dietsch, Marius Greitschus,
Alexander Nutz, Betim Musa, Claus Schätzle, Christian Schilling,
Frank Schüssele, Andreas Podelski:
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare
Automata - (Competition Contribution). TACAS (2) 2017: 394-398
[3] Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Software Model
Checking for People Who Love Automata. CAV 2013:36-52
[4] https://github.com/sosy-lab/sv-benchmarks
[5] Dirk Beyer: Software Verification with Validation of Results -
(Report on SV-COMP 2017). TACAS (2) 2017: 331-349
[6] https://sv-comp.sosy-lab.org/2017/
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun |c_main_#t~nondet0| () (_ BitVec 32))
(declare-fun c_main_~y~5 () (_ BitVec 32))
(declare-fun c_main_~y~5_primed () (_ BitVec 32))
(declare-fun |c___VERIFIER_assert_#in~cond| () (_ BitVec 32))
(declare-fun |c___VERIFIER_assert_#in~cond_primed| () (_ BitVec 32))
(declare-fun c___VERIFIER_assert_~cond () (_ BitVec 32))
(declare-fun c___VERIFIER_assert_~cond_primed () (_ BitVec 32))
(push 1)
(check-sat)
(pop 1)
(push 1)
(check-sat)
(pop 1)
(push 1)
(check-sat)
(pop 1)
(push 1)
(check-sat)
(pop 1)
(push 1)
(assert false)
(check-sat)
(pop 1)
(push 1)
(declare-fun |v_main_#res_1_const_591105527| () (_ BitVec 32))
(assert (let ((|v_main_#res_1| |v_main_#res_1_const_591105527|)) (= |v_main_#res_1| (_ bv0 32))))
(check-sat)
(pop 1)
(push 1)
(declare-fun v_main_~y~5_1_const_-2023643558 () (_ BitVec 32))
(assert (let ((v_main_~y~5_1 v_main_~y~5_1_const_-2023643558)) (= v_main_~y~5_1 (_ bv1 32))))
(check-sat)
(pop 1)
(push 1)
(check-sat)
(pop 1)
(push 1)
(check-sat)
(pop 1)
(push 1)
(assert false)
(check-sat)
(pop 1)
(push 1)
(declare-fun |v_main_#t~nondet0_2_const_-747887338| () (_ BitVec 32))
(declare-fun v_main_~y~5_4_const_-2023643553 () (_ BitVec 32))
(declare-fun v_main_~y~5_3_const_-2023643560 () (_ BitVec 32))
(assert (let ((|v_main_#t~nondet0_2| |v_main_#t~nondet0_2_const_-747887338|) (v_main_~y~5_4 v_main_~y~5_4_const_-2023643553) (v_main_~y~5_3 v_main_~y~5_3_const_-2023643560)) (= v_main_~y~5_3 (bvadd (bvmul (_ bv2 32) |v_main_#t~nondet0_2|) v_main_~y~5_4))))
(check-sat)
(pop 1)
(push 1)
(check-sat)
(pop 1)
(push 1)
(declare-fun v___VERIFIER_assert_~cond_1_const_-2004088190 () (_ BitVec 32))
(declare-fun |v___VERIFIER_assert_#in~cond_1_const_-656375880| () (_ BitVec 32))
(assert (let ((v___VERIFIER_assert_~cond_1 v___VERIFIER_assert_~cond_1_const_-2004088190) (|v___VERIFIER_assert_#in~cond_1| |v___VERIFIER_assert_#in~cond_1_const_-656375880|)) (= v___VERIFIER_assert_~cond_1 |v___VERIFIER_assert_#in~cond_1|)))
(check-sat)
(pop 1)
(push 1)
(declare-fun v___VERIFIER_assert_~cond_2_const_-2004088191 () (_ BitVec 32))
(assert (let ((v___VERIFIER_assert_~cond_2 v___VERIFIER_assert_~cond_2_const_-2004088191)) (= v___VERIFIER_assert_~cond_2 (_ bv0 32))))
(check-sat)
(pop 1)
(push 1)
(check-sat)
(pop 1)
(push 1)
(assert false)
(check-sat)
(pop 1)
(push 1)
(declare-fun v___VERIFIER_assert_~cond_3_const_-2004088192 () (_ BitVec 32))
(assert (let ((v___VERIFIER_assert_~cond_3 v___VERIFIER_assert_~cond_3_const_-2004088192)) (not (= v___VERIFIER_assert_~cond_3 (_ bv0 32)))))
(check-sat)
(pop 1)
(push 1)
(check-sat)
(pop 1)
(push 1)
(assert (distinct c___VERIFIER_assert_~cond (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(assert (= c___VERIFIER_assert_~cond (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(declare-fun __VERIFIER_assert_~cond_const_1478984107 () (_ BitVec 32))
(push 1)
(assert (not (distinct __VERIFIER_assert_~cond_const_1478984107 (_ bv0 32))))
(check-sat)
(pop 1)
(push 1)
(assert (distinct __VERIFIER_assert_~cond_const_1478984107 (_ bv0 32)))
(check-sat)
(pop 1)
(pop 1)
(push 1)
(assert (distinct |c___VERIFIER_assert_#in~cond| (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(assert (= |c___VERIFIER_assert_#in~cond| (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct |c___VERIFIER_assert_#in~cond| (_ bv0 32)))
(assert (= c___VERIFIER_assert_~cond (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct c___VERIFIER_assert_~cond (_ bv0 32)))
(assert (= |c___VERIFIER_assert_#in~cond| (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(declare-fun |__VERIFIER_assert_#in~cond_const_-1053858157| () (_ BitVec 32))
(push 1)
(assert (not (distinct |__VERIFIER_assert_#in~cond_const_-1053858157| (_ bv0 32))))
(check-sat)
(pop 1)
(push 1)
(assert (distinct |__VERIFIER_assert_#in~cond_const_-1053858157| (_ bv0 32)))
(check-sat)
(pop 1)
(pop 1)
(push 1)
(assert (distinct c_main_~y~5 (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(assert (= c_main_~y~5 (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct c_main_~y~5 (_ bv0 32)))
(assert (= c___VERIFIER_assert_~cond (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct c___VERIFIER_assert_~cond (_ bv0 32)))
(assert (= c_main_~y~5 (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct c_main_~y~5 (_ bv0 32)))
(assert (= |c___VERIFIER_assert_#in~cond| (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct |c___VERIFIER_assert_#in~cond| (_ bv0 32)))
(assert (= c_main_~y~5 (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(declare-fun main_~y~5_const_-993907773 () (_ BitVec 32))
(push 1)
(assert (not (distinct main_~y~5_const_-993907773 (_ bv0 32))))
(check-sat)
(pop 1)
(push 1)
(assert (distinct main_~y~5_const_-993907773 (_ bv0 32)))
(check-sat)
(pop 1)
(pop 1)
(push 1)
(declare-fun main_~y~5_const_-993907773 () (_ BitVec 32))
(declare-fun |main_#t~nondet0_const_1527797368| () (_ BitVec 32))
(push 1)
(assert (not (distinct (bvadd main_~y~5_const_-993907773 (bvmul (_ bv2 32) |main_#t~nondet0_const_1527797368|)) (_ bv0 32))))
(check-sat)
(pop 1)
(push 1)
(assert (distinct (bvadd main_~y~5_const_-993907773 (bvmul (_ bv2 32) |main_#t~nondet0_const_1527797368|)) (_ bv0 32)))
(check-sat)
(pop 1)
(pop 1)
(push 1)
(assert (forall ((|main_#t~nondet0| (_ BitVec 32))) (distinct (bvadd c_main_~y~5 (bvmul (_ bv2 32) |main_#t~nondet0|)) (_ bv0 32))))
(check-sat)
(pop 1)
(push 1)
(assert (not (forall ((|main_#t~nondet0| (_ BitVec 32))) (distinct (bvadd c_main_~y~5 (bvmul (_ bv2 32) |main_#t~nondet0|)) (_ bv0 32)))))
(check-sat)
(pop 1)
(push 1)
(assert (forall ((|main_#t~nondet0| (_ BitVec 32))) (distinct (bvadd c_main_~y~5 (bvmul (_ bv2 32) |main_#t~nondet0|)) (_ bv0 32))))
(assert (= c___VERIFIER_assert_~cond (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct c___VERIFIER_assert_~cond (_ bv0 32)))
(assert (not (forall ((|main_#t~nondet0| (_ BitVec 32))) (distinct (bvadd c_main_~y~5 (bvmul (_ bv2 32) |main_#t~nondet0|)) (_ bv0 32)))))
(check-sat)
(pop 1)
(push 1)
(assert (forall ((|main_#t~nondet0| (_ BitVec 32))) (distinct (bvadd c_main_~y~5 (bvmul (_ bv2 32) |main_#t~nondet0|)) (_ bv0 32))))
(assert (= |c___VERIFIER_assert_#in~cond| (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct |c___VERIFIER_assert_#in~cond| (_ bv0 32)))
(assert (not (forall ((|main_#t~nondet0| (_ BitVec 32))) (distinct (bvadd c_main_~y~5 (bvmul (_ bv2 32) |main_#t~nondet0|)) (_ bv0 32)))))
(check-sat)
(pop 1)
(push 1)
(assert (forall ((|main_#t~nondet0| (_ BitVec 32))) (distinct (bvadd c_main_~y~5 (bvmul (_ bv2 32) |main_#t~nondet0|)) (_ bv0 32))))
(assert (= c_main_~y~5 (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct c_main_~y~5 (_ bv0 32)))
(assert (not (forall ((|main_#t~nondet0| (_ BitVec 32))) (distinct (bvadd c_main_~y~5 (bvmul (_ bv2 32) |main_#t~nondet0|)) (_ bv0 32)))))
(check-sat)
(pop 1)
(push 1)
(declare-fun main_~y~5_const_-993907773 () (_ BitVec 32))
(push 1)
(assert (not (forall ((|main_#t~nondet0| (_ BitVec 32))) (distinct (bvadd main_~y~5_const_-993907773 (bvmul (_ bv2 32) |main_#t~nondet0|)) (_ bv0 32)))))
(check-sat)
(pop 1)
(push 1)
(assert (forall ((|main_#t~nondet0| (_ BitVec 32))) (distinct (bvadd main_~y~5_const_-993907773 (bvmul (_ bv2 32) |main_#t~nondet0|)) (_ bv0 32))))
(check-sat)
(pop 1)
(pop 1)
(push 1)
(declare-fun main_~y~5_const_-993907773 () (_ BitVec 32))
(declare-fun |main_#t~nondet0_const_1527797368| () (_ BitVec 32))
(push 1)
(assert (not (distinct (bvadd main_~y~5_const_-993907773 (bvmul (_ bv2 32) |main_#t~nondet0_const_1527797368|)) (_ bv0 32))))
(check-sat)
(pop 1)
(push 1)
(assert (distinct (bvadd main_~y~5_const_-993907773 (bvmul (_ bv2 32) |main_#t~nondet0_const_1527797368|)) (_ bv0 32)))
(check-sat)
(pop 1)
(pop 1)
(push 1)
(declare-fun |main_#t~nondet0_const_1527797368| () (_ BitVec 32))
(assert (let ((|main_#t~nondet0| |main_#t~nondet0_const_1527797368|)) (= (bvadd (bvmul (_ bv2 32) |main_#t~nondet0|) (_ bv1 32)) (_ bv0 32))))
(check-sat)
(pop 1)
(push 1)
(push 1)
(assert false)
(check-sat)
(pop 1)
(pop 1)
(push 1)
(push 1)
(assert false)
(check-sat)
(pop 1)
(pop 1)
(push 1)
(push 1)
(assert false)
(check-sat)
(pop 1)
(pop 1)
(push 1)
(push 1)
(assert false)
(check-sat)
(pop 1)
(pop 1)
(push 1)
(assert (= c_main_~y~5_primed (_ bv1 32)))
(push 1)
(push 1)
(assert (not (distinct c_main_~y~5_primed (_ bv0 32))))
(check-sat)
(pop 1)
(pop 1)
(pop 1)
(push 1)
(assert (= c_main_~y~5_primed (bvadd (bvmul (_ bv2 32) |c_main_#t~nondet0|) c_main_~y~5)))
(push 1)
(assert (forall ((|main_#t~nondet0| (_ BitVec 32))) (distinct (bvadd c_main_~y~5 (bvmul (_ bv2 32) |main_#t~nondet0|)) (_ bv0 32))))
(push 1)
(check-sat)
(pop 1)
(pop 1)
(pop 1)
(push 1)
(assert (= c___VERIFIER_assert_~cond_primed |c___VERIFIER_assert_#in~cond|))
(push 1)
(assert (distinct |c___VERIFIER_assert_#in~cond| (_ bv0 32)))
(push 1)
(check-sat)
(pop 1)
(push 1)
(assert (not (distinct c_main_~y~5 (_ bv0 32))))
(check-sat)
(pop 1)
(pop 1)
(pop 1)
(push 1)
(assert (and (distinct |c___VERIFIER_assert_#in~cond| (_ bv0 32)) (distinct c___VERIFIER_assert_~cond (_ bv0 32))))
(check-sat)
(pop 1)
(push 1)
(assert (not (and (distinct |c___VERIFIER_assert_#in~cond| (_ bv0 32)) (distinct c___VERIFIER_assert_~cond (_ bv0 32)))))
(check-sat)
(pop 1)
(push 1)
(assert (and (distinct |c___VERIFIER_assert_#in~cond| (_ bv0 32)) (distinct c___VERIFIER_assert_~cond (_ bv0 32))))
(assert (= c_main_~y~5 (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(declare-fun |__VERIFIER_assert_#in~cond_const_-1053858157| () (_ BitVec 32))
(declare-fun __VERIFIER_assert_~cond_const_1478984107 () (_ BitVec 32))
(push 1)
(assert (not (and (distinct |__VERIFIER_assert_#in~cond_const_-1053858157| (_ bv0 32)) (distinct __VERIFIER_assert_~cond_const_1478984107 (_ bv0 32)))))
(check-sat)
(pop 1)
(push 1)
(assert (and (distinct |__VERIFIER_assert_#in~cond_const_-1053858157| (_ bv0 32)) (distinct __VERIFIER_assert_~cond_const_1478984107 (_ bv0 32))))
(check-sat)
(pop 1)
(push 1)
(push 1)
(assert (distinct __VERIFIER_assert_~cond_const_1478984107 (_ bv0 32)))
(push 1)
(assert (not (distinct |__VERIFIER_assert_#in~cond_const_-1053858157| (_ bv0 32))))
(check-sat)
(pop 1)
(push 1)
(assert (distinct |__VERIFIER_assert_#in~cond_const_-1053858157| (_ bv0 32)))
(check-sat)
(pop 1)
(pop 1)
(assert (distinct |__VERIFIER_assert_#in~cond_const_-1053858157| (_ bv0 32)))
(push 1)
(assert (not (distinct __VERIFIER_assert_~cond_const_1478984107 (_ bv0 32))))
(check-sat)
(pop 1)
(push 1)
(assert (distinct __VERIFIER_assert_~cond_const_1478984107 (_ bv0 32)))
(check-sat)
(pop 1)
(pop 1)
(pop 1)
(push 1)
(assert (not (= c___VERIFIER_assert_~cond (_ bv0 32))))
(push 1)
(assert (and (distinct |c___VERIFIER_assert_#in~cond| (_ bv0 32)) (distinct c___VERIFIER_assert_~cond (_ bv0 32))))
(push 1)
(check-sat)
(pop 1)
(push 1)
(assert (not (distinct c_main_~y~5 (_ bv0 32))))
(check-sat)
(pop 1)
(pop 1)
(pop 1)
(push 1)
(declare-fun c_main_~y~5_Hier () (_ BitVec 32))
(assert (= |c___VERIFIER_assert_#in~cond| (ite (not (= c_main_~y~5_Hier (_ bv0 32))) (_ bv1 32) (_ bv0 32))))
(push 1)
(assert (and (distinct |c___VERIFIER_assert_#in~cond| (_ bv0 32)) (distinct c___VERIFIER_assert_~cond (_ bv0 32))))
(push 1)
(assert (distinct c_main_~y~5_Hier (_ bv0 32)))
(push 1)
(check-sat)
(pop 1)
(push 1)
(declare-fun |c___VERIFIER_assert_#in~cond_Hier| () (_ BitVec 32))
(assert (not (distinct |c___VERIFIER_assert_#in~cond_Hier| (_ bv0 32))))
(check-sat)
(pop 1)
(push 1)
(assert (not (forall ((|main_#t~nondet0| (_ BitVec 32))) (distinct (bvadd c_main_~y~5_Hier (bvmul (_ bv2 32) |main_#t~nondet0|)) (_ bv0 32)))))
(check-sat)
(pop 1)
(push 1)
(declare-fun c___VERIFIER_assert_~cond_Hier () (_ BitVec 32))
(assert (not (distinct c___VERIFIER_assert_~cond_Hier (_ bv0 32))))
(check-sat)
(pop 1)
(pop 1)
(pop 1)
(pop 1)
(push 1)
(assert (= |c___VERIFIER_assert_#in~cond_primed| (ite (not (= c_main_~y~5 (_ bv0 32))) (_ bv1 32) (_ bv0 32))))
(push 1)
(push 1)
(assert (not (distinct |c___VERIFIER_assert_#in~cond_primed| (_ bv0 32))))
(check-sat)
(pop 1)
(pop 1)
(pop 1)
(push 1)
(assert (= c___VERIFIER_assert_~cond_primed |c___VERIFIER_assert_#in~cond|))
(push 1)
(push 1)
(assert (not (distinct |c___VERIFIER_assert_#in~cond| (_ bv0 32))))
(check-sat)
(pop 1)
(push 1)
(assert (not (distinct c___VERIFIER_assert_~cond_primed (_ bv0 32))))
(check-sat)
(pop 1)
(pop 1)
(pop 1)
(push 1)
(assert (= c___VERIFIER_assert_~cond (_ bv0 32)))
(push 1)
(push 1)
(assert (not (distinct c___VERIFIER_assert_~cond (_ bv0 32))))
(check-sat)
(pop 1)
(pop 1)
(pop 1)
(push 1)
(assert (not (= c___VERIFIER_assert_~cond (_ bv0 32))))
(push 1)
(push 1)
(assert (not (distinct c___VERIFIER_assert_~cond (_ bv0 32))))
(check-sat)
(pop 1)
(pop 1)
(pop 1)
(push 1)
(assert (distinct c___VERIFIER_assert_~cond (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(assert (= c___VERIFIER_assert_~cond (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(declare-fun __VERIFIER_assert_~cond_const_1478984107 () (_ BitVec 32))
(push 1)
(assert (not (distinct __VERIFIER_assert_~cond_const_1478984107 (_ bv0 32))))
(check-sat)
(pop 1)
(push 1)
(assert (distinct __VERIFIER_assert_~cond_const_1478984107 (_ bv0 32)))
(check-sat)
(pop 1)
(pop 1)
(push 1)
(assert (distinct |c___VERIFIER_assert_#in~cond| (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(assert (= |c___VERIFIER_assert_#in~cond| (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct |c___VERIFIER_assert_#in~cond| (_ bv0 32)))
(assert (= c___VERIFIER_assert_~cond (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct c___VERIFIER_assert_~cond (_ bv0 32)))
(assert (= |c___VERIFIER_assert_#in~cond| (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(declare-fun |__VERIFIER_assert_#in~cond_const_-1053858157| () (_ BitVec 32))
(push 1)
(assert (not (distinct |__VERIFIER_assert_#in~cond_const_-1053858157| (_ bv0 32))))
(check-sat)
(pop 1)
(push 1)
(assert (distinct |__VERIFIER_assert_#in~cond_const_-1053858157| (_ bv0 32)))
(check-sat)
(pop 1)
(pop 1)
(push 1)
(assert (distinct c_main_~y~5 (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(assert (= c_main_~y~5 (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct c_main_~y~5 (_ bv0 32)))
(assert (= c___VERIFIER_assert_~cond (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct c___VERIFIER_assert_~cond (_ bv0 32)))
(assert (= c_main_~y~5 (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct c_main_~y~5 (_ bv0 32)))
(assert (= |c___VERIFIER_assert_#in~cond| (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct |c___VERIFIER_assert_#in~cond| (_ bv0 32)))
(assert (= c_main_~y~5 (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(declare-fun main_~y~5_const_-993907773 () (_ BitVec 32))
(push 1)
(assert (not (distinct main_~y~5_const_-993907773 (_ bv0 32))))
(check-sat)
(pop 1)
(push 1)
(assert (distinct main_~y~5_const_-993907773 (_ bv0 32)))
(check-sat)
(pop 1)
(pop 1)
(push 1)
(declare-fun main_~y~5_const_-993907773 () (_ BitVec 32))
(declare-fun |main_#t~nondet0_const_1527797368| () (_ BitVec 32))
(push 1)
(assert (not (distinct (bvadd main_~y~5_const_-993907773 (bvmul (_ bv2 32) |main_#t~nondet0_const_1527797368|)) (_ bv0 32))))
(check-sat)
(pop 1)
(push 1)
(assert (distinct (bvadd main_~y~5_const_-993907773 (bvmul (_ bv2 32) |main_#t~nondet0_const_1527797368|)) (_ bv0 32)))
(check-sat)
(pop 1)
(pop 1)
(push 1)
(assert (forall ((|main_#t~nondet0| (_ BitVec 32))) (distinct (bvadd c_main_~y~5 (bvmul (_ bv2 32) |main_#t~nondet0|)) (_ bv0 32))))
(check-sat)
(pop 1)
(push 1)
(assert (not (forall ((|main_#t~nondet0| (_ BitVec 32))) (distinct (bvadd c_main_~y~5 (bvmul (_ bv2 32) |main_#t~nondet0|)) (_ bv0 32)))))
(check-sat)
(pop 1)
(push 1)
(assert (forall ((|main_#t~nondet0| (_ BitVec 32))) (distinct (bvadd c_main_~y~5 (bvmul (_ bv2 32) |main_#t~nondet0|)) (_ bv0 32))))
(assert (= c___VERIFIER_assert_~cond (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct c___VERIFIER_assert_~cond (_ bv0 32)))
(assert (not (forall ((|main_#t~nondet0| (_ BitVec 32))) (distinct (bvadd c_main_~y~5 (bvmul (_ bv2 32) |main_#t~nondet0|)) (_ bv0 32)))))
(check-sat)
(pop 1)
(push 1)
(assert (forall ((|main_#t~nondet0| (_ BitVec 32))) (distinct (bvadd c_main_~y~5 (bvmul (_ bv2 32) |main_#t~nondet0|)) (_ bv0 32))))
(assert (= |c___VERIFIER_assert_#in~cond| (_ bv0 32)))
(check-sat)
(pop 1)
(push 1)
(assert (distinct |c___VERIFIER_assert_#in~cond| (_ bv0 32)))
(assert (not (forall ((|main_#t~nondet0| (_ BitVec 32))) (distinct (bvadd c_main_~y~5 (bvmul (_ bv2 32) |main_#t~nondet0|)) (_ bv0 32)))))
(check-sat)
(pop 1)
(push 1)