Commit e359e664 authored by Mathias Preiner's avatar Mathias Preiner
Browse files

Squashed commit of the following:

commit 3cbdf538
Author: Mathias Preiner <mathias.preiner@gmail.com>
Date:   Fri May 13 15:38:29 2022 -0700

    Moved benchmarks with Real to BVFPLRA.
parent e893f0ed
(set-info :smt-lib-version 2.6)
(set-logic BVFP)
(set-info :source |
Generated by the tool Ultimate Automizer [1,2] which implements
an automata theoretic approach [3] to software verification.
This SMT script belongs to a set of SMT scripts that was generated by
applying Ultimate Automizer to benchmarks [4] from the SV-COMP 2017 [5,6].
This script might _not_ contain all SMT commands that are used by
Ultimate Automizer. In order to satisfy the restrictions of
the SMT-COMP we have to drop e.g., the commands for getting
values (resp. models), unsatisfiable cores and interpolants.
2017-05-01, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Wen Chen, Daniel Dietsch, Marius Greitschus,
Alexander Nutz, Betim Musa, Claus Schätzle, Christian Schilling,
Frank Schüssele, Andreas Podelski:
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare
Automata - (Competition Contribution). TACAS (2) 2017: 394-398
[3] Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Software Model
Checking for People Who Love Automata. CAV 2013:36-52
[4] https://github.com/sosy-lab/sv-benchmarks
[5] Dirk Beyer: Software Verification with Validation of Results -
(Report on SV-COMP 2017). TACAS (2) 2017: 331-349
[6] https://sv-comp.sosy-lab.org/2017/
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun ~unnamed0~FALSE () (_ BitVec 32))
(declare-fun ~unnamed0~TRUE () (_ BitVec 32))
(assert (= ~unnamed0~FALSE (_ bv0 32)))
(assert (= ~unnamed0~TRUE (_ bv1 32)))
(declare-fun ~X~8_const_-29249129 () (_ FloatingPoint 8 24))
(assert (let ((~X~8 ~X~8_const_-29249129)) (and (exists ((~Y~8 (_ FloatingPoint 8 24))) (and (fp.geq ~Y~8 (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq ~Y~8 ((_ to_fp 8 24) RNE 1.0)) (= ~X~8 (fp.add RNE (fp.add RNE (fp.mul RNE ((_ to_fp 8 24) RNE 0.50000001) ~Y~8) (fp.mul RNE ((_ to_fp 8 24) RNE 0.30000001) ~Y~8)) (fp.mul RNE ((_ to_fp 8 24) RNE 0.20000001) ~Y~8))))) (not (fp.geq ~X~8 (fp.neg ((_ to_fp 8 24) RNE 5.0)))))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic BVFP)
(set-info :source |
Generated by the tool Ultimate Automizer [1,2] which implements
an automata theoretic approach [3] to software verification.
This SMT script belongs to a set of SMT scripts that was generated by
applying Ultimate Automizer to benchmarks [4] from the SV-COMP 2017 [5,6].
This script might _not_ contain all SMT commands that are used by
Ultimate Automizer. In order to satisfy the restrictions of
the SMT-COMP we have to drop e.g., the commands for getting
values (resp. models), unsatisfiable cores and interpolants.
2017-05-01, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Wen Chen, Daniel Dietsch, Marius Greitschus,
Alexander Nutz, Betim Musa, Claus Schätzle, Christian Schilling,
Frank Schüssele, Andreas Podelski:
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare
Automata - (Competition Contribution). TACAS (2) 2017: 394-398
[3] Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Software Model
Checking for People Who Love Automata. CAV 2013:36-52
[4] https://github.com/sosy-lab/sv-benchmarks
[5] Dirk Beyer: Software Verification with Validation of Results -
(Report on SV-COMP 2017). TACAS (2) 2017: 331-349
[6] https://sv-comp.sosy-lab.org/2017/
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun ~unnamed0~FALSE () (_ BitVec 32))
(declare-fun ~unnamed0~TRUE () (_ BitVec 32))
(declare-fun c_~X~8 () (_ FloatingPoint 8 24))
(assert (= ~unnamed0~FALSE (_ bv0 32)))
(assert (= ~unnamed0~TRUE (_ bv1 32)))
(assert (not (exists ((~Y~8 (_ FloatingPoint 8 24))) (and (fp.geq ~Y~8 (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq ~Y~8 ((_ to_fp 8 24) RNE 1.0)) (= c_~X~8 (fp.add RNE (fp.add RNE (fp.mul RNE ((_ to_fp 8 24) RNE 0.50000001) ~Y~8) (fp.mul RNE ((_ to_fp 8 24) RNE 0.30000001) ~Y~8)) (fp.mul RNE ((_ to_fp 8 24) RNE 0.20000001) ~Y~8)))))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic BVFP)
(set-info :source |
Generated by the tool Ultimate Automizer [1,2] which implements
an automata theoretic approach [3] to software verification.
This SMT script belongs to a set of SMT scripts that was generated by
applying Ultimate Automizer to benchmarks [4] from the SV-COMP 2017 [5,6].
This script might _not_ contain all SMT commands that are used by
Ultimate Automizer. In order to satisfy the restrictions of
the SMT-COMP we have to drop e.g., the commands for getting
values (resp. models), unsatisfiable cores and interpolants.
2017-05-01, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Wen Chen, Daniel Dietsch, Marius Greitschus,
Alexander Nutz, Betim Musa, Claus Schätzle, Christian Schilling,
Frank Schüssele, Andreas Podelski:
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare
Automata - (Competition Contribution). TACAS (2) 2017: 394-398
[3] Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Software Model
Checking for People Who Love Automata. CAV 2013:36-52
[4] https://github.com/sosy-lab/sv-benchmarks
[5] Dirk Beyer: Software Verification with Validation of Results -
(Report on SV-COMP 2017). TACAS (2) 2017: 331-349
[6] https://sv-comp.sosy-lab.org/2017/
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun ~unnamed0~FALSE () (_ BitVec 32))
(declare-fun ~unnamed0~TRUE () (_ BitVec 32))
(assert (= ~unnamed0~FALSE (_ bv0 32)))
(assert (= ~unnamed0~TRUE (_ bv1 32)))
(declare-fun ~X~8_const_-29249129 () (_ FloatingPoint 8 24))
(assert (let ((~X~8 ~X~8_const_-29249129)) (and (exists ((~Y~8 (_ FloatingPoint 8 24))) (and (fp.geq ~Y~8 (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq ~Y~8 ((_ to_fp 8 24) RNE 1.0)) (= ~X~8 (fp.add RNE (fp.add RNE (fp.mul RNE ((_ to_fp 8 24) RNE 0.50000001) ~Y~8) (fp.mul RNE ((_ to_fp 8 24) RNE 0.30000001) ~Y~8)) (fp.mul RNE ((_ to_fp 8 24) RNE 0.20000001) ~Y~8))))) (or (not (fp.geq ~X~8 (fp.neg ((_ to_fp 8 24) RNE 5.0)))) (not (fp.leq ~X~8 ((_ to_fp 8 24) RNE 5.0)))))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic BVFP)
(set-info :source |
Generated by the tool Ultimate Automizer [1,2] which implements
an automata theoretic approach [3] to software verification.
This SMT script belongs to a set of SMT scripts that was generated by
applying Ultimate Automizer to benchmarks [4] from the SV-COMP 2017 [5,6].
This script might _not_ contain all SMT commands that are used by
Ultimate Automizer. In order to satisfy the restrictions of
the SMT-COMP we have to drop e.g., the commands for getting
values (resp. models), unsatisfiable cores and interpolants.
2017-05-01, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Wen Chen, Daniel Dietsch, Marius Greitschus,
Alexander Nutz, Betim Musa, Claus Schätzle, Christian Schilling,
Frank Schüssele, Andreas Podelski:
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare
Automata - (Competition Contribution). TACAS (2) 2017: 394-398
[3] Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Software Model
Checking for People Who Love Automata. CAV 2013:36-52
[4] https://github.com/sosy-lab/sv-benchmarks
[5] Dirk Beyer: Software Verification with Validation of Results -
(Report on SV-COMP 2017). TACAS (2) 2017: 331-349
[6] https://sv-comp.sosy-lab.org/2017/
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun ~unnamed0~FALSE () (_ BitVec 32))
(declare-fun ~unnamed0~TRUE () (_ BitVec 32))
(assert (= ~unnamed0~FALSE (_ bv0 32)))
(assert (= ~unnamed0~TRUE (_ bv1 32)))
(declare-fun ~X~8_const_-29249129 () (_ FloatingPoint 8 24))
(assert (let ((~X~8 ~X~8_const_-29249129)) (and (exists ((~Y~8 (_ FloatingPoint 8 24))) (and (fp.geq ~Y~8 (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq ~Y~8 ((_ to_fp 8 24) RNE 1.0)) (= ~X~8 (fp.add RNE (fp.add RNE (fp.mul RNE ((_ to_fp 8 24) RNE 0.50000001) ~Y~8) (fp.mul RNE ((_ to_fp 8 24) RNE 0.30000001) ~Y~8)) (fp.mul RNE ((_ to_fp 8 24) RNE 0.20000001) ~Y~8))))) (not (fp.leq ~X~8 ((_ to_fp 8 24) RNE 5.0))))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic BVFP)
(set-info :source |
Generated by the tool Ultimate Automizer [1,2] which implements
an automata theoretic approach [3] to software verification.
This SMT script belongs to a set of SMT scripts that was generated by
applying Ultimate Automizer to benchmarks [4] from the SV-COMP 2017 [5,6].
This script might _not_ contain all SMT commands that are used by
Ultimate Automizer. In order to satisfy the restrictions of
the SMT-COMP we have to drop e.g., the commands for getting
values (resp. models), unsatisfiable cores and interpolants.
2017-05-01, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Wen Chen, Daniel Dietsch, Marius Greitschus,
Alexander Nutz, Betim Musa, Claus Schätzle, Christian Schilling,
Frank Schüssele, Andreas Podelski:
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare
Automata - (Competition Contribution). TACAS (2) 2017: 394-398
[3] Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Software Model
Checking for People Who Love Automata. CAV 2013:36-52
[4] https://github.com/sosy-lab/sv-benchmarks
[5] Dirk Beyer: Software Verification with Validation of Results -
(Report on SV-COMP 2017). TACAS (2) 2017: 331-349
[6] https://sv-comp.sosy-lab.org/2017/
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun ~unnamed0~FALSE () (_ BitVec 32))
(declare-fun ~unnamed0~TRUE () (_ BitVec 32))
(declare-fun c_~C1 () (_ FloatingPoint 8 24))
(declare-fun c_~I () (_ FloatingPoint 8 24))
(declare-fun c_~X~8 () (_ FloatingPoint 8 24))
(assert (= ~unnamed0~FALSE (_ bv0 32)))
(assert (= ~unnamed0~TRUE (_ bv1 32)))
(assert (and (fp.gt c_~C1 (_ +zero 8 24)) (fp.geq c_~I (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq c_~I ((_ to_fp 8 24) RNE 1.0))))
(assert (not (and (fp.gt c_~C1 (_ +zero 8 24)) (fp.geq c_~I (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq c_~I ((_ to_fp 8 24) RNE 1.0)) (exists ((~Y~8 (_ FloatingPoint 8 24))) (and (fp.geq ~Y~8 (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq ~Y~8 ((_ to_fp 8 24) RNE 1.0)) (= c_~X~8 (fp.add RNE (fp.add RNE (fp.mul RNE ((_ to_fp 8 24) RNE 0.50000001) ~Y~8) (fp.mul RNE ((_ to_fp 8 24) RNE 0.30000001) ~Y~8)) (fp.mul RNE ((_ to_fp 8 24) RNE 0.20000001) ~Y~8))))))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic BVFP)
(set-info :source |
Generated by the tool Ultimate Automizer [1,2] which implements
an automata theoretic approach [3] to software verification.
This SMT script belongs to a set of SMT scripts that was generated by
applying Ultimate Automizer to benchmarks [4] from the SV-COMP 2017 [5,6].
This script might _not_ contain all SMT commands that are used by
Ultimate Automizer. In order to satisfy the restrictions of
the SMT-COMP we have to drop e.g., the commands for getting
values (resp. models), unsatisfiable cores and interpolants.
2017-05-01, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Wen Chen, Daniel Dietsch, Marius Greitschus,
Alexander Nutz, Betim Musa, Claus Schätzle, Christian Schilling,
Frank Schüssele, Andreas Podelski:
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare
Automata - (Competition Contribution). TACAS (2) 2017: 394-398
[3] Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Software Model
Checking for People Who Love Automata. CAV 2013:36-52
[4] https://github.com/sosy-lab/sv-benchmarks
[5] Dirk Beyer: Software Verification with Validation of Results -
(Report on SV-COMP 2017). TACAS (2) 2017: 331-349
[6] https://sv-comp.sosy-lab.org/2017/
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun ~unnamed0~FALSE () (_ BitVec 32))
(declare-fun ~unnamed0~TRUE () (_ BitVec 32))
(declare-fun c_~C1 () (_ FloatingPoint 8 24))
(declare-fun c_~I () (_ FloatingPoint 8 24))
(declare-fun c_~X~8 () (_ FloatingPoint 8 24))
(declare-fun c_~Y~8 () (_ FloatingPoint 8 24))
(declare-fun c_~Z~8 () (_ FloatingPoint 8 24))
(assert (= ~unnamed0~FALSE (_ bv0 32)))
(assert (= ~unnamed0~TRUE (_ bv1 32)))
(assert (and (fp.gt c_~C1 (_ +zero 8 24)) (fp.leq c_~Z~8 ((_ to_fp 8 24) RNE 1.0)) (= c_~X~8 c_~I) (fp.geq c_~Z~8 (fp.neg ((_ to_fp 8 24) RNE 1.0))) (= c_~X~8 c_~Z~8) (= c_~X~8 c_~Y~8)))
(assert (not (and (fp.gt c_~C1 (_ +zero 8 24)) (fp.geq c_~I (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq c_~I ((_ to_fp 8 24) RNE 1.0)) (exists ((~Y~8 (_ FloatingPoint 8 24))) (and (fp.geq ~Y~8 (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq ~Y~8 ((_ to_fp 8 24) RNE 1.0)) (= c_~X~8 (fp.add RNE (fp.add RNE (fp.mul RNE ((_ to_fp 8 24) RNE 0.50000001) ~Y~8) (fp.mul RNE ((_ to_fp 8 24) RNE 0.30000001) ~Y~8)) (fp.mul RNE ((_ to_fp 8 24) RNE 0.20000001) ~Y~8))))))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic BVFP)
(set-info :source |
Generated by the tool Ultimate Automizer [1,2] which implements
an automata theoretic approach [3] to software verification.
This SMT script belongs to a set of SMT scripts that was generated by
applying Ultimate Automizer to benchmarks [4] from the SV-COMP 2017 [5,6].
This script might _not_ contain all SMT commands that are used by
Ultimate Automizer. In order to satisfy the restrictions of
the SMT-COMP we have to drop e.g., the commands for getting
values (resp. models), unsatisfiable cores and interpolants.
2017-05-01, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Wen Chen, Daniel Dietsch, Marius Greitschus,
Alexander Nutz, Betim Musa, Claus Schätzle, Christian Schilling,
Frank Schüssele, Andreas Podelski:
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare
Automata - (Competition Contribution). TACAS (2) 2017: 394-398
[3] Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Software Model
Checking for People Who Love Automata. CAV 2013:36-52
[4] https://github.com/sosy-lab/sv-benchmarks
[5] Dirk Beyer: Software Verification with Validation of Results -
(Report on SV-COMP 2017). TACAS (2) 2017: 331-349
[6] https://sv-comp.sosy-lab.org/2017/
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun ~unnamed0~FALSE () (_ BitVec 32))
(declare-fun ~unnamed0~TRUE () (_ BitVec 32))
(declare-fun c_~C1 () (_ FloatingPoint 8 24))
(declare-fun c_~I () (_ FloatingPoint 8 24))
(declare-fun c_~X~8 () (_ FloatingPoint 8 24))
(declare-fun c_~Y~8 () (_ FloatingPoint 8 24))
(declare-fun c_~Z~8 () (_ FloatingPoint 8 24))
(declare-fun |c___VERIFIER_assert_#in~cond| () (_ BitVec 32))
(assert (= ~unnamed0~FALSE (_ bv0 32)))
(assert (= ~unnamed0~TRUE (_ bv1 32)))
(assert (and (fp.gt c_~C1 (_ +zero 8 24)) (fp.leq c_~Z~8 ((_ to_fp 8 24) RNE 1.0)) (= c_~X~8 c_~I) (fp.geq c_~Z~8 (fp.neg ((_ to_fp 8 24) RNE 1.0))) (= (bvadd |c___VERIFIER_assert_#in~cond| (_ bv4294967295 32)) (_ bv0 32)) (= c_~X~8 c_~Z~8) (= c_~X~8 c_~Y~8)))
(assert (not (and (fp.gt c_~C1 (_ +zero 8 24)) (fp.geq c_~I (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq c_~I ((_ to_fp 8 24) RNE 1.0)) (exists ((~Y~8 (_ FloatingPoint 8 24))) (and (fp.geq ~Y~8 (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq ~Y~8 ((_ to_fp 8 24) RNE 1.0)) (= c_~X~8 (fp.add RNE (fp.add RNE (fp.mul RNE ((_ to_fp 8 24) RNE 0.50000001) ~Y~8) (fp.mul RNE ((_ to_fp 8 24) RNE 0.30000001) ~Y~8)) (fp.mul RNE ((_ to_fp 8 24) RNE 0.20000001) ~Y~8))))))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic BVFP)
(set-info :source |
Generated by the tool Ultimate Automizer [1,2] which implements
an automata theoretic approach [3] to software verification.
This SMT script belongs to a set of SMT scripts that was generated by
applying Ultimate Automizer to benchmarks [4] from the SV-COMP 2017 [5,6].
This script might _not_ contain all SMT commands that are used by
Ultimate Automizer. In order to satisfy the restrictions of
the SMT-COMP we have to drop e.g., the commands for getting
values (resp. models), unsatisfiable cores and interpolants.
2017-05-01, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Wen Chen, Daniel Dietsch, Marius Greitschus,
Alexander Nutz, Betim Musa, Claus Schätzle, Christian Schilling,
Frank Schüssele, Andreas Podelski:
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare
Automata - (Competition Contribution). TACAS (2) 2017: 394-398
[3] Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Software Model
Checking for People Who Love Automata. CAV 2013:36-52
[4] https://github.com/sosy-lab/sv-benchmarks
[5] Dirk Beyer: Software Verification with Validation of Results -
(Report on SV-COMP 2017). TACAS (2) 2017: 331-349
[6] https://sv-comp.sosy-lab.org/2017/
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun ~unnamed0~FALSE () (_ BitVec 32))
(declare-fun ~unnamed0~TRUE () (_ BitVec 32))
(declare-fun c_~C1 () (_ FloatingPoint 8 24))
(declare-fun c_~I () (_ FloatingPoint 8 24))
(declare-fun c_~X~8 () (_ FloatingPoint 8 24))
(declare-fun c_~Y~8 () (_ FloatingPoint 8 24))
(declare-fun c_~Z~8 () (_ FloatingPoint 8 24))
(declare-fun |c___VERIFIER_assert_#in~cond| () (_ BitVec 32))
(declare-fun c___VERIFIER_assert_~cond () (_ BitVec 32))
(assert (= ~unnamed0~FALSE (_ bv0 32)))
(assert (= ~unnamed0~TRUE (_ bv1 32)))
(assert (and (fp.gt c_~C1 (_ +zero 8 24)) (fp.leq c_~Z~8 ((_ to_fp 8 24) RNE 1.0)) (= c_~X~8 c_~I) (fp.geq c_~Z~8 (fp.neg ((_ to_fp 8 24) RNE 1.0))) (= c_~X~8 c_~Z~8) (= (bvadd c___VERIFIER_assert_~cond (_ bv4294967295 32)) (_ bv0 32)) (= c_~X~8 c_~Y~8) (= c___VERIFIER_assert_~cond |c___VERIFIER_assert_#in~cond|)))
(assert (not (and (fp.gt c_~C1 (_ +zero 8 24)) (fp.geq c_~I (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq c_~I ((_ to_fp 8 24) RNE 1.0)) (exists ((~Y~8 (_ FloatingPoint 8 24))) (and (fp.geq ~Y~8 (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq ~Y~8 ((_ to_fp 8 24) RNE 1.0)) (= c_~X~8 (fp.add RNE (fp.add RNE (fp.mul RNE ((_ to_fp 8 24) RNE 0.50000001) ~Y~8) (fp.mul RNE ((_ to_fp 8 24) RNE 0.30000001) ~Y~8)) (fp.mul RNE ((_ to_fp 8 24) RNE 0.20000001) ~Y~8))))))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic BVFP)
(set-info :source |
Generated by the tool Ultimate Automizer [1,2] which implements
an automata theoretic approach [3] to software verification.
This SMT script belongs to a set of SMT scripts that was generated by
applying Ultimate Automizer to benchmarks [4] from the SV-COMP 2017 [5,6].
This script might _not_ contain all SMT commands that are used by
Ultimate Automizer. In order to satisfy the restrictions of
the SMT-COMP we have to drop e.g., the commands for getting
values (resp. models), unsatisfiable cores and interpolants.
2017-05-01, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Wen Chen, Daniel Dietsch, Marius Greitschus,
Alexander Nutz, Betim Musa, Claus Schätzle, Christian Schilling,
Frank Schüssele, Andreas Podelski:
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare
Automata - (Competition Contribution). TACAS (2) 2017: 394-398
[3] Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Software Model
Checking for People Who Love Automata. CAV 2013:36-52
[4] https://github.com/sosy-lab/sv-benchmarks
[5] Dirk Beyer: Software Verification with Validation of Results -
(Report on SV-COMP 2017). TACAS (2) 2017: 331-349
[6] https://sv-comp.sosy-lab.org/2017/
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun ~unnamed0~FALSE () (_ BitVec 32))
(declare-fun ~unnamed0~TRUE () (_ BitVec 32))
(declare-fun c_~C1 () (_ FloatingPoint 8 24))
(declare-fun c_~I () (_ FloatingPoint 8 24))
(declare-fun c_~X~8 () (_ FloatingPoint 8 24))
(declare-fun |c___VERIFIER_assert_#in~cond| () (_ BitVec 32))
(declare-fun c___VERIFIER_assert_~cond () (_ BitVec 32))
(assert (= ~unnamed0~FALSE (_ bv0 32)))
(assert (= ~unnamed0~TRUE (_ bv1 32)))
(assert (and (fp.gt c_~C1 (_ +zero 8 24)) (fp.geq c_~I (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq c_~I ((_ to_fp 8 24) RNE 1.0)) (= c___VERIFIER_assert_~cond |c___VERIFIER_assert_#in~cond|)))
(assert (not (and (fp.gt c_~C1 (_ +zero 8 24)) (fp.geq c_~I (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq c_~I ((_ to_fp 8 24) RNE 1.0)) (exists ((~Y~8 (_ FloatingPoint 8 24))) (and (fp.geq ~Y~8 (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq ~Y~8 ((_ to_fp 8 24) RNE 1.0)) (= c_~X~8 (fp.add RNE (fp.add RNE (fp.mul RNE ((_ to_fp 8 24) RNE 0.50000001) ~Y~8) (fp.mul RNE ((_ to_fp 8 24) RNE 0.30000001) ~Y~8)) (fp.mul RNE ((_ to_fp 8 24) RNE 0.20000001) ~Y~8))))))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic BVFP)
(set-info :source |
Generated by the tool Ultimate Automizer [1,2] which implements
an automata theoretic approach [3] to software verification.
This SMT script belongs to a set of SMT scripts that was generated by
applying Ultimate Automizer to benchmarks [4] from the SV-COMP 2017 [5,6].
This script might _not_ contain all SMT commands that are used by
Ultimate Automizer. In order to satisfy the restrictions of
the SMT-COMP we have to drop e.g., the commands for getting
values (resp. models), unsatisfiable cores and interpolants.
2017-05-01, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Wen Chen, Daniel Dietsch, Marius Greitschus,
Alexander Nutz, Betim Musa, Claus Schätzle, Christian Schilling,
Frank Schüssele, Andreas Podelski:
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare
Automata - (Competition Contribution). TACAS (2) 2017: 394-398
[3] Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Software Model
Checking for People Who Love Automata. CAV 2013:36-52
[4] https://github.com/sosy-lab/sv-benchmarks
[5] Dirk Beyer: Software Verification with Validation of Results -
(Report on SV-COMP 2017). TACAS (2) 2017: 331-349
[6] https://sv-comp.sosy-lab.org/2017/
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun ~unnamed0~FALSE () (_ BitVec 32))
(declare-fun ~unnamed0~TRUE () (_ BitVec 32))
(declare-fun c_~C1 () (_ FloatingPoint 8 24))
(declare-fun c_~I () (_ FloatingPoint 8 24))
(declare-fun c_~X~8 () (_ FloatingPoint 8 24))
(declare-fun |c___VERIFIER_assert_#in~cond| () (_ BitVec 32))
(declare-fun c___VERIFIER_assert_~cond () (_ BitVec 32))
(assert (= ~unnamed0~FALSE (_ bv0 32)))
(assert (= ~unnamed0~TRUE (_ bv1 32)))
(assert (and (distinct |c___VERIFIER_assert_#in~cond| (_ bv0 32)) (fp.gt c_~C1 (_ +zero 8 24)) (fp.geq c_~I (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq c_~I ((_ to_fp 8 24) RNE 1.0)) (= c___VERIFIER_assert_~cond |c___VERIFIER_assert_#in~cond|)))
(assert (not (and (fp.gt c_~C1 (_ +zero 8 24)) (fp.geq c_~I (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq c_~I ((_ to_fp 8 24) RNE 1.0)) (exists ((~Y~8 (_ FloatingPoint 8 24))) (and (fp.geq ~Y~8 (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq ~Y~8 ((_ to_fp 8 24) RNE 1.0)) (= c_~X~8 (fp.add RNE (fp.add RNE (fp.mul RNE ((_ to_fp 8 24) RNE 0.50000001) ~Y~8) (fp.mul RNE ((_ to_fp 8 24) RNE 0.30000001) ~Y~8)) (fp.mul RNE ((_ to_fp 8 24) RNE 0.20000001) ~Y~8))))))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic BVFP)
(set-info :source |
Generated by the tool Ultimate Automizer [1,2] which implements
an automata theoretic approach [3] to software verification.
This SMT script belongs to a set of SMT scripts that was generated by
applying Ultimate Automizer to benchmarks [4] from the SV-COMP 2017 [5,6].
This script might _not_ contain all SMT commands that are used by
Ultimate Automizer. In order to satisfy the restrictions of
the SMT-COMP we have to drop e.g., the commands for getting
values (resp. models), unsatisfiable cores and interpolants.
2017-05-01, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Wen Chen, Daniel Dietsch, Marius Greitschus,
Alexander Nutz, Betim Musa, Claus Schätzle, Christian Schilling,
Frank Schüssele, Andreas Podelski:
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare
Automata - (Competition Contribution). TACAS (2) 2017: 394-398
[3] Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Software Model
Checking for People Who Love Automata. CAV 2013:36-52
[4] https://github.com/sosy-lab/sv-benchmarks
[5] Dirk Beyer: Software Verification with Validation of Results -
(Report on SV-COMP 2017). TACAS (2) 2017: 331-349
[6] https://sv-comp.sosy-lab.org/2017/
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun ~unnamed0~FALSE () (_ BitVec 32))
(declare-fun ~unnamed0~TRUE () (_ BitVec 32))
(declare-fun c_~C1 () (_ FloatingPoint 8 24))
(declare-fun c_~I () (_ FloatingPoint 8 24))
(declare-fun c_~X~8 () (_ FloatingPoint 8 24))
(declare-fun c_~Y~8 () (_ FloatingPoint 8 24))
(declare-fun c_~Z~8 () (_ FloatingPoint 8 24))
(declare-fun |c_RANDOM_INPUT_#res| () (_ FloatingPoint 8 24))
(assert (= ~unnamed0~FALSE (_ bv0 32)))
(assert (= ~unnamed0~TRUE (_ bv1 32)))
(assert (and (fp.gt c_~C1 (_ +zero 8 24)) (fp.geq |c_RANDOM_INPUT_#res| (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq c_~Z~8 ((_ to_fp 8 24) RNE 1.0)) (= c_~X~8 c_~I) (fp.geq c_~Z~8 (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq |c_RANDOM_INPUT_#res| ((_ to_fp 8 24) RNE 1.0)) (= c_~X~8 c_~Z~8) (= c_~X~8 c_~Y~8)))
(assert (not (and (fp.gt c_~C1 (_ +zero 8 24)) (fp.geq c_~I (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq c_~I ((_ to_fp 8 24) RNE 1.0)) (exists ((~Y~8 (_ FloatingPoint 8 24))) (and (fp.geq ~Y~8 (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq ~Y~8 ((_ to_fp 8 24) RNE 1.0)) (= c_~X~8 (fp.add RNE (fp.add RNE (fp.mul RNE ((_ to_fp 8 24) RNE 0.50000001) ~Y~8) (fp.mul RNE ((_ to_fp 8 24) RNE 0.30000001) ~Y~8)) (fp.mul RNE ((_ to_fp 8 24) RNE 0.20000001) ~Y~8))))))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic BVFP)
(set-info :source |
Generated by the tool Ultimate Automizer [1,2] which implements
an automata theoretic approach [3] to software verification.
This SMT script belongs to a set of SMT scripts that was generated by
applying Ultimate Automizer to benchmarks [4] from the SV-COMP 2017 [5,6].
This script might _not_ contain all SMT commands that are used by
Ultimate Automizer. In order to satisfy the restrictions of
the SMT-COMP we have to drop e.g., the commands for getting
values (resp. models), unsatisfiable cores and interpolants.
2017-05-01, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Wen Chen, Daniel Dietsch, Marius Greitschus,
Alexander Nutz, Betim Musa, Claus Schätzle, Christian Schilling,
Frank Schüssele, Andreas Podelski:
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare
Automata - (Competition Contribution). TACAS (2) 2017: 394-398
[3] Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Software Model
Checking for People Who Love Automata. CAV 2013:36-52
[4] https://github.com/sosy-lab/sv-benchmarks
[5] Dirk Beyer: Software Verification with Validation of Results -
(Report on SV-COMP 2017). TACAS (2) 2017: 331-349
[6] https://sv-comp.sosy-lab.org/2017/
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun ~unnamed0~FALSE () (_ BitVec 32))
(declare-fun ~unnamed0~TRUE () (_ BitVec 32))
(declare-fun c_~C1 () (_ FloatingPoint 8 24))
(declare-fun c_~I () (_ FloatingPoint 8 24))
(declare-fun c_~X~8 () (_ FloatingPoint 8 24))
(declare-fun |c_RANDOM_INPUT_#res| () (_ FloatingPoint 8 24))
(assert (= ~unnamed0~FALSE (_ bv0 32)))
(assert (= ~unnamed0~TRUE (_ bv1 32)))
(assert (and (fp.gt c_~C1 (_ +zero 8 24)) (fp.geq c_~I (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.geq |c_RANDOM_INPUT_#res| (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq c_~I ((_ to_fp 8 24) RNE 1.0)) (fp.leq |c_RANDOM_INPUT_#res| ((_ to_fp 8 24) RNE 1.0))))
(assert (not (and (fp.gt c_~C1 (_ +zero 8 24)) (fp.geq c_~I (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq c_~I ((_ to_fp 8 24) RNE 1.0)) (exists ((~Y~8 (_ FloatingPoint 8 24))) (and (fp.geq ~Y~8 (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq ~Y~8 ((_ to_fp 8 24) RNE 1.0)) (= c_~X~8 (fp.add RNE (fp.add RNE (fp.mul RNE ((_ to_fp 8 24) RNE 0.50000001) ~Y~8) (fp.mul RNE ((_ to_fp 8 24) RNE 0.30000001) ~Y~8)) (fp.mul RNE ((_ to_fp 8 24) RNE 0.20000001) ~Y~8))))))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic BVFP)
(set-info :source |
Generated by the tool Ultimate Automizer [1,2] which implements
an automata theoretic approach [3] to software verification.
This SMT script belongs to a set of SMT scripts that was generated by
applying Ultimate Automizer to benchmarks [4] from the SV-COMP 2017 [5,6].
This script might _not_ contain all SMT commands that are used by
Ultimate Automizer. In order to satisfy the restrictions of
the SMT-COMP we have to drop e.g., the commands for getting
values (resp. models), unsatisfiable cores and interpolants.
2017-05-01, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Wen Chen, Daniel Dietsch, Marius Greitschus,
Alexander Nutz, Betim Musa, Claus Schätzle, Christian Schilling,
Frank Schüssele, Andreas Podelski:
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare
Automata - (Competition Contribution). TACAS (2) 2017: 394-398
[3] Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Software Model
Checking for People Who Love Automata. CAV 2013:36-52
[4] https://github.com/sosy-lab/sv-benchmarks
[5] Dirk Beyer: Software Verification with Validation of Results -
(Report on SV-COMP 2017). TACAS (2) 2017: 331-349
[6] https://sv-comp.sosy-lab.org/2017/
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun ~unnamed0~FALSE () (_ BitVec 32))
(declare-fun ~unnamed0~TRUE () (_ BitVec 32))
(declare-fun c_~C1 () (_ FloatingPoint 8 24))
(declare-fun c_~I () (_ FloatingPoint 8 24))
(declare-fun c_~X~8 () (_ FloatingPoint 8 24))
(declare-fun c_~Y~8 () (_ FloatingPoint 8 24))
(declare-fun c_~Z~8 () (_ FloatingPoint 8 24))
(assert (= ~unnamed0~FALSE (_ bv0 32)))
(assert (= ~unnamed0~TRUE (_ bv1 32)))
(assert (and (fp.gt c_~C1 (_ +zero 8 24)) (fp.geq c_~I (fp.neg ((_ to_fp 8 24) RNE 1.0))) (fp.leq c_~I ((_ to_fp 8 24) RNE 1.0)) (fp.leq c_~Z~8 ((_ to_fp 8 24) RNE 1.0)) (fp.geq c_~Z~8 (fp.neg ((_ to_fp 8 24) RNE 1.0))) (= c_~X~8 c_~Z~8) (= c_~X~8 c_~Y~8)))