Skip to content
GitLab
Commit 03648c4a authored by Mathias Preiner's avatar Mathias Preiner
Browse files

Squashed commit of the following: 

commit b4c02e6e
Author: Mathias Preiner <mathias.preiner@gmail.com>
Date:   Fri Apr 24 22:44:48 2020 -0700

    Move benchmarks from pending repository.
parent 273e1c0c
Expand all Hide whitespace changes
Inline Side-by-side
20190429-UltimateAutomizerSvcomp2019/avg20_true-unreach-call.i_0.smt2 0 → 100644
View file @ 03648c4a
(set-info :smt-lib-version 2.6)
(set-logic QF_ALIA)
(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 2019 [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.
2019-04-27, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus,
Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian
Schilling, Tanja Schindler, Andreas Podelski: Ultimate Automizer
and the Search for Perfect Interpolants - (Competition Contribution).
TACAS (2) 2018: 447-451
[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: Automatic Verification of C and Java Programs: SV-COMP 2019.
TACAS (3) 2019: 133-155
[6] https://sv-comp.sosy-lab.org/2019/
|")
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun |v_#memory_int_110| () (Array Int (Array Int Int)))
(declare-fun |main_~#x~0.base| () Int)
(declare-fun |main_~#x~0.offset| () Int)
(declare-fun main_~ret~1 () Int)
(declare-fun |#memory_int| () (Array Int (Array Int Int)))
(assert (let ((.cse44 (select |v_#memory_int_110| |main_~#x~0.base|)) (.cse46 (+ |main_~#x~0.offset| 4))) (let ((.cse51 (+ |main_~#x~0.offset| 72)) (.cse52 (+ |main_~#x~0.offset| 76)) (.cse56 (+ |main_~#x~0.offset| 44)) (.cse57 (+ |main_~#x~0.offset| 68)) (.cse63 (+ |main_~#x~0.offset| 24)) (.cse62 (+ |main_~#x~0.offset| 20)) (.cse59 (+ |main_~#x~0.offset| 40)) (.cse45 (select .cse44 .cse46)) (.cse54 (+ |main_~#x~0.offset| 8)) (.cse50 (+ |main_~#x~0.offset| 28)) (.cse65 (+ |main_~#x~0.offset| 36)) (.cse61 (+ |main_~#x~0.offset| 32)) (.cse58 (+ |main_~#x~0.offset| 60)) (.cse55 (+ |main_~#x~0.offset| 52)) (.cse53 (+ |main_~#x~0.offset| 64)) (.cse66 (+ |main_~#x~0.offset| 16)) (.cse60 (+ |main_~#x~0.offset| 56)) (.cse64 (+ |main_~#x~0.offset| 48)) (.cse47 (select .cse44 |main_~#x~0.offset|)) (.cse49 (+ |main_~#x~0.offset| 12))) (let ((.cse42 (+ (select .cse44 .cse51) (select .cse44 .cse52) (select .cse44 .cse56) (select .cse44 .cse57) (select .cse44 .cse63) (select .cse44 .cse62) (select .cse44 .cse59) .cse45 (select .cse44 .cse54) (select .cse44 .cse50) (select .cse44 .cse65) (select .cse44 .cse61) (select .cse44 .cse58) (select .cse44 .cse55) (select .cse44 .cse53) (select .cse44 .cse66) (select .cse44 .cse60) (select .cse44 .cse64) .cse47 (select .cse44 .cse49)))) (let ((.cse67 (div .cse42 20))) (let ((.cse38 (= |main_~#x~0.offset| 0)) (.cse4 (+ main_~ret~1 4294967296)) (.cse43 (mod .cse67 4294967296)) (.cse41 (mod (+ .cse67 1) 4294967296)) (.cse30 (= (mod .cse42 20) 0)) (.cse48 (select |#memory_int| |main_~#x~0.base|))) (let ((.cse5 (select .cse48 .cse66)) (.cse7 (select .cse48 .cse65)) (.cse6 (select .cse48 .cse64)) (.cse8 (select .cse48 .cse63)) (.cse9 (select .cse48 .cse62)) (.cse10 (select .cse48 .cse61)) (.cse11 (select .cse48 .cse60)) (.cse12 (select .cse48 .cse59)) (.cse13 (select .cse48 .cse58)) (.cse14 (select .cse48 .cse57)) (.cse15 (select .cse48 .cse56)) (.cse16 (select .cse48 .cse55)) (.cse17 (select .cse48 |main_~#x~0.offset|)) (.cse18 (select .cse48 .cse54)) (.cse19 (select .cse48 .cse53)) (.cse20 (select .cse48 .cse52)) (.cse21 (select .cse48 .cse46)) (.cse22 (select .cse48 .cse51)) (.cse23 (select .cse48 .cse50)) (.cse24 (select .cse48 .cse49)) (.cse34 (not .cse30)) (.cse29 (not (= main_~ret~1 .cse41))) (.cse28 (not (<= .cse43 2147483647))) (.cse35 (not (= .cse43 main_~ret~1))) (.cse26 (not (<= .cse41 2147483647))) (.cse40 (not (<= 0 .cse42))) (.cse37 (not (= .cse43 .cse4))) (.cse39 (not (< 2147483647 .cse41))) (.cse25 (not (= (store |v_#memory_int_110| |main_~#x~0.base| (store (store .cse44 |main_~#x~0.offset| .cse45) .cse46 .cse47)) |#memory_int|))) (.cse36 (not (< 2147483647 .cse43))) (.cse27 (not (< .cse42 0))) (.cse2 (not .cse38))) (and (let ((.cse3 (+ .cse5 .cse6 .cse7 .cse8 .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24))) (let ((.cse1 (div .cse3 20))) (let ((.cse0 (mod .cse1 4294967296))) (or (not (< 2147483647 .cse0)) (not (< 2147483647 (mod (+ .cse1 1) 4294967296))) .cse2 (not (= (mod .cse3 20) 0)) (not (= .cse4 .cse0)))))) (or .cse25 .cse26 .cse27 .cse2 .cse28 .cse29 .cse30) (let ((.cse31 (+ .cse5 .cse7 .cse6 .cse8 .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24))) (let ((.cse32 (div .cse31 20))) (let ((.cse33 (mod (+ .cse32 1) 4294967296))) (or (= 0 (mod .cse31 20)) (not (< .cse31 0)) (not (<= (mod .cse32 4294967296) 2147483647)) .cse2 (not (= .cse33 .cse4)) (not (< 2147483647 .cse33)))))) (or .cse25 .cse26 .cse2 .cse28 .cse34 .cse35) (or .cse25 .cse26 .cse36 .cse2 .cse37 .cse34) .cse38 (or .cse39 .cse25 .cse40 .cse2 .cse28 .cse35) (or .cse25 .cse26 .cse36 .cse27 .cse2 .cse29 .cse30) (or .cse25 .cse26 .cse40 .cse2 .cse28 .cse35) (or .cse39 .cse25 .cse40 .cse36 .cse2 .cse37) (or .cse25 .cse26 .cse40 .cse36 .cse2 .cse37) (or .cse39 .cse25 .cse36 .cse27 .cse2 (not (= .cse4 .cse41)) .cse30)))))))))
(assert (not (let ((.cse0 (select |v_#memory_int_110| |main_~#x~0.base|))) (= (select .cse0 (+ |main_~#x~0.offset| 48)) (select .cse0 (+ |main_~#x~0.offset| 28))))))
(check-sat)
(exit)
20190429-UltimateAutomizerSvcomp2019/avg20_true-unreach-call.i_1.smt2 0 → 100644
View file @ 03648c4a
(set-info :smt-lib-version 2.6)
(set-logic QF_ALIA)
(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 2019 [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.
2019-04-27, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus,
Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian
Schilling, Tanja Schindler, Andreas Podelski: Ultimate Automizer
and the Search for Perfect Interpolants - (Competition Contribution).
TACAS (2) 2018: 447-451
[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: Automatic Verification of C and Java Programs: SV-COMP 2019.
TACAS (3) 2019: 133-155
[6] https://sv-comp.sosy-lab.org/2019/
|")
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun |v_#memory_int_110| () (Array Int (Array Int Int)))
(declare-fun |main_~#x~0.base| () Int)
(declare-fun |main_~#x~0.offset| () Int)
(declare-fun main_~ret~1 () Int)
(declare-fun |#memory_int| () (Array Int (Array Int Int)))
(assert (let ((.cse46 (select |v_#memory_int_110| |main_~#x~0.base|)) (.cse48 (+ |main_~#x~0.offset| 4))) (let ((.cse52 (select |#memory_int| |main_~#x~0.base|)) (.cse55 (+ |main_~#x~0.offset| 72)) (.cse56 (+ |main_~#x~0.offset| 76)) (.cse60 (+ |main_~#x~0.offset| 44)) (.cse61 (+ |main_~#x~0.offset| 68)) (.cse67 (+ |main_~#x~0.offset| 24)) (.cse66 (+ |main_~#x~0.offset| 20)) (.cse64 (+ |main_~#x~0.offset| 40)) (.cse47 (select .cse46 .cse48)) (.cse58 (+ |main_~#x~0.offset| 8)) (.cse53 (+ |main_~#x~0.offset| 28)) (.cse69 (+ |main_~#x~0.offset| 36)) (.cse65 (+ |main_~#x~0.offset| 32)) (.cse62 (+ |main_~#x~0.offset| 60)) (.cse59 (+ |main_~#x~0.offset| 52)) (.cse57 (+ |main_~#x~0.offset| 64)) (.cse70 (+ |main_~#x~0.offset| 16)) (.cse63 (+ |main_~#x~0.offset| 56)) (.cse68 (+ |main_~#x~0.offset| 48)) (.cse49 (select .cse46 |main_~#x~0.offset|)) (.cse54 (+ |main_~#x~0.offset| 12))) (let ((.cse44 (+ (select .cse46 .cse55) (select .cse46 .cse56) (select .cse46 .cse60) (select .cse46 .cse61) (select .cse46 .cse67) (select .cse46 .cse66) (select .cse46 .cse64) .cse47 (select .cse46 .cse58) (select .cse46 .cse53) (select .cse46 .cse69) (select .cse46 .cse65) (select .cse46 .cse62) (select .cse46 .cse59) (select .cse46 .cse57) (select .cse46 .cse70) (select .cse46 .cse63) (select .cse46 .cse68) .cse49 (select .cse46 .cse54))) (.cse5 (select .cse52 .cse70)) (.cse7 (select .cse52 .cse69)) (.cse6 (select .cse52 .cse68)) (.cse8 (select .cse52 .cse67)) (.cse9 (select .cse52 .cse66)) (.cse10 (select .cse52 .cse65)) (.cse12 (select .cse52 .cse64)) (.cse11 (select .cse52 .cse63)) (.cse13 (select .cse52 .cse62)) (.cse14 (select .cse52 .cse61)) (.cse15 (select .cse52 .cse60)) (.cse16 (select .cse52 .cse59)) (.cse17 (select .cse52 |main_~#x~0.offset|)) (.cse18 (select .cse52 .cse58)) (.cse19 (select .cse52 .cse57)) (.cse20 (select .cse52 .cse56)) (.cse21 (select .cse52 .cse48)) (.cse22 (select .cse52 .cse55)) (.cse24 (select .cse52 .cse54)) (.cse23 (select .cse52 .cse53))) (let ((.cse39 (+ .cse5 .cse7 .cse6 .cse8 .cse9 .cse10 .cse12 .cse11 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23)) (.cse51 (div .cse44 20))) (let ((.cse41 (= |main_~#x~0.offset| 0)) (.cse4 (+ main_~ret~1 4294967296)) (.cse45 (mod .cse51 4294967296)) (.cse29 (mod (+ .cse51 1) 4294967296)) (.cse50 (div .cse39 20)) (.cse30 (= (mod .cse44 20) 0))) (let ((.cse34 (not .cse30)) (.cse38 (mod .cse50 4294967296)) (.cse40 (mod (+ .cse50 1) 4294967296)) (.cse26 (not (<= .cse29 2147483647))) (.cse28 (not (<= .cse45 2147483647))) (.cse35 (not (= .cse45 main_~ret~1))) (.cse43 (not (<= 0 .cse44))) (.cse37 (not (= .cse45 .cse4))) (.cse42 (not (< 2147483647 .cse29))) (.cse25 (not (= (store |v_#memory_int_110| |main_~#x~0.base| (store (store .cse46 |main_~#x~0.offset| .cse47) .cse48 .cse49)) |#memory_int|))) (.cse36 (not (< 2147483647 .cse45))) (.cse27 (not (< .cse44 0))) (.cse2 (not .cse41))) (and (let ((.cse3 (+ .cse5 .cse6 .cse7 .cse8 .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24))) (let ((.cse1 (div .cse3 20))) (let ((.cse0 (mod .cse1 4294967296))) (or (not (< 2147483647 .cse0)) (not (< 2147483647 (mod (+ .cse1 1) 4294967296))) .cse2 (not (= (mod .cse3 20) 0)) (not (= .cse4 .cse0)))))) (or .cse25 .cse26 .cse27 .cse2 .cse28 (not (= main_~ret~1 .cse29)) .cse30) (let ((.cse31 (+ .cse5 .cse7 .cse6 .cse8 .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24))) (let ((.cse32 (div .cse31 20))) (let ((.cse33 (mod (+ .cse32 1) 4294967296))) (or (= 0 (mod .cse31 20)) (not (< .cse31 0)) (not (<= (mod .cse32 4294967296) 2147483647)) .cse2 (not (= .cse33 .cse4)) (not (< 2147483647 .cse33)))))) (or .cse25 .cse26 .cse2 .cse28 .cse34 .cse35) (or .cse25 .cse26 .cse36 .cse2 .cse37 .cse34) (or (not (= main_~ret~1 .cse38)) (not (= 0 (mod .cse39 20))) (not (< 2147483647 .cse40)) .cse2 (not (<= .cse38 2147483647))) .cse41 (or .cse42 .cse25 .cse43 .cse2 .cse28 .cse35) (or (not (< 2147483647 .cse38)) (not (<= 0 .cse39)) .cse2 (not (= .cse4 .cse38)) (not (<= .cse40 2147483647))) (or .cse25 .cse26 .cse43 .cse2 .cse28 .cse35) (or .cse42 .cse25 .cse43 .cse36 .cse2 .cse37) (or .cse42 .cse25 .cse36 .cse27 .cse2 (not (= .cse4 .cse29)) .cse30)))))))))
(assert (not (= (+ |main_~#x~0.offset| 24) (+ |main_~#x~0.offset| 48))))
(check-sat)
(exit)
20190429-UltimateAutomizerSvcomp2019/avg20_true-unreach-call.i_2.smt2 0 → 100644
View file @ 03648c4a
(set-info :smt-lib-version 2.6)
(set-logic QF_ALIA)
(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 2019 [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.
2019-04-27, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus,
Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian
Schilling, Tanja Schindler, Andreas Podelski: Ultimate Automizer
and the Search for Perfect Interpolants - (Competition Contribution).
TACAS (2) 2018: 447-451
[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: Automatic Verification of C and Java Programs: SV-COMP 2019.
TACAS (3) 2019: 133-155
[6] https://sv-comp.sosy-lab.org/2019/
|")
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun |v_#memory_int_110| () (Array Int (Array Int Int)))
(declare-fun |main_~#x~0.base| () Int)
(declare-fun |main_~#x~0.offset| () Int)
(declare-fun main_~ret~1 () Int)
(declare-fun |#memory_int| () (Array Int (Array Int Int)))
(assert (let ((.cse46 (select |v_#memory_int_110| |main_~#x~0.base|)) (.cse48 (+ |main_~#x~0.offset| 4))) (let ((.cse52 (select |#memory_int| |main_~#x~0.base|)) (.cse55 (+ |main_~#x~0.offset| 72)) (.cse56 (+ |main_~#x~0.offset| 76)) (.cse60 (+ |main_~#x~0.offset| 44)) (.cse61 (+ |main_~#x~0.offset| 68)) (.cse67 (+ |main_~#x~0.offset| 24)) (.cse66 (+ |main_~#x~0.offset| 20)) (.cse64 (+ |main_~#x~0.offset| 40)) (.cse47 (select .cse46 .cse48)) (.cse58 (+ |main_~#x~0.offset| 8)) (.cse53 (+ |main_~#x~0.offset| 28)) (.cse69 (+ |main_~#x~0.offset| 36)) (.cse65 (+ |main_~#x~0.offset| 32)) (.cse62 (+ |main_~#x~0.offset| 60)) (.cse59 (+ |main_~#x~0.offset| 52)) (.cse57 (+ |main_~#x~0.offset| 64)) (.cse70 (+ |main_~#x~0.offset| 16)) (.cse63 (+ |main_~#x~0.offset| 56)) (.cse68 (+ |main_~#x~0.offset| 48)) (.cse49 (select .cse46 |main_~#x~0.offset|)) (.cse54 (+ |main_~#x~0.offset| 12))) (let ((.cse44 (+ (select .cse46 .cse55) (select .cse46 .cse56) (select .cse46 .cse60) (select .cse46 .cse61) (select .cse46 .cse67) (select .cse46 .cse66) (select .cse46 .cse64) .cse47 (select .cse46 .cse58) (select .cse46 .cse53) (select .cse46 .cse69) (select .cse46 .cse65) (select .cse46 .cse62) (select .cse46 .cse59) (select .cse46 .cse57) (select .cse46 .cse70) (select .cse46 .cse63) (select .cse46 .cse68) .cse49 (select .cse46 .cse54))) (.cse5 (select .cse52 .cse70)) (.cse7 (select .cse52 .cse69)) (.cse6 (select .cse52 .cse68)) (.cse8 (select .cse52 .cse67)) (.cse9 (select .cse52 .cse66)) (.cse10 (select .cse52 .cse65)) (.cse12 (select .cse52 .cse64)) (.cse11 (select .cse52 .cse63)) (.cse13 (select .cse52 .cse62)) (.cse14 (select .cse52 .cse61)) (.cse15 (select .cse52 .cse60)) (.cse16 (select .cse52 .cse59)) (.cse17 (select .cse52 |main_~#x~0.offset|)) (.cse18 (select .cse52 .cse58)) (.cse19 (select .cse52 .cse57)) (.cse20 (select .cse52 .cse56)) (.cse21 (select .cse52 .cse48)) (.cse22 (select .cse52 .cse55)) (.cse24 (select .cse52 .cse54)) (.cse23 (select .cse52 .cse53))) (let ((.cse39 (+ .cse5 .cse7 .cse6 .cse8 .cse9 .cse10 .cse12 .cse11 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23)) (.cse51 (div .cse44 20))) (let ((.cse41 (= |main_~#x~0.offset| 0)) (.cse4 (+ main_~ret~1 4294967296)) (.cse45 (mod .cse51 4294967296)) (.cse29 (mod (+ .cse51 1) 4294967296)) (.cse50 (div .cse39 20)) (.cse30 (= (mod .cse44 20) 0))) (let ((.cse34 (not .cse30)) (.cse38 (mod .cse50 4294967296)) (.cse40 (mod (+ .cse50 1) 4294967296)) (.cse26 (not (<= .cse29 2147483647))) (.cse28 (not (<= .cse45 2147483647))) (.cse35 (not (= .cse45 main_~ret~1))) (.cse43 (not (<= 0 .cse44))) (.cse37 (not (= .cse45 .cse4))) (.cse42 (not (< 2147483647 .cse29))) (.cse25 (not (= (store |v_#memory_int_110| |main_~#x~0.base| (store (store .cse46 |main_~#x~0.offset| .cse47) .cse48 .cse49)) |#memory_int|))) (.cse36 (not (< 2147483647 .cse45))) (.cse27 (not (< .cse44 0))) (.cse2 (not .cse41))) (and (let ((.cse3 (+ .cse5 .cse6 .cse7 .cse8 .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24))) (let ((.cse1 (div .cse3 20))) (let ((.cse0 (mod .cse1 4294967296))) (or (not (< 2147483647 .cse0)) (not (< 2147483647 (mod (+ .cse1 1) 4294967296))) .cse2 (not (= (mod .cse3 20) 0)) (not (= .cse4 .cse0)))))) (or .cse25 .cse26 .cse27 .cse2 .cse28 (not (= main_~ret~1 .cse29)) .cse30) (let ((.cse31 (+ .cse5 .cse7 .cse6 .cse8 .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24))) (let ((.cse32 (div .cse31 20))) (let ((.cse33 (mod (+ .cse32 1) 4294967296))) (or (= 0 (mod .cse31 20)) (not (< .cse31 0)) (not (<= (mod .cse32 4294967296) 2147483647)) .cse2 (not (= .cse33 .cse4)) (not (< 2147483647 .cse33)))))) (or .cse25 .cse26 .cse2 .cse28 .cse34 .cse35) (or .cse25 .cse26 .cse36 .cse2 .cse37 .cse34) (or (not (= main_~ret~1 .cse38)) (not (= 0 (mod .cse39 20))) (not (< 2147483647 .cse40)) .cse2 (not (<= .cse38 2147483647))) .cse41 (or .cse42 .cse25 .cse43 .cse2 .cse28 .cse35) (or (not (< 2147483647 .cse38)) (not (<= 0 .cse39)) .cse2 (not (= .cse4 .cse38)) (not (<= .cse40 2147483647))) (or .cse25 .cse26 .cse43 .cse2 .cse28 .cse35) (or .cse42 .cse25 .cse43 .cse36 .cse2 .cse37) (or .cse42 .cse25 .cse36 .cse27 .cse2 (not (= .cse4 .cse29)) .cse30)))))))))
(assert (not (= (+ |main_~#x~0.offset| 24) (+ |main_~#x~0.offset| 56))))
(check-sat)
(exit)
20190429-UltimateAutomizerSvcomp2019/avg20_true-unreach-call.i_3.smt2 0 → 100644
View file @ 03648c4a
(set-info :smt-lib-version 2.6)
(set-logic QF_ALIA)
(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 2019 [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.
2019-04-27, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus,
Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian
Schilling, Tanja Schindler, Andreas Podelski: Ultimate Automizer
and the Search for Perfect Interpolants - (Competition Contribution).
TACAS (2) 2018: 447-451
[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: Automatic Verification of C and Java Programs: SV-COMP 2019.
TACAS (3) 2019: 133-155
[6] https://sv-comp.sosy-lab.org/2019/
|")
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun |v_#memory_int_110| () (Array Int (Array Int Int)))
(declare-fun |main_~#x~0.base| () Int)
(declare-fun |main_~#x~0.offset| () Int)
(declare-fun main_~ret~1 () Int)
(declare-fun |#memory_int| () (Array Int (Array Int Int)))
(assert (let ((.cse54 (select |v_#memory_int_110| |main_~#x~0.base|)) (.cse66 (+ |main_~#x~0.offset| 28)) (.cse75 (+ |main_~#x~0.offset| 12)) (.cse58 (+ |main_~#x~0.offset| 72)) (.cse56 (+ |main_~#x~0.offset| 4)) (.cse59 (+ |main_~#x~0.offset| 76)) (.cse71 (+ |main_~#x~0.offset| 64)) (.cse65 (+ |main_~#x~0.offset| 8)) (.cse70 (+ |main_~#x~0.offset| 52)) (.cse60 (+ |main_~#x~0.offset| 44)) (.cse61 (+ |main_~#x~0.offset| 68)) (.cse69 (+ |main_~#x~0.offset| 60)) (.cse73 (+ |main_~#x~0.offset| 56)) (.cse64 (+ |main_~#x~0.offset| 40)) (.cse68 (+ |main_~#x~0.offset| 32)) (.cse63 (+ |main_~#x~0.offset| 20)) (.cse62 (+ |main_~#x~0.offset| 24)) (.cse74 (+ |main_~#x~0.offset| 48)) (.cse67 (+ |main_~#x~0.offset| 36)) (.cse76 (select |#memory_int| |main_~#x~0.base|)) (.cse72 (+ |main_~#x~0.offset| 16))) (let ((.cse9 (select .cse76 .cse72)) (.cse11 (select .cse76 .cse67)) (.cse10 (select .cse76 .cse74)) (.cse12 (select .cse76 .cse62)) (.cse13 (select .cse76 .cse63)) (.cse14 (select .cse76 .cse68)) (.cse16 (select .cse76 .cse64)) (.cse15 (select .cse76 .cse73)) (.cse17 (select .cse76 .cse69)) (.cse18 (select .cse76 .cse61)) (.cse19 (select .cse76 .cse60)) (.cse20 (select .cse76 .cse70)) (.cse21 (select .cse76 |main_~#x~0.offset|)) (.cse22 (select .cse76 .cse65)) (.cse23 (select .cse76 .cse71)) (.cse24 (select .cse76 .cse59)) (.cse25 (select .cse76 .cse56)) (.cse26 (select .cse76 .cse58)) (.cse28 (select .cse76 .cse75)) (.cse27 (select .cse76 .cse66)) (.cse55 (select .cse54 .cse56)) (.cse57 (select .cse54 |main_~#x~0.offset|))) (let ((.cse52 (+ (select .cse54 .cse58) (select .cse54 .cse59) (select .cse54 .cse60) (select .cse54 .cse61) (select .cse54 .cse62) (select .cse54 .cse63) (select .cse54 .cse64) .cse55 (select .cse54 .cse65) (select .cse54 .cse66) (select .cse54 .cse67) (select .cse54 .cse68) (select .cse54 .cse69) (select .cse54 .cse70) (select .cse54 .cse71) (select .cse54 .cse72) (select .cse54 .cse73) (select .cse54 .cse74) .cse57 (select .cse54 .cse75))) (.cse40 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse28 .cse27)) (.cse50 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse28 .cse27))) (let ((.cse45 (= |main_~#x~0.offset| 0)) (.cse49 (div .cse50 20)) (.cse51 (div .cse40 20)) (.cse53 (div .cse52 20))) (let ((.cse35 (not (= (store |v_#memory_int_110| |main_~#x~0.base| (store (store .cse54 |main_~#x~0.offset| .cse55) .cse56 .cse57)) |#memory_int|))) (.cse36 (not (<= (mod (+ .cse53 1) 4294967296) 2147483647))) (.cse37 (mod .cse53 4294967296)) (.cse38 (not (= (mod .cse52 20) 0))) (.cse2 (+ main_~ret~1 4294967296)) (.cse39 (mod .cse51 4294967296)) (.cse41 (mod (+ .cse51 1) 4294967296)) (.cse1 (= 0 (mod .cse50 20))) (.cse4 (not (< .cse50 0))) (.cse0 (mod .cse49 4294967296)) (.cse5 (not .cse45)) (.cse3 (mod (+ .cse49 1) 4294967296))) (and (or (not (< 2147483647 .cse0)) .cse1 (not (= .cse2 .cse3)) (not (< 2147483647 .cse3)) .cse4 .cse5) (let ((.cse8 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse27 .cse28))) (let ((.cse7 (div .cse8 20))) (let ((.cse6 (mod .cse7 4294967296))) (or (not (< 2147483647 .cse6)) (not (< 2147483647 (mod (+ .cse7 1) 4294967296))) .cse5 (not (= (mod .cse8 20) 0)) (not (= .cse2 .cse6)))))) (let ((.cse30 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse27 .cse28))) (let ((.cse31 (div .cse30 20))) (let ((.cse29 (mod .cse31 4294967296))) (or (not (= main_~ret~1 .cse29)) (not (<= 0 .cse30)) (not (<= (mod (+ .cse31 1) 4294967296) 2147483647)) .cse5 (not (<= .cse29 2147483647)))))) (let ((.cse32 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse27 .cse28))) (let ((.cse33 (div .cse32 20))) (let ((.cse34 (mod (+ .cse33 1) 4294967296))) (or (= 0 (mod .cse32 20)) (not (< .cse32 0)) (not (<= (mod .cse33 4294967296) 2147483647)) .cse5 (not (= .cse34 .cse2)) (not (< 2147483647 .cse34)))))) (or .cse35 .cse36 .cse5 (not (<= .cse37 2147483647)) .cse38 (not (= .cse37 main_~ret~1))) (or .cse35 .cse36 (not (< 2147483647 .cse37)) .cse5 (not (= .cse37 .cse2)) .cse38) (or (not (= main_~ret~1 .cse39)) (not (= 0 (mod .cse40 20))) (not (< 2147483647 .cse41)) .cse5 (not (<= .cse39 2147483647))) (let ((.cse44 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse28 .cse27))) (let ((.cse43 (div .cse44 20))) (let ((.cse42 (mod .cse43 4294967296))) (or (not (<= .cse42 2147483647)) (not (< 2147483647 (mod (+ .cse43 1) 4294967296))) (not (= main_~ret~1 .cse42)) .cse5 (not (<= 0 .cse44)))))) .cse45 (or (not (< 2147483647 .cse39)) (not (<= 0 .cse40)) .cse5 (not (= .cse2 .cse39)) (not (<= .cse41 2147483647))) (let ((.cse47 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse27 .cse28))) (let ((.cse48 (div .cse47 20))) (let ((.cse46 (mod (+ .cse48 1) 4294967296))) (or (not (= .cse46 main_~ret~1)) (not (< .cse47 0)) (not (< 2147483647 (mod .cse48 4294967296))) (not (<= .cse46 2147483647)) .cse5 (= 0 (mod .cse47 20)))))) (or .cse1 .cse4 (not (<= .cse0 2147483647)) .cse5 (not (= .cse3 main_~ret~1)) (not (<= .cse3 2147483647))))))))))
(assert (let ((.cse0 (select |v_#memory_int_110| |main_~#x~0.base|))) (= (select .cse0 (+ |main_~#x~0.offset| 8)) (select .cse0 (+ |main_~#x~0.offset| 24)))))
(check-sat)
(exit)
20190429-UltimateAutomizerSvcomp2019/avg20_true-unreach-call.i_4.smt2 0 → 100644
View file @ 03648c4a
(set-info :smt-lib-version 2.6)
(set-logic QF_ALIA)
(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 2019 [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.
2019-04-27, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus,
Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian
Schilling, Tanja Schindler, Andreas Podelski: Ultimate Automizer
and the Search for Perfect Interpolants - (Competition Contribution).
TACAS (2) 2018: 447-451
[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: Automatic Verification of C and Java Programs: SV-COMP 2019.
TACAS (3) 2019: 133-155
[6] https://sv-comp.sosy-lab.org/2019/
|")
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun |v_#memory_int_110| () (Array Int (Array Int Int)))
(declare-fun |main_~#x~0.base| () Int)
(declare-fun |main_~#x~0.offset| () Int)
(declare-fun main_~ret~1 () Int)
(declare-fun |#memory_int| () (Array Int (Array Int Int)))
(assert (let ((.cse50 (+ |main_~#x~0.offset| 28)) (.cse59 (+ |main_~#x~0.offset| 12)) (.cse42 (+ |main_~#x~0.offset| 72)) (.cse37 (+ |main_~#x~0.offset| 4)) (.cse55 (+ |main_~#x~0.offset| 64)) (.cse43 (+ |main_~#x~0.offset| 76)) (.cse49 (+ |main_~#x~0.offset| 8)) (.cse54 (+ |main_~#x~0.offset| 52)) (.cse44 (+ |main_~#x~0.offset| 44)) (.cse45 (+ |main_~#x~0.offset| 68)) (.cse53 (+ |main_~#x~0.offset| 60)) (.cse57 (+ |main_~#x~0.offset| 56)) (.cse48 (+ |main_~#x~0.offset| 40)) (.cse52 (+ |main_~#x~0.offset| 32)) (.cse47 (+ |main_~#x~0.offset| 20)) (.cse46 (+ |main_~#x~0.offset| 24)) (.cse51 (+ |main_~#x~0.offset| 36)) (.cse58 (+ |main_~#x~0.offset| 48)) (.cse75 (select |#memory_int| |main_~#x~0.base|)) (.cse56 (+ |main_~#x~0.offset| 16))) (let ((.cse9 (select .cse75 .cse56)) (.cse10 (select .cse75 .cse58)) (.cse11 (select .cse75 .cse51)) (.cse12 (select .cse75 .cse46)) (.cse13 (select .cse75 .cse47)) (.cse14 (select .cse75 .cse52)) (.cse16 (select .cse75 .cse48)) (.cse15 (select .cse75 .cse57)) (.cse17 (select .cse75 .cse53)) (.cse18 (select .cse75 .cse45)) (.cse19 (select .cse75 .cse44)) (.cse20 (select .cse75 .cse54)) (.cse21 (select .cse75 |main_~#x~0.offset|)) (.cse22 (select .cse75 .cse49)) (.cse24 (select .cse75 .cse43)) (.cse23 (select .cse75 .cse55)) (.cse25 (select .cse75 .cse37)) (.cse26 (select .cse75 .cse42)) (.cse28 (select .cse75 .cse59)) (.cse27 (select .cse75 .cse50))) (let ((.cse73 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse28 .cse27)) (.cse61 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse28 .cse27)) (.cse71 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse28 .cse27))) (let ((.cse66 (= |main_~#x~0.offset| 0)) (.cse70 (div .cse71 20)) (.cse72 (div .cse61 20)) (.cse74 (div .cse73 20))) (let ((.cse63 (not (< 2147483647 (mod (+ .cse74 1) 4294967296)))) (.cse64 (mod .cse74 4294967296)) (.cse65 (not (<= 0 .cse73))) (.cse2 (+ main_~ret~1 4294967296)) (.cse60 (mod .cse72 4294967296)) (.cse62 (mod (+ .cse72 1) 4294967296)) (.cse1 (= 0 (mod .cse71 20))) (.cse4 (not (< .cse71 0))) (.cse0 (mod .cse70 4294967296)) (.cse5 (not .cse66)) (.cse3 (mod (+ .cse70 1) 4294967296))) (and (or (not (< 2147483647 .cse0)) .cse1 (not (= .cse2 .cse3)) (not (< 2147483647 .cse3)) .cse4 .cse5) (let ((.cse8 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse27 .cse28))) (let ((.cse7 (div .cse8 20))) (let ((.cse6 (mod .cse7 4294967296))) (or (not (< 2147483647 .cse6)) (not (< 2147483647 (mod (+ .cse7 1) 4294967296))) .cse5 (not (= (mod .cse8 20) 0)) (not (= .cse2 .cse6)))))) (let ((.cse30 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse27 .cse28))) (let ((.cse31 (div .cse30 20))) (let ((.cse29 (mod .cse31 4294967296))) (or (not (= main_~ret~1 .cse29)) (not (<= 0 .cse30)) (not (<= (mod (+ .cse31 1) 4294967296) 2147483647)) .cse5 (not (<= .cse29 2147483647)))))) (let ((.cse32 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse27 .cse28))) (let ((.cse33 (div .cse32 20))) (let ((.cse34 (mod (+ .cse33 1) 4294967296))) (or (= 0 (mod .cse32 20)) (not (< .cse32 0)) (not (<= (mod .cse33 4294967296) 2147483647)) .cse5 (not (= .cse34 .cse2)) (not (< 2147483647 .cse34)))))) (let ((.cse35 (select |v_#memory_int_110| |main_~#x~0.base|))) (let ((.cse36 (select .cse35 .cse37)) (.cse38 (select .cse35 |main_~#x~0.offset|))) (let ((.cse41 (+ (select .cse35 .cse42) (select .cse35 .cse43) (select .cse35 .cse44) (select .cse35 .cse45) (select .cse35 .cse46) (select .cse35 .cse47) (select .cse35 .cse48) .cse36 (select .cse35 .cse49) (select .cse35 .cse50) (select .cse35 .cse51) (select .cse35 .cse52) (select .cse35 .cse53) (select .cse35 .cse54) (select .cse35 .cse55) (select .cse35 .cse56) (select .cse35 .cse57) (select .cse35 .cse58) .cse38 (select .cse35 .cse59)))) (let ((.cse39 (div .cse41 20))) (let ((.cse40 (mod .cse39 4294967296))) (or (not (= (store |v_#memory_int_110| |main_~#x~0.base| (store (store .cse35 |main_~#x~0.offset| .cse36) .cse37 .cse38)) |#memory_int|)) (not (<= (mod (+ .cse39 1) 4294967296) 2147483647)) .cse5 (not (<= .cse40 2147483647)) (not (= (mod .cse41 20) 0)) (not (= .cse40 main_~ret~1)))))))) (or (not (= main_~ret~1 .cse60)) (not (= 0 (mod .cse61 20))) (not (< 2147483647 .cse62)) .cse5 (not (<= .cse60 2147483647))) (or .cse63 (not (= .cse2 .cse64)) .cse5 (not (< 2147483647 .cse64)) .cse65) (or (not (<= .cse64 2147483647)) .cse63 (not (= main_~ret~1 .cse64)) .cse5 .cse65) .cse66 (or (not (< 2147483647 .cse60)) (not (<= 0 .cse61)) .cse5 (not (= .cse2 .cse60)) (not (<= .cse62 2147483647))) (let ((.cse68 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse27 .cse28))) (let ((.cse69 (div .cse68 20))) (let ((.cse67 (mod (+ .cse69 1) 4294967296))) (or (not (= .cse67 main_~ret~1)) (not (< .cse68 0)) (not (< 2147483647 (mod .cse69 4294967296))) (not (<= .cse67 2147483647)) .cse5 (= 0 (mod .cse68 20)))))) (or .cse1 .cse4 (not (<= .cse0 2147483647)) .cse5 (not (= .cse3 main_~ret~1)) (not (<= .cse3 2147483647))))))))))
(assert (not (= (+ |main_~#x~0.offset| 72) (+ |main_~#x~0.offset| 4))))
(check-sat)
(exit)
20190429-UltimateAutomizerSvcomp2019/avg20_true-unreach-call.i_5.smt2 0 → 100644
View file @ 03648c4a
(set-info :smt-lib-version 2.6)
(set-logic QF_ALIA)
(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 2019 [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.
2019-04-27, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus,
Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian
Schilling, Tanja Schindler, Andreas Podelski: Ultimate Automizer
and the Search for Perfect Interpolants - (Competition Contribution).
TACAS (2) 2018: 447-451
[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: Automatic Verification of C and Java Programs: SV-COMP 2019.
TACAS (3) 2019: 133-155
[6] https://sv-comp.sosy-lab.org/2019/
|")
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun |v_#memory_int_110| () (Array Int (Array Int Int)))
(declare-fun |main_~#x~0.base| () Int)
(declare-fun |main_~#x~0.offset| () Int)
(declare-fun main_~ret~1 () Int)
(declare-fun |#memory_int| () (Array Int (Array Int Int)))
(assert (let ((.cse50 (+ |main_~#x~0.offset| 28)) (.cse59 (+ |main_~#x~0.offset| 12)) (.cse42 (+ |main_~#x~0.offset| 72)) (.cse37 (+ |main_~#x~0.offset| 4)) (.cse55 (+ |main_~#x~0.offset| 64)) (.cse43 (+ |main_~#x~0.offset| 76)) (.cse49 (+ |main_~#x~0.offset| 8)) (.cse54 (+ |main_~#x~0.offset| 52)) (.cse44 (+ |main_~#x~0.offset| 44)) (.cse45 (+ |main_~#x~0.offset| 68)) (.cse53 (+ |main_~#x~0.offset| 60)) (.cse57 (+ |main_~#x~0.offset| 56)) (.cse48 (+ |main_~#x~0.offset| 40)) (.cse52 (+ |main_~#x~0.offset| 32)) (.cse47 (+ |main_~#x~0.offset| 20)) (.cse46 (+ |main_~#x~0.offset| 24)) (.cse51 (+ |main_~#x~0.offset| 36)) (.cse58 (+ |main_~#x~0.offset| 48)) (.cse75 (select |#memory_int| |main_~#x~0.base|)) (.cse56 (+ |main_~#x~0.offset| 16))) (let ((.cse9 (select .cse75 .cse56)) (.cse10 (select .cse75 .cse58)) (.cse11 (select .cse75 .cse51)) (.cse12 (select .cse75 .cse46)) (.cse13 (select .cse75 .cse47)) (.cse14 (select .cse75 .cse52)) (.cse16 (select .cse75 .cse48)) (.cse15 (select .cse75 .cse57)) (.cse17 (select .cse75 .cse53)) (.cse18 (select .cse75 .cse45)) (.cse19 (select .cse75 .cse44)) (.cse20 (select .cse75 .cse54)) (.cse21 (select .cse75 |main_~#x~0.offset|)) (.cse22 (select .cse75 .cse49)) (.cse24 (select .cse75 .cse43)) (.cse23 (select .cse75 .cse55)) (.cse25 (select .cse75 .cse37)) (.cse26 (select .cse75 .cse42)) (.cse28 (select .cse75 .cse59)) (.cse27 (select .cse75 .cse50))) (let ((.cse73 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse28 .cse27)) (.cse61 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse28 .cse27)) (.cse71 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse28 .cse27))) (let ((.cse66 (= |main_~#x~0.offset| 0)) (.cse70 (div .cse71 20)) (.cse72 (div .cse61 20)) (.cse74 (div .cse73 20))) (let ((.cse63 (not (< 2147483647 (mod (+ .cse74 1) 4294967296)))) (.cse64 (mod .cse74 4294967296)) (.cse65 (not (<= 0 .cse73))) (.cse2 (+ main_~ret~1 4294967296)) (.cse60 (mod .cse72 4294967296)) (.cse62 (mod (+ .cse72 1) 4294967296)) (.cse1 (= 0 (mod .cse71 20))) (.cse4 (not (< .cse71 0))) (.cse0 (mod .cse70 4294967296)) (.cse5 (not .cse66)) (.cse3 (mod (+ .cse70 1) 4294967296))) (and (or (not (< 2147483647 .cse0)) .cse1 (not (= .cse2 .cse3)) (not (< 2147483647 .cse3)) .cse4 .cse5) (let ((.cse8 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse27 .cse28))) (let ((.cse7 (div .cse8 20))) (let ((.cse6 (mod .cse7 4294967296))) (or (not (< 2147483647 .cse6)) (not (< 2147483647 (mod (+ .cse7 1) 4294967296))) .cse5 (not (= (mod .cse8 20) 0)) (not (= .cse2 .cse6)))))) (let ((.cse30 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse27 .cse28))) (let ((.cse31 (div .cse30 20))) (let ((.cse29 (mod .cse31 4294967296))) (or (not (= main_~ret~1 .cse29)) (not (<= 0 .cse30)) (not (<= (mod (+ .cse31 1) 4294967296) 2147483647)) .cse5 (not (<= .cse29 2147483647)))))) (let ((.cse32 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse27 .cse28))) (let ((.cse33 (div .cse32 20))) (let ((.cse34 (mod (+ .cse33 1) 4294967296))) (or (= 0 (mod .cse32 20)) (not (< .cse32 0)) (not (<= (mod .cse33 4294967296) 2147483647)) .cse5 (not (= .cse34 .cse2)) (not (< 2147483647 .cse34)))))) (let ((.cse35 (select |v_#memory_int_110| |main_~#x~0.base|))) (let ((.cse36 (select .cse35 .cse37)) (.cse38 (select .cse35 |main_~#x~0.offset|))) (let ((.cse41 (+ (select .cse35 .cse42) (select .cse35 .cse43) (select .cse35 .cse44) (select .cse35 .cse45) (select .cse35 .cse46) (select .cse35 .cse47) (select .cse35 .cse48) .cse36 (select .cse35 .cse49) (select .cse35 .cse50) (select .cse35 .cse51) (select .cse35 .cse52) (select .cse35 .cse53) (select .cse35 .cse54) (select .cse35 .cse55) (select .cse35 .cse56) (select .cse35 .cse57) (select .cse35 .cse58) .cse38 (select .cse35 .cse59)))) (let ((.cse39 (div .cse41 20))) (let ((.cse40 (mod .cse39 4294967296))) (or (not (= (store |v_#memory_int_110| |main_~#x~0.base| (store (store .cse35 |main_~#x~0.offset| .cse36) .cse37 .cse38)) |#memory_int|)) (not (<= (mod (+ .cse39 1) 4294967296) 2147483647)) .cse5 (not (<= .cse40 2147483647)) (not (= (mod .cse41 20) 0)) (not (= .cse40 main_~ret~1)))))))) (or (not (= main_~ret~1 .cse60)) (not (= 0 (mod .cse61 20))) (not (< 2147483647 .cse62)) .cse5 (not (<= .cse60 2147483647))) (or .cse63 (not (= .cse2 .cse64)) .cse5 (not (< 2147483647 .cse64)) .cse65) (or (not (<= .cse64 2147483647)) .cse63 (not (= main_~ret~1 .cse64)) .cse5 .cse65) .cse66 (or (not (< 2147483647 .cse60)) (not (<= 0 .cse61)) .cse5 (not (= .cse2 .cse60)) (not (<= .cse62 2147483647))) (let ((.cse68 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse27 .cse28))) (let ((.cse69 (div .cse68 20))) (let ((.cse67 (mod (+ .cse69 1) 4294967296))) (or (not (= .cse67 main_~ret~1)) (not (< .cse68 0)) (not (< 2147483647 (mod .cse69 4294967296))) (not (<= .cse67 2147483647)) .cse5 (= 0 (mod .cse68 20)))))) (or .cse1 .cse4 (not (<= .cse0 2147483647)) .cse5 (not (= .cse3 main_~ret~1)) (not (<= .cse3 2147483647))))))))))
(assert (not (= (+ |main_~#x~0.offset| 48) (+ |main_~#x~0.offset| 4))))
(check-sat)
(exit)
20190429-UltimateAutomizerSvcomp2019/avg20_true-unreach-call.i_6.smt2 0 → 100644
View file @ 03648c4a
(set-info :smt-lib-version 2.6)
(set-logic QF_ALIA)
(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 2019 [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.
2019-04-27, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus,
Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian
Schilling, Tanja Schindler, Andreas Podelski: Ultimate Automizer
and the Search for Perfect Interpolants - (Competition Contribution).
TACAS (2) 2018: 447-451
[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: Automatic Verification of C and Java Programs: SV-COMP 2019.
TACAS (3) 2019: 133-155
[6] https://sv-comp.sosy-lab.org/2019/
|")
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun |v_#memory_int_110| () (Array Int (Array Int Int)))
(declare-fun |main_~#x~0.base| () Int)
(declare-fun |main_~#x~0.offset| () Int)
(declare-fun main_~ret~1 () Int)
(declare-fun |#memory_int| () (Array Int (Array Int Int)))
(assert (let ((.cse50 (+ |main_~#x~0.offset| 28)) (.cse59 (+ |main_~#x~0.offset| 12)) (.cse42 (+ |main_~#x~0.offset| 72)) (.cse37 (+ |main_~#x~0.offset| 4)) (.cse55 (+ |main_~#x~0.offset| 64)) (.cse43 (+ |main_~#x~0.offset| 76)) (.cse49 (+ |main_~#x~0.offset| 8)) (.cse54 (+ |main_~#x~0.offset| 52)) (.cse44 (+ |main_~#x~0.offset| 44)) (.cse45 (+ |main_~#x~0.offset| 68)) (.cse53 (+ |main_~#x~0.offset| 60)) (.cse57 (+ |main_~#x~0.offset| 56)) (.cse48 (+ |main_~#x~0.offset| 40)) (.cse52 (+ |main_~#x~0.offset| 32)) (.cse47 (+ |main_~#x~0.offset| 20)) (.cse46 (+ |main_~#x~0.offset| 24)) (.cse51 (+ |main_~#x~0.offset| 36)) (.cse58 (+ |main_~#x~0.offset| 48)) (.cse75 (select |#memory_int| |main_~#x~0.base|)) (.cse56 (+ |main_~#x~0.offset| 16))) (let ((.cse9 (select .cse75 .cse56)) (.cse10 (select .cse75 .cse58)) (.cse11 (select .cse75 .cse51)) (.cse12 (select .cse75 .cse46)) (.cse13 (select .cse75 .cse47)) (.cse14 (select .cse75 .cse52)) (.cse16 (select .cse75 .cse48)) (.cse15 (select .cse75 .cse57)) (.cse17 (select .cse75 .cse53)) (.cse18 (select .cse75 .cse45)) (.cse19 (select .cse75 .cse44)) (.cse20 (select .cse75 .cse54)) (.cse21 (select .cse75 |main_~#x~0.offset|)) (.cse22 (select .cse75 .cse49)) (.cse24 (select .cse75 .cse43)) (.cse23 (select .cse75 .cse55)) (.cse25 (select .cse75 .cse37)) (.cse26 (select .cse75 .cse42)) (.cse28 (select .cse75 .cse59)) (.cse27 (select .cse75 .cse50))) (let ((.cse73 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse28 .cse27)) (.cse61 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse28 .cse27)) (.cse71 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse28 .cse27))) (let ((.cse66 (= |main_~#x~0.offset| 0)) (.cse70 (div .cse71 20)) (.cse72 (div .cse61 20)) (.cse74 (div .cse73 20))) (let ((.cse63 (not (< 2147483647 (mod (+ .cse74 1) 4294967296)))) (.cse64 (mod .cse74 4294967296)) (.cse65 (not (<= 0 .cse73))) (.cse2 (+ main_~ret~1 4294967296)) (.cse60 (mod .cse72 4294967296)) (.cse62 (mod (+ .cse72 1) 4294967296)) (.cse1 (= 0 (mod .cse71 20))) (.cse4 (not (< .cse71 0))) (.cse0 (mod .cse70 4294967296)) (.cse5 (not .cse66)) (.cse3 (mod (+ .cse70 1) 4294967296))) (and (or (not (< 2147483647 .cse0)) .cse1 (not (= .cse2 .cse3)) (not (< 2147483647 .cse3)) .cse4 .cse5) (let ((.cse8 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse27 .cse28))) (let ((.cse7 (div .cse8 20))) (let ((.cse6 (mod .cse7 4294967296))) (or (not (< 2147483647 .cse6)) (not (< 2147483647 (mod (+ .cse7 1) 4294967296))) .cse5 (not (= (mod .cse8 20) 0)) (not (= .cse2 .cse6)))))) (let ((.cse30 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse27 .cse28))) (let ((.cse31 (div .cse30 20))) (let ((.cse29 (mod .cse31 4294967296))) (or (not (= main_~ret~1 .cse29)) (not (<= 0 .cse30)) (not (<= (mod (+ .cse31 1) 4294967296) 2147483647)) .cse5 (not (<= .cse29 2147483647)))))) (let ((.cse32 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse27 .cse28))) (let ((.cse33 (div .cse32 20))) (let ((.cse34 (mod (+ .cse33 1) 4294967296))) (or (= 0 (mod .cse32 20)) (not (< .cse32 0)) (not (<= (mod .cse33 4294967296) 2147483647)) .cse5 (not (= .cse34 .cse2)) (not (< 2147483647 .cse34)))))) (let ((.cse35 (select |v_#memory_int_110| |main_~#x~0.base|))) (let ((.cse36 (select .cse35 .cse37)) (.cse38 (select .cse35 |main_~#x~0.offset|))) (let ((.cse41 (+ (select .cse35 .cse42) (select .cse35 .cse43) (select .cse35 .cse44) (select .cse35 .cse45) (select .cse35 .cse46) (select .cse35 .cse47) (select .cse35 .cse48) .cse36 (select .cse35 .cse49) (select .cse35 .cse50) (select .cse35 .cse51) (select .cse35 .cse52) (select .cse35 .cse53) (select .cse35 .cse54) (select .cse35 .cse55) (select .cse35 .cse56) (select .cse35 .cse57) (select .cse35 .cse58) .cse38 (select .cse35 .cse59)))) (let ((.cse39 (div .cse41 20))) (let ((.cse40 (mod .cse39 4294967296))) (or (not (= (store |v_#memory_int_110| |main_~#x~0.base| (store (store .cse35 |main_~#x~0.offset| .cse36) .cse37 .cse38)) |#memory_int|)) (not (<= (mod (+ .cse39 1) 4294967296) 2147483647)) .cse5 (not (<= .cse40 2147483647)) (not (= (mod .cse41 20) 0)) (not (= .cse40 main_~ret~1)))))))) (or (not (= main_~ret~1 .cse60)) (not (= 0 (mod .cse61 20))) (not (< 2147483647 .cse62)) .cse5 (not (<= .cse60 2147483647))) (or .cse63 (not (= .cse2 .cse64)) .cse5 (not (< 2147483647 .cse64)) .cse65) (or (not (<= .cse64 2147483647)) .cse63 (not (= main_~ret~1 .cse64)) .cse5 .cse65) .cse66 (or (not (< 2147483647 .cse60)) (not (<= 0 .cse61)) .cse5 (not (= .cse2 .cse60)) (not (<= .cse62 2147483647))) (let ((.cse68 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse27 .cse28))) (let ((.cse69 (div .cse68 20))) (let ((.cse67 (mod (+ .cse69 1) 4294967296))) (or (not (= .cse67 main_~ret~1)) (not (< .cse68 0)) (not (< 2147483647 (mod .cse69 4294967296))) (not (<= .cse67 2147483647)) .cse5 (= 0 (mod .cse68 20)))))) (or .cse1 .cse4 (not (<= .cse0 2147483647)) .cse5 (not (= .cse3 main_~ret~1)) (not (<= .cse3 2147483647))))))))))
(assert (not (= (+ |main_~#x~0.offset| 32) (+ |main_~#x~0.offset| 8))))
(check-sat)
(exit)
20190429-UltimateAutomizerSvcomp2019/avg20_true-unreach-call.i_7.smt2 0 → 100644
View file @ 03648c4a
(set-info :smt-lib-version 2.6)
(set-logic QF_ALIA)
(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 2019 [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.
2019-04-27, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus,
Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian
Schilling, Tanja Schindler, Andreas Podelski: Ultimate Automizer
and the Search for Perfect Interpolants - (Competition Contribution).
TACAS (2) 2018: 447-451
[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: Automatic Verification of C and Java Programs: SV-COMP 2019.
TACAS (3) 2019: 133-155
[6] https://sv-comp.sosy-lab.org/2019/
|")
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun |v_#memory_int_110| () (Array Int (Array Int Int)))
(declare-fun |main_~#x~0.base| () Int)
(declare-fun |main_~#x~0.offset| () Int)
(declare-fun main_~ret~1 () Int)
(declare-fun |#memory_int| () (Array Int (Array Int Int)))
(assert (let ((.cse50 (+ |main_~#x~0.offset| 28)) (.cse59 (+ |main_~#x~0.offset| 12)) (.cse42 (+ |main_~#x~0.offset| 72)) (.cse37 (+ |main_~#x~0.offset| 4)) (.cse55 (+ |main_~#x~0.offset| 64)) (.cse43 (+ |main_~#x~0.offset| 76)) (.cse49 (+ |main_~#x~0.offset| 8)) (.cse54 (+ |main_~#x~0.offset| 52)) (.cse44 (+ |main_~#x~0.offset| 44)) (.cse45 (+ |main_~#x~0.offset| 68)) (.cse53 (+ |main_~#x~0.offset| 60)) (.cse57 (+ |main_~#x~0.offset| 56)) (.cse48 (+ |main_~#x~0.offset| 40)) (.cse52 (+ |main_~#x~0.offset| 32)) (.cse47 (+ |main_~#x~0.offset| 20)) (.cse46 (+ |main_~#x~0.offset| 24)) (.cse51 (+ |main_~#x~0.offset| 36)) (.cse58 (+ |main_~#x~0.offset| 48)) (.cse75 (select |#memory_int| |main_~#x~0.base|)) (.cse56 (+ |main_~#x~0.offset| 16))) (let ((.cse9 (select .cse75 .cse56)) (.cse10 (select .cse75 .cse58)) (.cse11 (select .cse75 .cse51)) (.cse12 (select .cse75 .cse46)) (.cse13 (select .cse75 .cse47)) (.cse14 (select .cse75 .cse52)) (.cse16 (select .cse75 .cse48)) (.cse15 (select .cse75 .cse57)) (.cse17 (select .cse75 .cse53)) (.cse18 (select .cse75 .cse45)) (.cse19 (select .cse75 .cse44)) (.cse20 (select .cse75 .cse54)) (.cse21 (select .cse75 |main_~#x~0.offset|)) (.cse22 (select .cse75 .cse49)) (.cse24 (select .cse75 .cse43)) (.cse23 (select .cse75 .cse55)) (.cse25 (select .cse75 .cse37)) (.cse26 (select .cse75 .cse42)) (.cse28 (select .cse75 .cse59)) (.cse27 (select .cse75 .cse50))) (let ((.cse73 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse28 .cse27)) (.cse61 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse28 .cse27)) (.cse71 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse28 .cse27))) (let ((.cse66 (= |main_~#x~0.offset| 0)) (.cse70 (div .cse71 20)) (.cse72 (div .cse61 20)) (.cse74 (div .cse73 20))) (let ((.cse63 (not (< 2147483647 (mod (+ .cse74 1) 4294967296)))) (.cse64 (mod .cse74 4294967296)) (.cse65 (not (<= 0 .cse73))) (.cse2 (+ main_~ret~1 4294967296)) (.cse60 (mod .cse72 4294967296)) (.cse62 (mod (+ .cse72 1) 4294967296)) (.cse1 (= 0 (mod .cse71 20))) (.cse4 (not (< .cse71 0))) (.cse0 (mod .cse70 4294967296)) (.cse5 (not .cse66)) (.cse3 (mod (+ .cse70 1) 4294967296))) (and (or (not (< 2147483647 .cse0)) .cse1 (not (= .cse2 .cse3)) (not (< 2147483647 .cse3)) .cse4 .cse5) (let ((.cse8 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse27 .cse28))) (let ((.cse7 (div .cse8 20))) (let ((.cse6 (mod .cse7 4294967296))) (or (not (< 2147483647 .cse6)) (not (< 2147483647 (mod (+ .cse7 1) 4294967296))) .cse5 (not (= (mod .cse8 20) 0)) (not (= .cse2 .cse6)))))) (let ((.cse30 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse27 .cse28))) (let ((.cse31 (div .cse30 20))) (let ((.cse29 (mod .cse31 4294967296))) (or (not (= main_~ret~1 .cse29)) (not (<= 0 .cse30)) (not (<= (mod (+ .cse31 1) 4294967296) 2147483647)) .cse5 (not (<= .cse29 2147483647)))))) (let ((.cse32 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse27 .cse28))) (let ((.cse33 (div .cse32 20))) (let ((.cse34 (mod (+ .cse33 1) 4294967296))) (or (= 0 (mod .cse32 20)) (not (< .cse32 0)) (not (<= (mod .cse33 4294967296) 2147483647)) .cse5 (not (= .cse34 .cse2)) (not (< 2147483647 .cse34)))))) (let ((.cse35 (select |v_#memory_int_110| |main_~#x~0.base|))) (let ((.cse36 (select .cse35 .cse37)) (.cse38 (select .cse35 |main_~#x~0.offset|))) (let ((.cse41 (+ (select .cse35 .cse42) (select .cse35 .cse43) (select .cse35 .cse44) (select .cse35 .cse45) (select .cse35 .cse46) (select .cse35 .cse47) (select .cse35 .cse48) .cse36 (select .cse35 .cse49) (select .cse35 .cse50) (select .cse35 .cse51) (select .cse35 .cse52) (select .cse35 .cse53) (select .cse35 .cse54) (select .cse35 .cse55) (select .cse35 .cse56) (select .cse35 .cse57) (select .cse35 .cse58) .cse38 (select .cse35 .cse59)))) (let ((.cse39 (div .cse41 20))) (let ((.cse40 (mod .cse39 4294967296))) (or (not (= (store |v_#memory_int_110| |main_~#x~0.base| (store (store .cse35 |main_~#x~0.offset| .cse36) .cse37 .cse38)) |#memory_int|)) (not (<= (mod (+ .cse39 1) 4294967296) 2147483647)) .cse5 (not (<= .cse40 2147483647)) (not (= (mod .cse41 20) 0)) (not (= .cse40 main_~ret~1)))))))) (or (not (= main_~ret~1 .cse60)) (not (= 0 (mod .cse61 20))) (not (< 2147483647 .cse62)) .cse5 (not (<= .cse60 2147483647))) (or .cse63 (not (= .cse2 .cse64)) .cse5 (not (< 2147483647 .cse64)) .cse65) (or (not (<= .cse64 2147483647)) .cse63 (not (= main_~ret~1 .cse64)) .cse5 .cse65) .cse66 (or (not (< 2147483647 .cse60)) (not (<= 0 .cse61)) .cse5 (not (= .cse2 .cse60)) (not (<= .cse62 2147483647))) (let ((.cse68 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse27 .cse28))) (let ((.cse69 (div .cse68 20))) (let ((.cse67 (mod (+ .cse69 1) 4294967296))) (or (not (= .cse67 main_~ret~1)) (not (< .cse68 0)) (not (< 2147483647 (mod .cse69 4294967296))) (not (<= .cse67 2147483647)) .cse5 (= 0 (mod .cse68 20)))))) (or .cse1 .cse4 (not (<= .cse0 2147483647)) .cse5 (not (= .cse3 main_~ret~1)) (not (<= .cse3 2147483647))))))))))
(assert (not (= (+ |main_~#x~0.offset| 44) (+ |main_~#x~0.offset| 68))))
(check-sat)
(exit)
20190429-UltimateAutomizerSvcomp2019/avg20_true-unreach-call.i_8.smt2 0 → 100644
View file @ 03648c4a
(set-info :smt-lib-version 2.6)
(set-logic QF_ALIA)
(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 2019 [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.
2019-04-27, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus,
Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian
Schilling, Tanja Schindler, Andreas Podelski: Ultimate Automizer
and the Search for Perfect Interpolants - (Competition Contribution).
TACAS (2) 2018: 447-451
[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: Automatic Verification of C and Java Programs: SV-COMP 2019.
TACAS (3) 2019: 133-155
[6] https://sv-comp.sosy-lab.org/2019/
|")
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun |v_#memory_int_110| () (Array Int (Array Int Int)))
(declare-fun |main_~#x~0.base| () Int)
(declare-fun |main_~#x~0.offset| () Int)
(declare-fun main_~ret~1 () Int)
(declare-fun |#memory_int| () (Array Int (Array Int Int)))
(assert (let ((.cse50 (+ |main_~#x~0.offset| 28)) (.cse59 (+ |main_~#x~0.offset| 12)) (.cse42 (+ |main_~#x~0.offset| 72)) (.cse37 (+ |main_~#x~0.offset| 4)) (.cse55 (+ |main_~#x~0.offset| 64)) (.cse43 (+ |main_~#x~0.offset| 76)) (.cse49 (+ |main_~#x~0.offset| 8)) (.cse54 (+ |main_~#x~0.offset| 52)) (.cse44 (+ |main_~#x~0.offset| 44)) (.cse45 (+ |main_~#x~0.offset| 68)) (.cse53 (+ |main_~#x~0.offset| 60)) (.cse57 (+ |main_~#x~0.offset| 56)) (.cse48 (+ |main_~#x~0.offset| 40)) (.cse52 (+ |main_~#x~0.offset| 32)) (.cse47 (+ |main_~#x~0.offset| 20)) (.cse46 (+ |main_~#x~0.offset| 24)) (.cse51 (+ |main_~#x~0.offset| 36)) (.cse58 (+ |main_~#x~0.offset| 48)) (.cse75 (select |#memory_int| |main_~#x~0.base|)) (.cse56 (+ |main_~#x~0.offset| 16))) (let ((.cse9 (select .cse75 .cse56)) (.cse10 (select .cse75 .cse58)) (.cse11 (select .cse75 .cse51)) (.cse12 (select .cse75 .cse46)) (.cse13 (select .cse75 .cse47)) (.cse14 (select .cse75 .cse52)) (.cse16 (select .cse75 .cse48)) (.cse15 (select .cse75 .cse57)) (.cse17 (select .cse75 .cse53)) (.cse18 (select .cse75 .cse45)) (.cse19 (select .cse75 .cse44)) (.cse20 (select .cse75 .cse54)) (.cse21 (select .cse75 |main_~#x~0.offset|)) (.cse22 (select .cse75 .cse49)) (.cse24 (select .cse75 .cse43)) (.cse23 (select .cse75 .cse55)) (.cse25 (select .cse75 .cse37)) (.cse26 (select .cse75 .cse42)) (.cse28 (select .cse75 .cse59)) (.cse27 (select .cse75 .cse50))) (let ((.cse73 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse28 .cse27)) (.cse61 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse28 .cse27)) (.cse71 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse28 .cse27))) (let ((.cse66 (= |main_~#x~0.offset| 0)) (.cse70 (div .cse71 20)) (.cse72 (div .cse61 20)) (.cse74 (div .cse73 20))) (let ((.cse63 (not (< 2147483647 (mod (+ .cse74 1) 4294967296)))) (.cse64 (mod .cse74 4294967296)) (.cse65 (not (<= 0 .cse73))) (.cse2 (+ main_~ret~1 4294967296)) (.cse60 (mod .cse72 4294967296)) (.cse62 (mod (+ .cse72 1) 4294967296)) (.cse1 (= 0 (mod .cse71 20))) (.cse4 (not (< .cse71 0))) (.cse0 (mod .cse70 4294967296)) (.cse5 (not .cse66)) (.cse3 (mod (+ .cse70 1) 4294967296))) (and (or (not (< 2147483647 .cse0)) .cse1 (not (= .cse2 .cse3)) (not (< 2147483647 .cse3)) .cse4 .cse5) (let ((.cse8 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse27 .cse28))) (let ((.cse7 (div .cse8 20))) (let ((.cse6 (mod .cse7 4294967296))) (or (not (< 2147483647 .cse6)) (not (< 2147483647 (mod (+ .cse7 1) 4294967296))) .cse5 (not (= (mod .cse8 20) 0)) (not (= .cse2 .cse6)))))) (let ((.cse30 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse27 .cse28))) (let ((.cse31 (div .cse30 20))) (let ((.cse29 (mod .cse31 4294967296))) (or (not (= main_~ret~1 .cse29)) (not (<= 0 .cse30)) (not (<= (mod (+ .cse31 1) 4294967296) 2147483647)) .cse5 (not (<= .cse29 2147483647)))))) (let ((.cse32 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse27 .cse28))) (let ((.cse33 (div .cse32 20))) (let ((.cse34 (mod (+ .cse33 1) 4294967296))) (or (= 0 (mod .cse32 20)) (not (< .cse32 0)) (not (<= (mod .cse33 4294967296) 2147483647)) .cse5 (not (= .cse34 .cse2)) (not (< 2147483647 .cse34)))))) (let ((.cse35 (select |v_#memory_int_110| |main_~#x~0.base|))) (let ((.cse36 (select .cse35 .cse37)) (.cse38 (select .cse35 |main_~#x~0.offset|))) (let ((.cse41 (+ (select .cse35 .cse42) (select .cse35 .cse43) (select .cse35 .cse44) (select .cse35 .cse45) (select .cse35 .cse46) (select .cse35 .cse47) (select .cse35 .cse48) .cse36 (select .cse35 .cse49) (select .cse35 .cse50) (select .cse35 .cse51) (select .cse35 .cse52) (select .cse35 .cse53) (select .cse35 .cse54) (select .cse35 .cse55) (select .cse35 .cse56) (select .cse35 .cse57) (select .cse35 .cse58) .cse38 (select .cse35 .cse59)))) (let ((.cse39 (div .cse41 20))) (let ((.cse40 (mod .cse39 4294967296))) (or (not (= (store |v_#memory_int_110| |main_~#x~0.base| (store (store .cse35 |main_~#x~0.offset| .cse36) .cse37 .cse38)) |#memory_int|)) (not (<= (mod (+ .cse39 1) 4294967296) 2147483647)) .cse5 (not (<= .cse40 2147483647)) (not (= (mod .cse41 20) 0)) (not (= .cse40 main_~ret~1)))))))) (or (not (= main_~ret~1 .cse60)) (not (= 0 (mod .cse61 20))) (not (< 2147483647 .cse62)) .cse5 (not (<= .cse60 2147483647))) (or .cse63 (not (= .cse2 .cse64)) .cse5 (not (< 2147483647 .cse64)) .cse65) (or (not (<= .cse64 2147483647)) .cse63 (not (= main_~ret~1 .cse64)) .cse5 .cse65) .cse66 (or (not (< 2147483647 .cse60)) (not (<= 0 .cse61)) .cse5 (not (= .cse2 .cse60)) (not (<= .cse62 2147483647))) (let ((.cse68 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse27 .cse28))) (let ((.cse69 (div .cse68 20))) (let ((.cse67 (mod (+ .cse69 1) 4294967296))) (or (not (= .cse67 main_~ret~1)) (not (< .cse68 0)) (not (< 2147483647 (mod .cse69 4294967296))) (not (<= .cse67 2147483647)) .cse5 (= 0 (mod .cse68 20)))))) (or .cse1 .cse4 (not (<= .cse0 2147483647)) .cse5 (not (= .cse3 main_~ret~1)) (not (<= .cse3 2147483647))))))))))
(assert (let ((.cse0 (select |v_#memory_int_110| |main_~#x~0.base|))) (= (select .cse0 (+ |main_~#x~0.offset| 40)) (select .cse0 (+ |main_~#x~0.offset| 12)))))
(check-sat)
(exit)
20190429-UltimateAutomizerSvcomp2019/avg20_true-unreach-call.i_9.smt2 0 → 100644
View file @ 03648c4a
(set-info :smt-lib-version 2.6)
(set-logic QF_ALIA)
(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 2019 [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.
2019-04-27, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus,
Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian
Schilling, Tanja Schindler, Andreas Podelski: Ultimate Automizer
and the Search for Perfect Interpolants - (Competition Contribution).
TACAS (2) 2018: 447-451
[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: Automatic Verification of C and Java Programs: SV-COMP 2019.
TACAS (3) 2019: 133-155
[6] https://sv-comp.sosy-lab.org/2019/
|")
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun |v_#memory_int_110| () (Array Int (Array Int Int)))
(declare-fun |main_~#x~0.base| () Int)
(declare-fun |main_~#x~0.offset| () Int)
(declare-fun main_~ret~1 () Int)
(declare-fun |#memory_int| () (Array Int (Array Int Int)))
(assert (let ((.cse50 (+ |main_~#x~0.offset| 28)) (.cse59 (+ |main_~#x~0.offset| 12)) (.cse42 (+ |main_~#x~0.offset| 72)) (.cse37 (+ |main_~#x~0.offset| 4)) (.cse55 (+ |main_~#x~0.offset| 64)) (.cse43 (+ |main_~#x~0.offset| 76)) (.cse49 (+ |main_~#x~0.offset| 8)) (.cse54 (+ |main_~#x~0.offset| 52)) (.cse44 (+ |main_~#x~0.offset| 44)) (.cse45 (+ |main_~#x~0.offset| 68)) (.cse53 (+ |main_~#x~0.offset| 60)) (.cse57 (+ |main_~#x~0.offset| 56)) (.cse48 (+ |main_~#x~0.offset| 40)) (.cse52 (+ |main_~#x~0.offset| 32)) (.cse47 (+ |main_~#x~0.offset| 20)) (.cse46 (+ |main_~#x~0.offset| 24)) (.cse51 (+ |main_~#x~0.offset| 36)) (.cse58 (+ |main_~#x~0.offset| 48)) (.cse75 (select |#memory_int| |main_~#x~0.base|)) (.cse56 (+ |main_~#x~0.offset| 16))) (let ((.cse9 (select .cse75 .cse56)) (.cse10 (select .cse75 .cse58)) (.cse11 (select .cse75 .cse51)) (.cse12 (select .cse75 .cse46)) (.cse13 (select .cse75 .cse47)) (.cse14 (select .cse75 .cse52)) (.cse16 (select .cse75 .cse48)) (.cse15 (select .cse75 .cse57)) (.cse17 (select .cse75 .cse53)) (.cse18 (select .cse75 .cse45)) (.cse19 (select .cse75 .cse44)) (.cse20 (select .cse75 .cse54)) (.cse21 (select .cse75 |main_~#x~0.offset|)) (.cse22 (select .cse75 .cse49)) (.cse24 (select .cse75 .cse43)) (.cse23 (select .cse75 .cse55)) (.cse25 (select .cse75 .cse37)) (.cse26 (select .cse75 .cse42)) (.cse28 (select .cse75 .cse59)) (.cse27 (select .cse75 .cse50))) (let ((.cse73 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse28 .cse27)) (.cse61 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse28 .cse27)) (.cse71 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse28 .cse27))) (let ((.cse66 (= |main_~#x~0.offset| 0)) (.cse70 (div .cse71 20)) (.cse72 (div .cse61 20)) (.cse74 (div .cse73 20))) (let ((.cse63 (not (< 2147483647 (mod (+ .cse74 1) 4294967296)))) (.cse64 (mod .cse74 4294967296)) (.cse65 (not (<= 0 .cse73))) (.cse2 (+ main_~ret~1 4294967296)) (.cse60 (mod .cse72 4294967296)) (.cse62 (mod (+ .cse72 1) 4294967296)) (.cse1 (= 0 (mod .cse71 20))) (.cse4 (not (< .cse71 0))) (.cse0 (mod .cse70 4294967296)) (.cse5 (not .cse66)) (.cse3 (mod (+ .cse70 1) 4294967296))) (and (or (not (< 2147483647 .cse0)) .cse1 (not (= .cse2 .cse3)) (not (< 2147483647 .cse3)) .cse4 .cse5) (let ((.cse8 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse27 .cse28))) (let ((.cse7 (div .cse8 20))) (let ((.cse6 (mod .cse7 4294967296))) (or (not (< 2147483647 .cse6)) (not (< 2147483647 (mod (+ .cse7 1) 4294967296))) .cse5 (not (= (mod .cse8 20) 0)) (not (= .cse2 .cse6)))))) (let ((.cse30 (+ .cse9 .cse10 .cse11 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse27 .cse28))) (let ((.cse31 (div .cse30 20))) (let ((.cse29 (mod .cse31 4294967296))) (or (not (= main_~ret~1 .cse29)) (not (<= 0 .cse30)) (not (<= (mod (+ .cse31 1) 4294967296) 2147483647)) .cse5 (not (<= .cse29 2147483647)))))) (let ((.cse32 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse15 .cse16 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse23 .cse24 .cse25 .cse26 .cse27 .cse28))) (let ((.cse33 (div .cse32 20))) (let ((.cse34 (mod (+ .cse33 1) 4294967296))) (or (= 0 (mod .cse32 20)) (not (< .cse32 0)) (not (<= (mod .cse33 4294967296) 2147483647)) .cse5 (not (= .cse34 .cse2)) (not (< 2147483647 .cse34)))))) (let ((.cse35 (select |v_#memory_int_110| |main_~#x~0.base|))) (let ((.cse36 (select .cse35 .cse37)) (.cse38 (select .cse35 |main_~#x~0.offset|))) (let ((.cse41 (+ (select .cse35 .cse42) (select .cse35 .cse43) (select .cse35 .cse44) (select .cse35 .cse45) (select .cse35 .cse46) (select .cse35 .cse47) (select .cse35 .cse48) .cse36 (select .cse35 .cse49) (select .cse35 .cse50) (select .cse35 .cse51) (select .cse35 .cse52) (select .cse35 .cse53) (select .cse35 .cse54) (select .cse35 .cse55) (select .cse35 .cse56) (select .cse35 .cse57) (select .cse35 .cse58) .cse38 (select .cse35 .cse59)))) (let ((.cse39 (div .cse41 20))) (let ((.cse40 (mod .cse39 4294967296))) (or (not (= (store |v_#memory_int_110| |main_~#x~0.base| (store (store .cse35 |main_~#x~0.offset| .cse36) .cse37 .cse38)) |#memory_int|)) (not (<= (mod (+ .cse39 1) 4294967296) 2147483647)) .cse5 (not (<= .cse40 2147483647)) (not (= (mod .cse41 20) 0)) (not (= .cse40 main_~ret~1)))))))) (or (not (= main_~ret~1 .cse60)) (not (= 0 (mod .cse61 20))) (not (< 2147483647 .cse62)) .cse5 (not (<= .cse60 2147483647))) (or .cse63 (not (= .cse2 .cse64)) .cse5 (not (< 2147483647 .cse64)) .cse65) (or (not (<= .cse64 2147483647)) .cse63 (not (= main_~ret~1 .cse64)) .cse5 .cse65) .cse66 (or (not (< 2147483647 .cse60)) (not (<= 0 .cse61)) .cse5 (not (= .cse2 .cse60)) (not (<= .cse62 2147483647))) (let ((.cse68 (+ .cse9 .cse11 .cse10 .cse12 .cse13 .cse14 .cse16 .cse15 .cse17 .cse18 .cse19 .cse20 .cse21 .cse22 .cse24 .cse23 .cse25 .cse26 .cse27 .cse28))) (let ((.cse69 (div .cse68 20))) (let ((.cse67 (mod (+ .cse69 1) 4294967296))) (or (not (= .cse67 main_~ret~1)) (not (< .cse68 0)) (not (< 2147483647 (mod .cse69 4294967296))) (not (<= .cse67 2147483647)) .cse5 (= 0 (mod .cse68 20)))))) (or .cse1 .cse4 (not (<= .cse0 2147483647)) .cse5 (not (= .cse3 main_~ret~1)) (not (<= .cse3 2147483647))))))))))
(assert (let ((.cse0 (select |v_#memory_int_110| |main_~#x~0.base|))) (= (select .cse0 (+ |main_~#x~0.offset| 64)) (select .cse0 (+ |main_~#x~0.offset| 72)))))
(check-sat)
(exit)
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment