tests for qf_ania and qf_aufnia

tests/regress/mcsat/avg20_true-unreach-call.i_9.smt2

@@ -0,0 +1,40 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_ANIA)
+(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)

tests/regress/mcsat/avg20_true-unreach-call.i_9.smt2.gold

@@ -0,0 +1 @@
+sat