Squashed commit of the following:

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

    Move benchmarks from pending repository.

20190429-UltimateAutomizerSvcomp2019/alternating_list_true-unreach-call_true-valid-memsafety.i_0.smt2

+(set-info :smt-lib-version 2.6)
+(set-logic 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 ~unnamed0~0~P_ALL () Int)
+(declare-fun ~unnamed0~0~P_PID () Int)
+(declare-fun ~unnamed0~0~P_PGID () Int)
+(declare-fun |c_#valid| () (Array Int Bool))
+(declare-fun |c_#memory_int| () (Array Int (Array Int Int)))
+(declare-fun c_main_~a~0.base () Int)
+(declare-fun c_main_~a~0.offset () Int)
+(declare-fun c_main_~p~0.base () Int)
+(declare-fun c_main_~p~0.offset () Int)
+(assert (= ~unnamed0~0~P_ALL 0))
+(assert (= ~unnamed0~0~P_PID 1))
+(assert (= 2 ~unnamed0~0~P_PGID))
+(assert (and (or (forall ((|v_main_#t~malloc4.base_2| Int)) (select |c_#valid| |v_main_#t~malloc4.base_2|)) (forall ((v_DerPreprocessor_1 Int)) (= 1 (select (select (store |c_#memory_int| c_main_~p~0.base (store (select |c_#memory_int| c_main_~p~0.base) (+ c_main_~p~0.offset 4) v_DerPreprocessor_1)) c_main_~a~0.base) c_main_~a~0.offset)))) (select |c_#valid| c_main_~a~0.base)))
+(assert (not (and (not (= c_main_~a~0.base c_main_~p~0.base)) (= 1 (select (select |c_#memory_int| c_main_~a~0.base) c_main_~a~0.offset)))))
+(check-sat)
+(exit)

20190429-UltimateAutomizerSvcomp2019/alternating_list_true-unreach-call_true-valid-memsafety.i_1.smt2

+(set-info :smt-lib-version 2.6)
+(set-logic 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 ~unnamed0~0~P_ALL () Int)
+(declare-fun ~unnamed0~0~P_PID () Int)
+(declare-fun ~unnamed0~0~P_PGID () Int)
+(assert (= ~unnamed0~0~P_ALL 0))
+(assert (= ~unnamed0~0~P_PID 1))
+(assert (= 2 ~unnamed0~0~P_PGID))
+(declare-fun main_~p~0.base () Int)
+(declare-fun main_~p~0.offset () Int)
+(declare-fun main_~a~0.offset () Int)
+(declare-fun main_~a~0.base () Int)
+(declare-fun |#memory_int| () (Array Int (Array Int Int)))
+(declare-fun |#valid| () (Array Int Bool))
+(assert (select |#valid| main_~a~0.base))
+(assert (not (forall ((v_DerPreprocessor_1 Int)) (= 1 (select (select (store |#memory_int| main_~p~0.base (store (select |#memory_int| main_~p~0.base) (+ main_~p~0.offset 4) v_DerPreprocessor_1)) main_~a~0.base) main_~a~0.offset)))))
+(assert (forall ((|v_main_#t~malloc4.base_2| Int)) (select |#valid| |v_main_#t~malloc4.base_2|)))
+(check-sat)
+(exit)

20190429-UltimateAutomizerSvcomp2019/alternating_list_true-unreach-call_true-valid-memsafety.i_2.smt2

+(set-info :smt-lib-version 2.6)
+(set-logic 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 ~unnamed0~0~P_ALL () Int)
+(declare-fun ~unnamed0~0~P_PID () Int)
+(declare-fun ~unnamed0~0~P_PGID () Int)
+(declare-fun |c_#valid| () (Array Int Bool))
+(declare-fun |c_#memory_$Pointer$.base| () (Array Int (Array Int Int)))
+(declare-fun |c_#memory_$Pointer$.offset| () (Array Int (Array Int Int)))
+(declare-fun c_main_~a~0.base () Int)
+(declare-fun c_main_~a~0.offset () Int)
+(declare-fun c_main_~p~0.base () Int)
+(declare-fun c_main_~p~0.offset () Int)
+(assert (= ~unnamed0~0~P_ALL 0))
+(assert (= ~unnamed0~0~P_PID 1))
+(assert (= 2 ~unnamed0~0~P_PGID))
+(assert (let ((.cse0 (forall ((|v_main_#t~malloc4.base_3| Int)) (select |c_#valid| |v_main_#t~malloc4.base_3|)))) (and (or (= c_main_~a~0.base c_main_~p~0.base) .cse0) (or .cse0 (= c_main_~a~0.offset c_main_~p~0.offset)) (select |c_#valid| c_main_~a~0.base))))
+(assert (not (and (forall ((v_DerPreprocessor_3 Int)) (= c_main_~p~0.offset (select (select (store |c_#memory_$Pointer$.offset| c_main_~p~0.base (store (select |c_#memory_$Pointer$.offset| c_main_~p~0.base) c_main_~p~0.offset v_DerPreprocessor_3)) c_main_~a~0.base) (+ c_main_~a~0.offset 4)))) (forall ((v_DerPreprocessor_4 Int)) (= (select (select (store |c_#memory_$Pointer$.base| c_main_~p~0.base (store (select |c_#memory_$Pointer$.base| c_main_~p~0.base) c_main_~p~0.offset v_DerPreprocessor_4)) c_main_~a~0.base) (+ c_main_~a~0.offset 4)) c_main_~p~0.base)))))
+(check-sat)
+(exit)

20190429-UltimateAutomizerSvcomp2019/dll-queue_false-unreach-call_false-valid-memcleanup.i_0.smt2

+(set-info :smt-lib-version 2.6)
+(set-logic 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 ~unnamed0~0~P_ALL () Int)
+(declare-fun ~unnamed0~0~P_PID () Int)
+(declare-fun ~unnamed0~0~P_PGID () Int)
+(assert (= ~unnamed0~0~P_ALL 0))
+(assert (= ~unnamed0~0~P_PID 1))
+(assert (= 2 ~unnamed0~0~P_PGID))
+(declare-fun main_~head~0.base () Int)
+(declare-fun |#memory_$Pointer$.base| () (Array Int (Array Int Int)))
+(declare-fun main_~item~0.base () Int)
+(declare-fun main_~head~0.offset () Int)
+(declare-fun main_~item~0.offset () Int)
+(assert (not (let ((.cse1 (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset))) (let ((.cse0 (select (select |#memory_$Pointer$.base| .cse1) 8))) (and (= 0 main_~head~0.offset) (= main_~item~0.base .cse0) (not (= .cse1 main_~head~0.base)) (not (= .cse1 0)) (= 0 (select (select |#memory_$Pointer$.base| main_~item~0.base) main_~item~0.offset)) (not (= main_~head~0.base .cse0)) (not (= .cse1 .cse0)))))))
+(assert (not (let ((.cse2 (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset))) (and (= 0 main_~head~0.offset) (exists ((v_main_~item~0.offset_25 Int)) (let ((.cse0 (= v_main_~item~0.offset_25 8)) (.cse1 (select |#memory_$Pointer$.base| (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset)))) (and (or (= 0 main_~head~0.base) (not .cse0)) (= (select .cse1 v_main_~item~0.offset_25) main_~item~0.base) (or .cse0 (= main_~head~0.base (select .cse1 8)))))) (not (= .cse2 main_~head~0.base)) (not (= .cse2 main_~item~0.base)) (not (= .cse2 0)) (= 0 (select (select |#memory_$Pointer$.base| main_~item~0.base) main_~item~0.offset)) (not (= main_~item~0.base main_~head~0.base))))))
+(assert (let ((.cse0 (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset))) (and (= 0 main_~head~0.offset) (= main_~item~0.base (select (select |#memory_$Pointer$.base| .cse0) (- 8))) (not (= .cse0 main_~head~0.base)) (not (= .cse0 main_~item~0.base)) (not (= .cse0 0)) (= 0 (select (select |#memory_$Pointer$.base| main_~item~0.base) main_~item~0.offset)) (not (= main_~item~0.base main_~head~0.base)))))
+(check-sat)
+(exit)

20190429-UltimateAutomizerSvcomp2019/dll-queue_false-unreach-call_false-valid-memcleanup.i_1.smt2

+(set-info :smt-lib-version 2.6)
+(set-logic 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 ~unnamed0~0~P_ALL () Int)
+(declare-fun ~unnamed0~0~P_PID () Int)
+(declare-fun ~unnamed0~0~P_PGID () Int)
+(assert (= ~unnamed0~0~P_ALL 0))
+(assert (= ~unnamed0~0~P_PID 1))
+(assert (= 2 ~unnamed0~0~P_PGID))
+(declare-fun main_~head~0.base () Int)
+(declare-fun |#memory_$Pointer$.base| () (Array Int (Array Int Int)))
+(declare-fun main_~item~0.base () Int)
+(declare-fun main_~head~0.offset () Int)
+(declare-fun main_~item~0.offset () Int)
+(assert (not (let ((.cse1 (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset))) (let ((.cse0 (select (select |#memory_$Pointer$.base| .cse1) 8))) (and (= 0 main_~head~0.offset) (= main_~item~0.base .cse0) (not (= .cse1 main_~head~0.base)) (not (= .cse1 0)) (= 0 (select (select |#memory_$Pointer$.base| main_~item~0.base) main_~item~0.offset)) (not (= main_~head~0.base .cse0)) (not (= .cse1 .cse0)))))))
+(assert (not (let ((.cse2 (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset))) (and (= 0 main_~head~0.offset) (exists ((v_main_~item~0.offset_25 Int)) (let ((.cse0 (= v_main_~item~0.offset_25 8)) (.cse1 (select |#memory_$Pointer$.base| (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset)))) (and (or (= 0 main_~head~0.base) (not .cse0)) (= (select .cse1 v_main_~item~0.offset_25) main_~item~0.base) (or .cse0 (= main_~head~0.base (select .cse1 8)))))) (not (= .cse2 main_~head~0.base)) (not (= .cse2 main_~item~0.base)) (not (= .cse2 0)) (= 0 (select (select |#memory_$Pointer$.base| main_~item~0.base) main_~item~0.offset)) (not (= main_~item~0.base main_~head~0.base))))))
+(assert (not (= main_~item~0.base main_~head~0.base)))
+(assert (= 0 (select (select |#memory_$Pointer$.base| main_~item~0.base) main_~item~0.offset)))
+(assert (not (= (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset) 0)))
+(assert (not (= (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset) main_~item~0.base)))
+(assert (= 0 main_~head~0.offset))
+(assert (= main_~item~0.base (select (select |#memory_$Pointer$.base| (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset)) (- 8))))
+(assert (not (= (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset) main_~head~0.base)))
+(check-sat)
+(exit)

20190429-UltimateAutomizerSvcomp2019/dll-queue_false-unreach-call_false-valid-memcleanup.i_10.smt2

+(set-info :smt-lib-version 2.6)
+(set-logic 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 ~unnamed0~0~P_ALL () Int)
+(declare-fun ~unnamed0~0~P_PID () Int)
+(declare-fun ~unnamed0~0~P_PGID () Int)
+(declare-fun |c_#valid| () (Array Int Bool))
+(declare-fun |c_#memory_$Pointer$.base| () (Array Int (Array Int Int)))
+(declare-fun c_main_~head~0.base () Int)
+(declare-fun c_main_~head~0.offset () Int)
+(declare-fun c_main_~item~0.base () Int)
+(declare-fun c_main_~item~0.offset () Int)
+(assert (= ~unnamed0~0~P_ALL 0))
+(assert (= ~unnamed0~0~P_PID 1))
+(assert (= 2 ~unnamed0~0~P_PGID))
+(assert (let ((.cse2 (= 0 c_main_~head~0.base)) (.cse3 (select |c_#valid| c_main_~head~0.base)) (.cse0 (and (= c_main_~head~0.offset c_main_~item~0.offset) (= c_main_~item~0.base c_main_~head~0.base)))) (and (forall ((|v_main_#t~malloc2.base_5| Int)) (or (select (store |c_#valid| |v_main_#t~malloc2.base_5| true) c_main_~head~0.base) (= |v_main_#t~malloc2.base_5| 0) (= |v_main_#t~malloc2.base_5| c_main_~head~0.base) (select |c_#valid| |v_main_#t~malloc2.base_5|))) (or .cse0 (let ((.cse1 (= 8 c_main_~head~0.offset))) (and (forall ((v_prenex_27 Int) (v_prenex_26 Int)) (or (select (store |c_#valid| v_prenex_27 true) v_prenex_26) (select |c_#valid| v_prenex_27) (= v_prenex_27 c_main_~head~0.base) (= v_prenex_27 0))) (forall ((v_prenex_34 Int) (v_prenex_35 Int)) (or (= v_prenex_34 c_main_~head~0.base) (= v_prenex_35 0) (select (store |c_#valid| v_prenex_35 true) v_prenex_34) (= v_prenex_35 c_main_~head~0.base) (select |c_#valid| v_prenex_35))) (or (forall ((v_prenex_30 Int) (v_prenex_31 Int)) (or (= v_prenex_30 c_main_~head~0.base) (select (store |c_#valid| v_prenex_31 true) v_prenex_30) (= v_prenex_31 0) (select |c_#valid| v_prenex_31) (= v_prenex_31 c_main_~head~0.base))) .cse1) (or (and (forall ((v_prenex_21 Int) (v_prenex_20 Int)) (or (select |c_#valid| v_prenex_21) (= v_prenex_21 c_main_~head~0.base) (= v_prenex_21 0) (select (store |c_#valid| v_prenex_21 true) v_prenex_20))) (forall ((v_prenex_29 Int) (v_prenex_28 Int)) (or (select (store |c_#valid| v_prenex_29 true) v_prenex_28) (= v_prenex_29 0) (= v_prenex_29 c_main_~head~0.base) (= v_prenex_28 c_main_~head~0.base) (select |c_#valid| v_prenex_29)))) .cse1) (or (and (forall ((v_prenex_18 Int) (v_prenex_19 Int)) (or (select |c_#valid| v_prenex_19) (select (store |c_#valid| v_prenex_19 true) v_prenex_18) (= v_prenex_18 c_main_~head~0.base) (= v_prenex_19 0))) (forall ((v_prenex_23 Int) (v_prenex_22 Int)) (or (select (store |c_#valid| v_prenex_23 true) v_prenex_22) (select |c_#valid| v_prenex_23) (= v_prenex_23 0)))) .cse1) (or .cse1 (forall ((v_prenex_25 Int) (v_prenex_24 Int)) (or (select (store |c_#valid| v_prenex_25 true) v_prenex_24) (= v_prenex_24 c_main_~head~0.base) (= v_prenex_25 0) (select |c_#valid| v_prenex_25))))))) (or (forall ((v_prenex_33 Int)) (select (store |c_#valid| c_main_~head~0.base true) v_prenex_33)) .cse2 (not (= c_main_~item~0.base 0)) .cse3) (forall ((v_prenex_32 Int)) (or (select (store |c_#valid| v_prenex_32 true) c_main_~head~0.base) (= v_prenex_32 0) (= v_prenex_32 c_main_~head~0.base) (select |c_#valid| v_prenex_32))) (or .cse2 .cse3 (forall ((v_prenex_36 Int)) (select (store |c_#valid| c_main_~head~0.base true) v_prenex_36))) (forall ((v_prenex_40 Int) (v_main_~item~0.offset_27 Int)) (let ((.cse4 (= v_prenex_40 c_main_~head~0.base))) (or (select |c_#valid| v_prenex_40) (= v_prenex_40 0) (select (store |c_#valid| v_prenex_40 true) c_main_~head~0.base) (and .cse4 (= (+ v_main_~item~0.offset_27 16) c_main_~head~0.offset)) .cse4))) (or .cse2 .cse3 (select (store |c_#valid| c_main_~head~0.base true) 0)) (forall ((v_prenex_37 Int)) (or (select (store |c_#valid| v_prenex_37 true) c_main_~head~0.base) (= v_prenex_37 0) (select |c_#valid| v_prenex_37))) (or .cse0 (forall ((v_prenex_38 Int) (|v_main_#t~malloc2.offset_4| Int) (v_prenex_39 Int) (v_prenex_40 Int) (v_main_~item~0.offset_27 Int)) (let ((.cse5 (= v_prenex_40 c_main_~head~0.base)) (.cse6 (= v_prenex_39 c_main_~head~0.base))) (or (select |c_#valid| v_prenex_40) (= v_prenex_40 0) (and .cse5 (= 8 c_main_~head~0.offset)) (and .cse5 (= (+ v_main_~item~0.offset_27 16) c_main_~head~0.offset)) (and (= (+ |v_main_#t~malloc2.offset_4| 8) c_main_~head~0.offset) .cse6) .cse5 (and (= (+ v_prenex_38 16) c_main_~head~0.offset) .cse6) (select (store |c_#valid| v_prenex_40 true) v_prenex_39))))))))
+(assert (not (forall ((|v_main_#t~malloc2.offset_4| Int) (|v_main_#t~malloc2.base_4| Int) (v_DerPreprocessor_3 Int) (v_main_~item~0.offset_26 Int) (v_DerPreprocessor_2 Int)) (or (not (= 0 (select (select (let ((.cse0 (let ((.cse2 (store |c_#memory_$Pointer$.base| c_main_~item~0.base (store (store (select |c_#memory_$Pointer$.base| c_main_~item~0.base) (+ c_main_~item~0.offset 16) v_DerPreprocessor_3) c_main_~item~0.offset |v_main_#t~malloc2.base_4|)))) (store .cse2 |v_main_#t~malloc2.base_4| (store (select .cse2 |v_main_#t~malloc2.base_4|) (+ |v_main_#t~malloc2.offset_4| 8) c_main_~item~0.base))))) (let ((.cse1 (select (select .cse0 c_main_~item~0.base) c_main_~item~0.offset))) (store .cse0 .cse1 (store (store (select .cse0 .cse1) v_main_~item~0.offset_26 0) (+ v_main_~item~0.offset_26 16) v_DerPreprocessor_2)))) c_main_~head~0.base) c_main_~head~0.offset))) (select |c_#valid| |v_main_#t~malloc2.base_4|)))))
+(check-sat)
+(exit)

20190429-UltimateAutomizerSvcomp2019/dll-queue_false-unreach-call_false-valid-memcleanup.i_11.smt2

+(set-info :smt-lib-version 2.6)
+(set-logic 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 ~unnamed0~0~P_ALL () Int)
+(declare-fun ~unnamed0~0~P_PID () Int)
+(declare-fun ~unnamed0~0~P_PGID () Int)
+(declare-fun |c_#valid| () (Array Int Bool))
+(declare-fun |c_#memory_$Pointer$.base| () (Array Int (Array Int Int)))
+(declare-fun c_main_~head~0.base () Int)
+(declare-fun c_main_~head~0.offset () Int)
+(declare-fun c_main_~item~0.base () Int)
+(declare-fun c_main_~item~0.offset () Int)
+(assert (= ~unnamed0~0~P_ALL 0))
+(assert (= ~unnamed0~0~P_PID 1))
+(assert (= 2 ~unnamed0~0~P_PGID))
+(assert (let ((.cse4 (forall ((v_prenex_39 Int) (v_prenex_40 Int)) (or (select |c_#valid| v_prenex_40) (= v_prenex_40 0) (= v_prenex_40 c_main_~head~0.base) (select (store |c_#valid| v_prenex_40 true) v_prenex_39)))) (.cse1 (= c_main_~head~0.offset c_main_~item~0.offset)) (.cse2 (forall ((v_prenex_41 Int) (v_prenex_42 Int)) (or (select (store |c_#valid| v_prenex_42 true) v_prenex_41) (select |c_#valid| v_prenex_42) (= v_prenex_42 c_main_~head~0.base) (= v_prenex_42 0) (= v_prenex_41 c_main_~head~0.base)))) (.cse3 (= 8 c_main_~head~0.offset)) (.cse6 (forall ((v_prenex_45 Int) (v_prenex_46 Int)) (or (= v_prenex_46 c_main_~head~0.base) (= v_prenex_45 c_main_~head~0.base) (= v_prenex_46 0) (select |c_#valid| v_prenex_46) (select (store |c_#valid| v_prenex_46 true) v_prenex_45)))) (.cse0 (forall ((v_prenex_44 Int) (v_prenex_43 Int)) (or (= v_prenex_44 0) (select (store |c_#valid| v_prenex_44 true) v_prenex_43) (= v_prenex_44 c_main_~head~0.base) (select |c_#valid| v_prenex_44)))) (.cse5 (= c_main_~item~0.base c_main_~head~0.base))) (and (or .cse0 .cse1) (or .cse2 .cse1 .cse3) (or .cse1 .cse4 .cse3) (or .cse4 .cse5 .cse3) (or .cse6 .cse1) (or .cse2 .cse5 .cse3) (or (select |c_#valid| c_main_~head~0.base) (select (store |c_#valid| c_main_~head~0.base true) 0)) (or .cse6 .cse5) (or .cse0 .cse5) (forall ((v_prenex_37 Int)) (or (select (store |c_#valid| v_prenex_37 true) c_main_~head~0.base) (= v_prenex_37 0) (select |c_#valid| v_prenex_37))))))
+(assert (not (forall ((|v_main_#t~malloc2.offset_4| Int) (|v_main_#t~malloc2.base_4| Int) (v_main_~item~0.offset_26 Int) (v_DerPreprocessor_2 Int)) (or (not (= 0 (select (select (let ((.cse0 (let ((.cse2 (store |c_#memory_$Pointer$.base| c_main_~item~0.base (store (select |c_#memory_$Pointer$.base| c_main_~item~0.base) c_main_~item~0.offset |v_main_#t~malloc2.base_4|)))) (store .cse2 |v_main_#t~malloc2.base_4| (store (select .cse2 |v_main_#t~malloc2.base_4|) (+ |v_main_#t~malloc2.offset_4| 8) c_main_~item~0.base))))) (let ((.cse1 (select (select .cse0 c_main_~item~0.base) c_main_~item~0.offset))) (store .cse0 .cse1 (store (store (select .cse0 .cse1) v_main_~item~0.offset_26 0) (+ v_main_~item~0.offset_26 16) v_DerPreprocessor_2)))) c_main_~head~0.base) c_main_~head~0.offset))) (select |c_#valid| |v_main_#t~malloc2.base_4|)))))
+(check-sat)
+(exit)

20190429-UltimateAutomizerSvcomp2019/dll-queue_false-unreach-call_false-valid-memcleanup.i_12.smt2

+(set-info :smt-lib-version 2.6)
+(set-logic 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 sat)
+(declare-fun ~unnamed0~0~P_ALL () Int)
+(declare-fun ~unnamed0~0~P_PID () Int)
+(declare-fun ~unnamed0~0~P_PGID () Int)
+(assert (= ~unnamed0~0~P_ALL 0))
+(assert (= ~unnamed0~0~P_PID 1))
+(assert (= 2 ~unnamed0~0~P_PGID))
+(declare-fun main_~item~0.offset () Int)
+(declare-fun |#valid| () (Array Int Bool))
+(declare-fun main_~head~0.base () Int)
+(declare-fun |#memory_$Pointer$.base| () (Array Int (Array Int Int)))
+(declare-fun main_~item~0.base () Int)
+(declare-fun main_~head~0.offset () Int)
+(assert (forall ((|v_main_#t~malloc2.offset_4| Int) (|v_main_#t~malloc2.base_4| Int) (v_DerPreprocessor_3 Int) (v_main_~item~0.offset_26 Int) (v_DerPreprocessor_2 Int)) (or (not (= 0 (select (select (let ((.cse0 (let ((.cse2 (store |#memory_$Pointer$.base| main_~item~0.base (store (store (select |#memory_$Pointer$.base| main_~item~0.base) (+ main_~item~0.offset 16) v_DerPreprocessor_3) main_~item~0.offset |v_main_#t~malloc2.base_4|)))) (store .cse2 |v_main_#t~malloc2.base_4| (store (select .cse2 |v_main_#t~malloc2.base_4|) (+ |v_main_#t~malloc2.offset_4| 8) main_~item~0.base))))) (let ((.cse1 (select (select .cse0 main_~item~0.base) main_~item~0.offset))) (store .cse0 .cse1 (store (store (select .cse0 .cse1) v_main_~item~0.offset_26 0) (+ v_main_~item~0.offset_26 16) v_DerPreprocessor_2)))) main_~head~0.base) main_~head~0.offset))) (select |#valid| |v_main_#t~malloc2.base_4|))))
+(assert (not (let ((.cse10 (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset))) (let ((.cse4 (not (= .cse10 main_~item~0.base))) (.cse7 (not (= main_~item~0.base main_~head~0.base))) (.cse0 (= 0 main_~head~0.offset)) (.cse3 (not (= .cse10 main_~head~0.base))) (.cse5 (not (= .cse10 0))) (.cse6 (= 0 (select (select |#memory_$Pointer$.base| main_~item~0.base) main_~item~0.offset))) (.cse8 (select |#memory_$Pointer$.base| .cse10))) (or (and .cse0 (exists ((v_main_~item~0.offset_25 Int)) (let ((.cse1 (= v_main_~item~0.offset_25 8)) (.cse2 (select |#memory_$Pointer$.base| (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset)))) (and (or (= 0 main_~head~0.base) (not .cse1)) (= (select .cse2 v_main_~item~0.offset_25) main_~item~0.base) (or .cse1 (= main_~head~0.base (select .cse2 8)))))) .cse3 .cse4 .cse5 .cse6 .cse7) (and .cse0 (= main_~item~0.base (select .cse8 (- 8))) .cse3 .cse4 .cse5 .cse6 .cse7) (let ((.cse9 (select .cse8 8))) (and .cse0 (= main_~item~0.base .cse9) .cse3 .cse5 .cse6 (not (= main_~head~0.base .cse9)) (not (= .cse10 .cse9)))))))))
+(check-sat)
+(exit)

20190429-UltimateAutomizerSvcomp2019/dll-queue_false-unreach-call_false-valid-memcleanup.i_13.smt2

+(set-info :smt-lib-version 2.6)
+(set-logic 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 ~unnamed0~0~P_ALL () Int)
+(declare-fun ~unnamed0~0~P_PID () Int)
+(declare-fun ~unnamed0~0~P_PGID () Int)
+(assert (= ~unnamed0~0~P_ALL 0))
+(assert (= ~unnamed0~0~P_PID 1))
+(assert (= 2 ~unnamed0~0~P_PGID))
+(declare-fun main_~item~0.offset () Int)
+(declare-fun |#valid| () (Array Int Bool))
+(declare-fun main_~head~0.base () Int)
+(declare-fun |#memory_$Pointer$.base| () (Array Int (Array Int Int)))
+(declare-fun main_~item~0.base () Int)
+(declare-fun main_~head~0.offset () Int)
+(assert (forall ((|v_main_#t~malloc2.offset_4| Int) (|v_main_#t~malloc2.base_4| Int) (v_DerPreprocessor_3 Int) (v_main_~item~0.offset_26 Int) (v_DerPreprocessor_2 Int)) (or (not (= 0 (select (select (let ((.cse0 (let ((.cse2 (store |#memory_$Pointer$.base| main_~item~0.base (store (store (select |#memory_$Pointer$.base| main_~item~0.base) (+ main_~item~0.offset 16) v_DerPreprocessor_3) main_~item~0.offset |v_main_#t~malloc2.base_4|)))) (store .cse2 |v_main_#t~malloc2.base_4| (store (select .cse2 |v_main_#t~malloc2.base_4|) (+ |v_main_#t~malloc2.offset_4| 8) main_~item~0.base))))) (let ((.cse1 (select (select .cse0 main_~item~0.base) main_~item~0.offset))) (store .cse0 .cse1 (store (store (select .cse0 .cse1) v_main_~item~0.offset_26 0) (+ v_main_~item~0.offset_26 16) v_DerPreprocessor_2)))) main_~head~0.base) main_~head~0.offset))) (select |#valid| |v_main_#t~malloc2.base_4|))))
+(assert (not (let ((.cse1 (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset))) (let ((.cse0 (select (select |#memory_$Pointer$.base| .cse1) 8))) (and (= 0 main_~head~0.offset) (= main_~item~0.base .cse0) (not (= .cse1 main_~head~0.base)) (not (= .cse1 0)) (= 0 (select (select |#memory_$Pointer$.base| main_~item~0.base) main_~item~0.offset)) (not (= main_~head~0.base .cse0)) (not (= .cse1 .cse0)))))))
+(assert (not (let ((.cse0 (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset))) (and (= 0 main_~head~0.offset) (= main_~item~0.base (select (select |#memory_$Pointer$.base| .cse0) (- 8))) (not (= .cse0 main_~head~0.base)) (not (= .cse0 main_~item~0.base)) (not (= .cse0 0)) (= 0 (select (select |#memory_$Pointer$.base| main_~item~0.base) main_~item~0.offset)) (not (= main_~item~0.base main_~head~0.base))))))
+(assert (not (let ((.cse2 (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset))) (and (= 0 main_~head~0.offset) (exists ((v_main_~item~0.offset_25 Int)) (let ((.cse0 (= v_main_~item~0.offset_25 8)) (.cse1 (select |#memory_$Pointer$.base| (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset)))) (and (or (= 0 main_~head~0.base) (not .cse0)) (= (select .cse1 v_main_~item~0.offset_25) main_~item~0.base) (or .cse0 (= main_~head~0.base (select .cse1 8)))))) (not (= .cse2 main_~head~0.base)) (not (= .cse2 main_~item~0.base)) (not (= .cse2 0)) (= 0 (select (select |#memory_$Pointer$.base| main_~item~0.base) main_~item~0.offset)) (not (= main_~item~0.base main_~head~0.base))))))
+(check-sat)
+(exit)

20190429-UltimateAutomizerSvcomp2019/dll-queue_false-unreach-call_false-valid-memcleanup.i_14.smt2

+(set-info :smt-lib-version 2.6)
+(set-logic 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 ~unnamed0~0~P_ALL () Int)
+(declare-fun ~unnamed0~0~P_PID () Int)
+(declare-fun ~unnamed0~0~P_PGID () Int)
+(assert (= ~unnamed0~0~P_ALL 0))
+(assert (= ~unnamed0~0~P_PID 1))
+(assert (= 2 ~unnamed0~0~P_PGID))
+(declare-fun main_~item~0.offset () Int)
+(declare-fun |#valid| () (Array Int Bool))
+(declare-fun main_~head~0.base () Int)
+(declare-fun |#memory_$Pointer$.base| () (Array Int (Array Int Int)))
+(declare-fun main_~item~0.base () Int)
+(declare-fun main_~head~0.offset () Int)
+(assert (forall ((|v_main_#t~malloc2.offset_4| Int) (|v_main_#t~malloc2.base_4| Int) (v_DerPreprocessor_3 Int) (v_main_~item~0.offset_26 Int) (v_DerPreprocessor_2 Int)) (or (not (= 0 (select (select (let ((.cse0 (let ((.cse2 (store |#memory_$Pointer$.base| main_~item~0.base (store (store (select |#memory_$Pointer$.base| main_~item~0.base) (+ main_~item~0.offset 16) v_DerPreprocessor_3) main_~item~0.offset |v_main_#t~malloc2.base_4|)))) (store .cse2 |v_main_#t~malloc2.base_4| (store (select .cse2 |v_main_#t~malloc2.base_4|) (+ |v_main_#t~malloc2.offset_4| 8) main_~item~0.base))))) (let ((.cse1 (select (select .cse0 main_~item~0.base) main_~item~0.offset))) (store .cse0 .cse1 (store (store (select .cse0 .cse1) v_main_~item~0.offset_26 0) (+ v_main_~item~0.offset_26 16) v_DerPreprocessor_2)))) main_~head~0.base) main_~head~0.offset))) (select |#valid| |v_main_#t~malloc2.base_4|))))
+(assert (not (let ((.cse1 (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset))) (let ((.cse0 (select (select |#memory_$Pointer$.base| .cse1) 8))) (and (= 0 main_~head~0.offset) (= main_~item~0.base .cse0) (not (= .cse1 main_~head~0.base)) (not (= .cse1 0)) (= 0 (select (select |#memory_$Pointer$.base| main_~item~0.base) main_~item~0.offset)) (not (= main_~head~0.base .cse0)) (not (= .cse1 .cse0)))))))
+(assert (not (let ((.cse0 (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset))) (and (= 0 main_~head~0.offset) (= main_~item~0.base (select (select |#memory_$Pointer$.base| .cse0) (- 8))) (not (= .cse0 main_~head~0.base)) (not (= .cse0 main_~item~0.base)) (not (= .cse0 0)) (= 0 (select (select |#memory_$Pointer$.base| main_~item~0.base) main_~item~0.offset)) (not (= main_~item~0.base main_~head~0.base))))))
+(assert (not (= main_~item~0.base main_~head~0.base)))
+(assert (= 0 (select (select |#memory_$Pointer$.base| main_~item~0.base) main_~item~0.offset)))
+(assert (= 0 main_~head~0.offset))
+(assert (exists ((v_main_~item~0.offset_25 Int)) (let ((.cse0 (= v_main_~item~0.offset_25 8)) (.cse1 (select |#memory_$Pointer$.base| (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset)))) (and (or (= 0 main_~head~0.base) (not .cse0)) (= (select .cse1 v_main_~item~0.offset_25) main_~item~0.base) (or .cse0 (= main_~head~0.base (select .cse1 8)))))))
+(assert (not (= (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset) main_~head~0.base)))
+(assert (not (= (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset) main_~item~0.base)))
+(assert (= (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset) 0))
+(check-sat)
+(exit)

20190429-UltimateAutomizerSvcomp2019/dll-queue_false-unreach-call_false-valid-memcleanup.i_15.smt2

+(set-info :smt-lib-version 2.6)
+(set-logic 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 ~unnamed0~0~P_ALL () Int)
+(declare-fun ~unnamed0~0~P_PID () Int)
+(declare-fun ~unnamed0~0~P_PGID () Int)
+(assert (= ~unnamed0~0~P_ALL 0))
+(assert (= ~unnamed0~0~P_PID 1))
+(assert (= 2 ~unnamed0~0~P_PGID))
+(declare-fun main_~item~0.offset () Int)
+(declare-fun |#valid| () (Array Int Bool))
+(declare-fun main_~head~0.base () Int)
+(declare-fun |#memory_$Pointer$.base| () (Array Int (Array Int Int)))
+(declare-fun main_~item~0.base () Int)
+(declare-fun main_~head~0.offset () Int)
+(assert (forall ((|v_main_#t~malloc2.offset_4| Int) (|v_main_#t~malloc2.base_4| Int) (v_DerPreprocessor_3 Int) (v_main_~item~0.offset_26 Int) (v_DerPreprocessor_2 Int)) (or (not (= 0 (select (select (let ((.cse0 (let ((.cse2 (store |#memory_$Pointer$.base| main_~item~0.base (store (store (select |#memory_$Pointer$.base| main_~item~0.base) (+ main_~item~0.offset 16) v_DerPreprocessor_3) main_~item~0.offset |v_main_#t~malloc2.base_4|)))) (store .cse2 |v_main_#t~malloc2.base_4| (store (select .cse2 |v_main_#t~malloc2.base_4|) (+ |v_main_#t~malloc2.offset_4| 8) main_~item~0.base))))) (let ((.cse1 (select (select .cse0 main_~item~0.base) main_~item~0.offset))) (store .cse0 .cse1 (store (store (select .cse0 .cse1) v_main_~item~0.offset_26 0) (+ v_main_~item~0.offset_26 16) v_DerPreprocessor_2)))) main_~head~0.base) main_~head~0.offset))) (select |#valid| |v_main_#t~malloc2.base_4|))))
+(assert (not (let ((.cse1 (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset))) (let ((.cse0 (select (select |#memory_$Pointer$.base| .cse1) 8))) (and (= 0 main_~head~0.offset) (= main_~item~0.base .cse0) (not (= .cse1 main_~head~0.base)) (not (= .cse1 0)) (= 0 (select (select |#memory_$Pointer$.base| main_~item~0.base) main_~item~0.offset)) (not (= main_~head~0.base .cse0)) (not (= .cse1 .cse0)))))))
+(assert (not (let ((.cse2 (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset))) (and (= 0 main_~head~0.offset) (exists ((v_main_~item~0.offset_25 Int)) (let ((.cse0 (= v_main_~item~0.offset_25 8)) (.cse1 (select |#memory_$Pointer$.base| (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset)))) (and (or (= 0 main_~head~0.base) (not .cse0)) (= (select .cse1 v_main_~item~0.offset_25) main_~item~0.base) (or .cse0 (= main_~head~0.base (select .cse1 8)))))) (not (= .cse2 main_~head~0.base)) (not (= .cse2 main_~item~0.base)) (not (= .cse2 0)) (= 0 (select (select |#memory_$Pointer$.base| main_~item~0.base) main_~item~0.offset)) (not (= main_~item~0.base main_~head~0.base))))))
+(assert (not (= main_~item~0.base main_~head~0.base)))
+(assert (= 0 (select (select |#memory_$Pointer$.base| main_~item~0.base) main_~item~0.offset)))
+(assert (= 0 main_~head~0.offset))
+(assert (= main_~item~0.base (select (select |#memory_$Pointer$.base| (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset)) (- 8))))
+(assert (not (= (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset) main_~head~0.base)))
+(assert (not (= (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset) main_~item~0.base)))
+(assert (= (select (select |#memory_$Pointer$.base| main_~head~0.base) main_~head~0.offset) 0))
+(check-sat)
+(exit)

20190429-UltimateAutomizerSvcomp2019/dll-queue_false-unreach-call_false-valid-memcleanup.i_16.smt2

+(set-info :smt-lib-version 2.6)
+(set-logic 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