Commit 82b67319 authored by Mathias Preiner's avatar Mathias Preiner
Browse files

Squashed commit of the following:

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

    Move benchmarks from pending repository.
parent 2426cfab
(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 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 c_currentRoundingMode () RoundingMode)
(declare-fun c_~one_asin~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS0_asin~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS1_asin~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS2_asin~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS3_asin~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS4_asin~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS5_asin~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS1_asin~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS2_asin~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS3_asin~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS4_asin~0 () (_ FloatingPoint 11 53))
(declare-fun |c___ieee754_asin_#in~x| () (_ FloatingPoint 11 53))
(declare-fun |c___ieee754_asin_#res_primed| () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_asin_~x () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_asin_~t~1_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_asin_~w~0_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_asin_~p~0_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_asin_~q~1_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_asin_~hx~0 () (_ BitVec 32))
(declare-fun c___ieee754_asin_~ix~0 () (_ BitVec 32))
(assert (and (= c___ieee754_asin_~p~0_primed (fp.mul c_currentRoundingMode c___ieee754_asin_~t~1_primed (fp.add c_currentRoundingMode c_~pS0_asin~0 (fp.mul c_currentRoundingMode c___ieee754_asin_~t~1_primed (fp.add c_currentRoundingMode c_~pS1_asin~0 (fp.mul c_currentRoundingMode c___ieee754_asin_~t~1_primed (fp.add c_currentRoundingMode c_~pS2_asin~0 (fp.mul c_currentRoundingMode c___ieee754_asin_~t~1_primed (fp.add c_currentRoundingMode c_~pS3_asin~0 (fp.mul c_currentRoundingMode c___ieee754_asin_~t~1_primed (fp.add c_currentRoundingMode c_~pS4_asin~0 (fp.mul c_currentRoundingMode c___ieee754_asin_~t~1_primed c_~pS5_asin~0)))))))))))) (= c___ieee754_asin_~t~1_primed (fp.mul c_currentRoundingMode c___ieee754_asin_~x c___ieee754_asin_~x)) (not (bvslt c___ieee754_asin_~ix~0 (_ bv1044381696 32))) (= c___ieee754_asin_~w~0_primed (fp.div c_currentRoundingMode c___ieee754_asin_~p~0_primed c___ieee754_asin_~q~1_primed)) (= c___ieee754_asin_~q~1_primed (fp.add c_currentRoundingMode c_~one_asin~0 (fp.mul c_currentRoundingMode c___ieee754_asin_~t~1_primed (fp.add c_currentRoundingMode c_~qS1_asin~0 (fp.mul c_currentRoundingMode c___ieee754_asin_~t~1_primed (fp.add c_currentRoundingMode c_~qS2_asin~0 (fp.mul c_currentRoundingMode c___ieee754_asin_~t~1_primed (fp.add c_currentRoundingMode c_~qS3_asin~0 (fp.mul c_currentRoundingMode c___ieee754_asin_~t~1_primed c_~qS4_asin~0))))))))) (= |c___ieee754_asin_#res_primed| (fp.add c_currentRoundingMode c___ieee754_asin_~x (fp.mul c_currentRoundingMode c___ieee754_asin_~x c___ieee754_asin_~w~0_primed)))))
(assert (and (not (bvsge c___ieee754_asin_~ix~0 (_ bv1072693248 32))) (exists ((v_skolemized_v_prenex_5_3 (_ BitVec 64))) (and (= |c___ieee754_asin_#in~x| (fp ((_ extract 63 63) v_skolemized_v_prenex_5_3) ((_ extract 62 52) v_skolemized_v_prenex_5_3) ((_ extract 51 0) v_skolemized_v_prenex_5_3))) (= c___ieee754_asin_~ix~0 (bvand (_ bv2147483647 32) ((_ extract 63 32) v_skolemized_v_prenex_5_3))))) (= |c___ieee754_asin_#in~x| c___ieee754_asin_~x) (exists ((v_skolemized_v_prenex_5_3 (_ BitVec 64))) (and (= |c___ieee754_asin_#in~x| (fp ((_ extract 63 63) v_skolemized_v_prenex_5_3) ((_ extract 62 52) v_skolemized_v_prenex_5_3) ((_ extract 51 0) v_skolemized_v_prenex_5_3))) (= ((_ extract 63 32) v_skolemized_v_prenex_5_3) c___ieee754_asin_~hx~0)))))
(assert (not false))
(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 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 c_currentRoundingMode () RoundingMode)
(declare-fun c_~one_asin~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS0_asin~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS1_asin~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS2_asin~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS3_asin~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS4_asin~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS5_asin~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS1_asin~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS2_asin~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS3_asin~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS4_asin~0 () (_ FloatingPoint 11 53))
(declare-fun |c___ieee754_asin_#in~x| () (_ FloatingPoint 11 53))
(declare-fun |c___ieee754_asin_#res_primed| () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_asin_~x () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_asin_~t~1_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_asin_~w~0_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_asin_~p~0_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_asin_~q~1_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_asin_~hx~0 () (_ BitVec 32))
(declare-fun c___ieee754_asin_~ix~0 () (_ BitVec 32))
(assert (and (= c___ieee754_asin_~w~0_primed (fp.div c_currentRoundingMode c___ieee754_asin_~p~0_primed c___ieee754_asin_~q~1_primed)) (not (bvslt c___ieee754_asin_~ix~0 (_ bv1044381696 32))) (= |c___ieee754_asin_#res_primed| (fp.add c_currentRoundingMode c___ieee754_asin_~x (fp.mul c_currentRoundingMode c___ieee754_asin_~x c___ieee754_asin_~w~0_primed))) (= c___ieee754_asin_~p~0_primed (fp.mul c_currentRoundingMode c___ieee754_asin_~t~1_primed (fp.add c_currentRoundingMode c_~pS0_asin~0 (fp.mul c_currentRoundingMode c___ieee754_asin_~t~1_primed (fp.add c_currentRoundingMode c_~pS1_asin~0 (fp.mul c_currentRoundingMode c___ieee754_asin_~t~1_primed (fp.add c_currentRoundingMode c_~pS2_asin~0 (fp.mul c_currentRoundingMode c___ieee754_asin_~t~1_primed (fp.add c_currentRoundingMode c_~pS3_asin~0 (fp.mul c_currentRoundingMode c___ieee754_asin_~t~1_primed (fp.add c_currentRoundingMode c_~pS4_asin~0 (fp.mul c_currentRoundingMode c___ieee754_asin_~t~1_primed c_~pS5_asin~0)))))))))))) (= c___ieee754_asin_~t~1_primed (fp.mul c_currentRoundingMode c___ieee754_asin_~x c___ieee754_asin_~x)) (= c___ieee754_asin_~q~1_primed (fp.add c_currentRoundingMode c_~one_asin~0 (fp.mul c_currentRoundingMode c___ieee754_asin_~t~1_primed (fp.add c_currentRoundingMode c_~qS1_asin~0 (fp.mul c_currentRoundingMode c___ieee754_asin_~t~1_primed (fp.add c_currentRoundingMode c_~qS2_asin~0 (fp.mul c_currentRoundingMode c___ieee754_asin_~t~1_primed (fp.add c_currentRoundingMode c_~qS3_asin~0 (fp.mul c_currentRoundingMode c___ieee754_asin_~t~1_primed c_~qS4_asin~0)))))))))))
(assert (and (not (bvsge c___ieee754_asin_~ix~0 (_ bv1072693248 32))) (exists ((v_skolemized_v_prenex_5_3 (_ BitVec 64))) (and (= |c___ieee754_asin_#in~x| (fp ((_ extract 63 63) v_skolemized_v_prenex_5_3) ((_ extract 62 52) v_skolemized_v_prenex_5_3) ((_ extract 51 0) v_skolemized_v_prenex_5_3))) (= c___ieee754_asin_~ix~0 (bvand (_ bv2147483647 32) ((_ extract 63 32) v_skolemized_v_prenex_5_3))))) (= |c___ieee754_asin_#in~x| c___ieee754_asin_~x) (exists ((v_skolemized_v_prenex_5_3 (_ BitVec 64))) (and (= |c___ieee754_asin_#in~x| (fp ((_ extract 63 63) v_skolemized_v_prenex_5_3) ((_ extract 62 52) v_skolemized_v_prenex_5_3) ((_ extract 51 0) v_skolemized_v_prenex_5_3))) (= ((_ extract 63 32) v_skolemized_v_prenex_5_3) c___ieee754_asin_~hx~0)))))
(assert (not false))
(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 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 c_currentRoundingMode () RoundingMode)
(declare-fun c_~C1_kcos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~C2_kcos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~C3_kcos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~C4_kcos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~C5_kcos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~C6_kcos~0 () (_ FloatingPoint 11 53))
(declare-fun |c_cos_double_#in~x| () (_ FloatingPoint 11 53))
(declare-fun |c_cos_double_#res| () (_ FloatingPoint 11 53))
(declare-fun c___kernel_cos_~x () (_ FloatingPoint 11 53))
(declare-fun c___kernel_cos_~z~2_primed () (_ FloatingPoint 11 53))
(declare-fun c___kernel_cos_~r~1_primed () (_ FloatingPoint 11 53))
(assert (and (= c___kernel_cos_~r~1_primed (fp.mul c_currentRoundingMode c___kernel_cos_~z~2_primed (fp.add c_currentRoundingMode c_~C1_kcos~0 (fp.mul c_currentRoundingMode c___kernel_cos_~z~2_primed (fp.add c_currentRoundingMode c_~C2_kcos~0 (fp.mul c_currentRoundingMode c___kernel_cos_~z~2_primed (fp.add c_currentRoundingMode c_~C3_kcos~0 (fp.mul c_currentRoundingMode c___kernel_cos_~z~2_primed (fp.add c_currentRoundingMode c_~C4_kcos~0 (fp.mul c_currentRoundingMode c___kernel_cos_~z~2_primed (fp.add c_currentRoundingMode c_~C5_kcos~0 (fp.mul c_currentRoundingMode c___kernel_cos_~z~2_primed c_~C6_kcos~0)))))))))))) (= c___kernel_cos_~z~2_primed (fp.mul c_currentRoundingMode c___kernel_cos_~x c___kernel_cos_~x))))
(assert (not (and (exists ((v_skolemized_v_prenex_18_3 (_ BitVec 64))) (and (bvsge (bvand (_ bv2147483647 32) ((_ extract 63 32) v_skolemized_v_prenex_18_3)) (_ bv2146435072 32)) (= |c_cos_double_#in~x| (fp ((_ extract 63 63) v_skolemized_v_prenex_18_3) ((_ extract 62 52) v_skolemized_v_prenex_18_3) ((_ extract 51 0) v_skolemized_v_prenex_18_3))))) (= (fp.sub c_currentRoundingMode |c_cos_double_#in~x| |c_cos_double_#in~x|) |c_cos_double_#res|))))
(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 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 |c_cos_double_#in~x| () (_ FloatingPoint 11 53))
(declare-fun c_cos_double_~x () (_ FloatingPoint 11 53))
(declare-fun c_cos_double_~ix~3 () (_ BitVec 32))
(assert (and (exists ((v_skolemized_v_prenex_18_3 (_ BitVec 64))) (and (bvsge (bvand (_ bv2147483647 32) ((_ extract 63 32) v_skolemized_v_prenex_18_3)) (_ bv2146435072 32)) (= |c_cos_double_#in~x| (fp ((_ extract 63 63) v_skolemized_v_prenex_18_3) ((_ extract 62 52) v_skolemized_v_prenex_18_3) ((_ extract 51 0) v_skolemized_v_prenex_18_3))))) (= |c_cos_double_#in~x| c_cos_double_~x) (exists ((v_skolemized_v_prenex_18_3 (_ BitVec 64))) (and (= |c_cos_double_#in~x| (fp ((_ extract 63 63) v_skolemized_v_prenex_18_3) ((_ extract 62 52) v_skolemized_v_prenex_18_3) ((_ extract 51 0) v_skolemized_v_prenex_18_3))) (= c_cos_double_~ix~3 (bvand (_ bv2147483647 32) ((_ extract 63 32) v_skolemized_v_prenex_18_3)))))))
(assert (not (exists ((v_skolemized_v_prenex_18_3 (_ BitVec 64))) (and (= |c_cos_double_#in~x| (fp ((_ extract 63 63) v_skolemized_v_prenex_18_3) ((_ extract 62 52) v_skolemized_v_prenex_18_3) ((_ extract 51 0) v_skolemized_v_prenex_18_3))) (= ((_ extract 63 32) v_skolemized_v_prenex_18_3) c_cos_double_~ix~3)))))
(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 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 |c_cos_double_#in~x| () (_ FloatingPoint 11 53))
(declare-fun c_cos_double_~x () (_ FloatingPoint 11 53))
(declare-fun c_cos_double_~ix~3 () (_ BitVec 32))
(assert (and (exists ((v_skolemized_v_prenex_18_3 (_ BitVec 64))) (and (bvsge (bvand (_ bv2147483647 32) ((_ extract 63 32) v_skolemized_v_prenex_18_3)) (_ bv2146435072 32)) (= |c_cos_double_#in~x| (fp ((_ extract 63 63) v_skolemized_v_prenex_18_3) ((_ extract 62 52) v_skolemized_v_prenex_18_3) ((_ extract 51 0) v_skolemized_v_prenex_18_3))))) (= |c_cos_double_#in~x| c_cos_double_~x) (exists ((v_skolemized_v_prenex_18_3 (_ BitVec 64))) (and (= |c_cos_double_#in~x| (fp ((_ extract 63 63) v_skolemized_v_prenex_18_3) ((_ extract 62 52) v_skolemized_v_prenex_18_3) ((_ extract 51 0) v_skolemized_v_prenex_18_3))) (= c_cos_double_~ix~3 (bvand (_ bv2147483647 32) ((_ extract 63 32) v_skolemized_v_prenex_18_3)))))))
(assert (not (and (exists ((v_skolemized_v_prenex_18_3 (_ BitVec 64))) (and (= |c_cos_double_#in~x| (fp ((_ extract 63 63) v_skolemized_v_prenex_18_3) ((_ extract 62 52) v_skolemized_v_prenex_18_3) ((_ extract 51 0) v_skolemized_v_prenex_18_3))) (= ((_ extract 63 32) v_skolemized_v_prenex_18_3) c_cos_double_~ix~3))) (= |c_cos_double_#in~x| c_cos_double_~x))))
(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 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 c_currentRoundingMode () RoundingMode)
(declare-fun c_~one_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pio2_hi_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pio2_lo_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS0_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS1_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS2_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS3_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS4_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS5_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS1_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS2_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS3_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS4_acos~0 () (_ FloatingPoint 11 53))
(declare-fun |c___ieee754_acos_#in~x| () (_ FloatingPoint 11 53))
(declare-fun |c___ieee754_acos_#res_primed| () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~x () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~z~1_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~p~0_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~q~1_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~r~1_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~hx~0 () (_ BitVec 32))
(declare-fun c___ieee754_acos_~ix~0 () (_ BitVec 32))
(assert (and (= c___ieee754_acos_~r~1_primed (fp.div c_currentRoundingMode c___ieee754_acos_~p~0_primed c___ieee754_acos_~q~1_primed)) (= c___ieee754_acos_~q~1_primed (fp.add c_currentRoundingMode c_~one_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~qS1_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~qS2_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~qS3_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed c_~qS4_acos~0))))))))) (= |c___ieee754_acos_#res_primed| (fp.sub c_currentRoundingMode c_~pio2_hi_acos~0 (fp.sub c_currentRoundingMode c___ieee754_acos_~x (fp.sub c_currentRoundingMode c_~pio2_lo_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~x c___ieee754_acos_~r~1_primed))))) (= c___ieee754_acos_~z~1_primed (fp.mul c_currentRoundingMode c___ieee754_acos_~x c___ieee754_acos_~x)) (= c___ieee754_acos_~p~0_primed (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~pS0_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~pS1_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~pS2_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~pS3_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~pS4_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed c_~pS5_acos~0)))))))))))) (not (bvsle c___ieee754_acos_~ix~0 (_ bv1012924416 32)))))
(assert (and (exists ((|v_skolemized_q#valueAsBitvector_9| (_ BitVec 64))) (and (= (bvand (_ bv2147483647 32) ((_ extract 63 32) |v_skolemized_q#valueAsBitvector_9|)) c___ieee754_acos_~ix~0) (= |c___ieee754_acos_#in~x| (fp ((_ extract 63 63) |v_skolemized_q#valueAsBitvector_9|) ((_ extract 62 52) |v_skolemized_q#valueAsBitvector_9|) ((_ extract 51 0) |v_skolemized_q#valueAsBitvector_9|))))) (exists ((|v_skolemized_q#valueAsBitvector_9| (_ BitVec 64))) (and (= ((_ extract 63 32) |v_skolemized_q#valueAsBitvector_9|) c___ieee754_acos_~hx~0) (= |c___ieee754_acos_#in~x| (fp ((_ extract 63 63) |v_skolemized_q#valueAsBitvector_9|) ((_ extract 62 52) |v_skolemized_q#valueAsBitvector_9|) ((_ extract 51 0) |v_skolemized_q#valueAsBitvector_9|))))) (exists ((|v_skolemized_q#valueAsBitvector_9| (_ BitVec 64))) (and (not (bvsge (bvand (_ bv2147483647 32) ((_ extract 63 32) |v_skolemized_q#valueAsBitvector_9|)) (_ bv1072693248 32))) (= |c___ieee754_acos_#in~x| (fp ((_ extract 63 63) |v_skolemized_q#valueAsBitvector_9|) ((_ extract 62 52) |v_skolemized_q#valueAsBitvector_9|) ((_ extract 51 0) |v_skolemized_q#valueAsBitvector_9|))))) (= |c___ieee754_acos_#in~x| c___ieee754_acos_~x)))
(assert (not false))
(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 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 c_currentRoundingMode () RoundingMode)
(declare-fun c_~one_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pio2_hi_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pio2_lo_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS0_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS1_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS2_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS3_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS4_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS5_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS1_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS2_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS3_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS4_acos~0 () (_ FloatingPoint 11 53))
(declare-fun |c___ieee754_acos_#in~x| () (_ FloatingPoint 11 53))
(declare-fun |c___ieee754_acos_#res_primed| () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~x () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~z~1_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~p~0_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~q~1_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~r~1_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~hx~0 () (_ BitVec 32))
(declare-fun c___ieee754_acos_~ix~0 () (_ BitVec 32))
(assert (and (= c___ieee754_acos_~r~1_primed (fp.div c_currentRoundingMode c___ieee754_acos_~p~0_primed c___ieee754_acos_~q~1_primed)) (= c___ieee754_acos_~q~1_primed (fp.add c_currentRoundingMode c_~one_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~qS1_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~qS2_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~qS3_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed c_~qS4_acos~0))))))))) (= |c___ieee754_acos_#res_primed| (fp.sub c_currentRoundingMode c_~pio2_hi_acos~0 (fp.sub c_currentRoundingMode c___ieee754_acos_~x (fp.sub c_currentRoundingMode c_~pio2_lo_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~x c___ieee754_acos_~r~1_primed))))) (= c___ieee754_acos_~z~1_primed (fp.mul c_currentRoundingMode c___ieee754_acos_~x c___ieee754_acos_~x)) (= c___ieee754_acos_~p~0_primed (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~pS0_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~pS1_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~pS2_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~pS3_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~pS4_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed c_~pS5_acos~0)))))))))))) (not (bvsle c___ieee754_acos_~ix~0 (_ bv1012924416 32)))))
(assert (and (exists ((|v_skolemized_q#valueAsBitvector_13| (_ BitVec 64))) (and (= |c___ieee754_acos_#in~x| (fp ((_ extract 63 63) |v_skolemized_q#valueAsBitvector_13|) ((_ extract 62 52) |v_skolemized_q#valueAsBitvector_13|) ((_ extract 51 0) |v_skolemized_q#valueAsBitvector_13|))) (= ((_ extract 63 32) |v_skolemized_q#valueAsBitvector_13|) c___ieee754_acos_~hx~0))) (= |c___ieee754_acos_#in~x| c___ieee754_acos_~x) (exists ((|v_skolemized_q#valueAsBitvector_13| (_ BitVec 64))) (and (= |c___ieee754_acos_#in~x| (fp ((_ extract 63 63) |v_skolemized_q#valueAsBitvector_13|) ((_ extract 62 52) |v_skolemized_q#valueAsBitvector_13|) ((_ extract 51 0) |v_skolemized_q#valueAsBitvector_13|))) (= (bvand (_ bv2147483647 32) ((_ extract 63 32) |v_skolemized_q#valueAsBitvector_13|)) c___ieee754_acos_~ix~0))) (bvslt c___ieee754_acos_~ix~0 (_ bv1071644672 32))))
(assert (not false))
(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 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 c_currentRoundingMode () RoundingMode)
(declare-fun c_~one_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pio2_hi_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pio2_lo_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS0_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS1_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS2_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS3_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS4_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS5_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS1_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS2_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS3_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS4_acos~0 () (_ FloatingPoint 11 53))
(declare-fun |c___ieee754_acos_#in~x| () (_ FloatingPoint 11 53))
(declare-fun |c___ieee754_acos_#res_primed| () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~x () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~z~1_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~p~0_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~q~1_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~r~1_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~hx~2 () (_ BitVec 32))
(declare-fun c___ieee754_acos_~ix~0 () (_ BitVec 32))
(assert (and (= c___ieee754_acos_~p~0_primed (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~pS0_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~pS1_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~pS2_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~pS3_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~pS4_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed c_~pS5_acos~0)))))))))))) (= |c___ieee754_acos_#res_primed| (fp.sub c_currentRoundingMode c_~pio2_hi_acos~0 (fp.sub c_currentRoundingMode c___ieee754_acos_~x (fp.sub c_currentRoundingMode c_~pio2_lo_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~x c___ieee754_acos_~r~1_primed))))) (= c___ieee754_acos_~z~1_primed (fp.mul c_currentRoundingMode c___ieee754_acos_~x c___ieee754_acos_~x)) (= c___ieee754_acos_~r~1_primed (fp.div c_currentRoundingMode c___ieee754_acos_~p~0_primed c___ieee754_acos_~q~1_primed)) (not (bvsle c___ieee754_acos_~ix~0 (_ bv1012924416 32))) (= c___ieee754_acos_~q~1_primed (fp.add c_currentRoundingMode c_~one_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~qS1_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~qS2_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~qS3_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed c_~qS4_acos~0)))))))))))
(assert (and (exists ((v_skolemized_v_prenex_5_3 (_ BitVec 64))) (and (= |c___ieee754_acos_#in~x| (fp ((_ extract 63 63) v_skolemized_v_prenex_5_3) ((_ extract 62 52) v_skolemized_v_prenex_5_3) ((_ extract 51 0) v_skolemized_v_prenex_5_3))) (not (bvsge (bvand (_ bv2147483647 32) ((_ extract 63 32) v_skolemized_v_prenex_5_3)) (_ bv1072693248 32))))) (exists ((v_skolemized_v_prenex_5_3 (_ BitVec 64))) (and (= |c___ieee754_acos_#in~x| (fp ((_ extract 63 63) v_skolemized_v_prenex_5_3) ((_ extract 62 52) v_skolemized_v_prenex_5_3) ((_ extract 51 0) v_skolemized_v_prenex_5_3))) (= (bvand (_ bv2147483647 32) ((_ extract 63 32) v_skolemized_v_prenex_5_3)) c___ieee754_acos_~ix~0))) (exists ((v_skolemized_v_prenex_5_3 (_ BitVec 64))) (and (= ((_ extract 63 32) v_skolemized_v_prenex_5_3) c___ieee754_acos_~hx~2) (= |c___ieee754_acos_#in~x| (fp ((_ extract 63 63) v_skolemized_v_prenex_5_3) ((_ extract 62 52) v_skolemized_v_prenex_5_3) ((_ extract 51 0) v_skolemized_v_prenex_5_3))))) (= |c___ieee754_acos_#in~x| c___ieee754_acos_~x)))
(assert (not false))
(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 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 c_currentRoundingMode () RoundingMode)
(declare-fun c_~one_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pio2_hi_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pio2_lo_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS0_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS1_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS2_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS3_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS4_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pS5_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS1_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS2_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS3_acos~0 () (_ FloatingPoint 11 53))
(declare-fun c_~qS4_acos~0 () (_ FloatingPoint 11 53))
(declare-fun |c___ieee754_acos_#in~x| () (_ FloatingPoint 11 53))
(declare-fun |c___ieee754_acos_#res_primed| () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~x () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~z~1_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~p~0_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~q~1_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~r~1_primed () (_ FloatingPoint 11 53))
(declare-fun c___ieee754_acos_~hx~2 () (_ BitVec 32))
(declare-fun c___ieee754_acos_~ix~0 () (_ BitVec 32))
(assert (and (= c___ieee754_acos_~p~0_primed (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~pS0_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~pS1_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~pS2_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~pS3_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~pS4_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed c_~pS5_acos~0)))))))))))) (= |c___ieee754_acos_#res_primed| (fp.sub c_currentRoundingMode c_~pio2_hi_acos~0 (fp.sub c_currentRoundingMode c___ieee754_acos_~x (fp.sub c_currentRoundingMode c_~pio2_lo_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~x c___ieee754_acos_~r~1_primed))))) (= c___ieee754_acos_~z~1_primed (fp.mul c_currentRoundingMode c___ieee754_acos_~x c___ieee754_acos_~x)) (= c___ieee754_acos_~r~1_primed (fp.div c_currentRoundingMode c___ieee754_acos_~p~0_primed c___ieee754_acos_~q~1_primed)) (not (bvsle c___ieee754_acos_~ix~0 (_ bv1012924416 32))) (= c___ieee754_acos_~q~1_primed (fp.add c_currentRoundingMode c_~one_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~qS1_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~qS2_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed (fp.add c_currentRoundingMode c_~qS3_acos~0 (fp.mul c_currentRoundingMode c___ieee754_acos_~z~1_primed c_~qS4_acos~0)))))))))))
(assert (and (exists ((v_skolemized_v_prenex_5_7 (_ BitVec 64))) (and (= |c___ieee754_acos_#in~x| (fp ((_ extract 63 63) v_skolemized_v_prenex_5_7) ((_ extract 62 52) v_skolemized_v_prenex_5_7) ((_ extract 51 0) v_skolemized_v_prenex_5_7))) (= ((_ extract 63 32) v_skolemized_v_prenex_5_7) c___ieee754_acos_~hx~2))) (exists ((v_skolemized_v_prenex_5_7 (_ BitVec 64))) (and (= |c___ieee754_acos_#in~x| (fp ((_ extract 63 63) v_skolemized_v_prenex_5_7) ((_ extract 62 52) v_skolemized_v_prenex_5_7) ((_ extract 51 0) v_skolemized_v_prenex_5_7))) (= (bvand (_ bv2147483647 32) ((_ extract 63 32) v_skolemized_v_prenex_5_7)) c___ieee754_acos_~ix~0))) (not (bvsge c___ieee754_acos_~ix~0 (_ bv1072693248 32))) (= |c___ieee754_acos_#in~x| c___ieee754_acos_~x)))
(assert (not false))
(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 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 |c_tan_double_#in~x| () (_ FloatingPoint 11 53))
(declare-fun c_tan_double_~x () (_ FloatingPoint 11 53))
(declare-fun c_tan_double_~ix~2 () (_ BitVec 32))
(assert (and (= |c_tan_double_#in~x| c_tan_double_~x) (exists ((|v_skolemized_q#valueAsBitvector_103| (_ BitVec 64))) (and (= |c_tan_double_#in~x| (fp ((_ extract 63 63) |v_skolemized_q#valueAsBitvector_103|) ((_ extract 62 52) |v_skolemized_q#valueAsBitvector_103|) ((_ extract 51 0) |v_skolemized_q#valueAsBitvector_103|))) (= c_tan_double_~ix~2 (bvand (_ bv2147483647 32) ((_ extract 63 32) |v_skolemized_q#valueAsBitvector_103|))))) (exists ((|v_skolemized_q#valueAsBitvector_103| (_ BitVec 64))) (and (= |c_tan_double_#in~x| (fp ((_ extract 63 63) |v_skolemized_q#valueAsBitvector_103|) ((_ extract 62 52) |v_skolemized_q#valueAsBitvector_103|) ((_ extract 51 0) |v_skolemized_q#valueAsBitvector_103|))) (bvsge (bvand (_ bv2147483647 32) ((_ extract 63 32) |v_skolemized_q#valueAsBitvector_103|)) (_ bv2146435072 32))))))
(assert (not (exists ((|v_skolemized_q#valueAsBitvector_103| (_ BitVec 64))) (and (= |c_tan_double_#in~x| (fp ((_ extract 63 63) |v_skolemized_q#valueAsBitvector_103|) ((_ extract 62 52) |v_skolemized_q#valueAsBitvector_103|) ((_ extract 51 0) |v_skolemized_q#valueAsBitvector_103|))) (= ((_ extract 63 32) |v_skolemized_q#valueAsBitvector_103|) c_tan_double_~ix~2)))))
(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 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 c_currentRoundingMode () RoundingMode)
(declare-fun c_~pio4_ktan~0 () (_ FloatingPoint 11 53))
(declare-fun c_~pio4lo_ktan~0 () (_ FloatingPoint 11 53))
(declare-fun |c_tan_double_#in~x| () (_ FloatingPoint 11 53))
(declare-fun |c___kernel_tan_#in~x| () (_ FloatingPoint 11 53))
(declare-fun c___kernel_tan_~x () (_ FloatingPoint 11 53))
(declare-fun c___kernel_tan_~x_primed () (_ FloatingPoint 11 53))
(declare-fun c___kernel_tan_~y () (_ FloatingPoint 11 53))
(declare-fun c___kernel_tan_~y_primed () (_ FloatingPoint 11 53))
(declare-fun c___kernel_tan_~z~2_primed () (_ FloatingPoint 11 53))
(declare-fun c___kernel_tan_~w~1_primed () (_ FloatingPoint 11 53))
(declare-fun c___kernel_tan_~ix~1 () (_ BitVec 32))
(declare-fun c___kernel_tan_~hx~3 () (_ BitVec 32))
(assert (and (= c___kernel_tan_~w~1_primed (fp.sub c_currentRoundingMode c_~pio4lo_ktan~0 c___kernel_tan_~y)) (= c___kernel_tan_~y_primed (_ +zero 11 53)) (= c___kernel_tan_~x_primed (fp.add c_currentRoundingMode c___kernel_tan_~z~2_primed c___kernel_tan_~w~1_primed)) (= c___kernel_tan_~z~2_primed (fp.sub c_currentRoundingMode c_~pio4_ktan~0 c___kernel_tan_~x))))
(assert (and (exists ((|v_skolemized_q#valueAsBitvector_107| (_ BitVec 64))) (and (= ((_ extract 63 32) |v_skolemized_q#valueAsBitvector_107|) c___kernel_tan_~hx~3) (= |c___kernel_tan_#in~x| (fp ((_ extract 63 63) |v_skolemized_q#valueAsBitvector_107|) ((_ extract 62 52) |v_skolemized_q#valueAsBitvector_107|) ((_ extract 51 0) |v_skolemized_q#valueAsBitvector_107|))))) (exists ((|v_skolemized_q#valueAsBitvector_107| (_ BitVec 64))) (and (= c___kernel_tan_~ix~1 (bvand (_ bv2147483647 32) ((_ extract 63 32) |v_skolemized_q#valueAsBitvector_107|))) (= |c___kernel_tan_#in~x| (fp ((_ extract 63 63) |v_skolemized_q#valueAsBitvector_107|) ((_ extract 62 52) |v_skolemized_q#valueAsBitvector_107|) ((_ extract 51 0) |v_skolemized_q#valueAsBitvector_107|))))) (= |c___kernel_tan_#in~x| c___kernel_tan_~x) (not (bvslt c___kernel_tan_~ix~1 (_ bv1043333120 32)))))
(assert (not (exists ((|v_skolemized_q#valueAsBitvector_107| (_ BitVec 64))) (let ((.cse0 (bvand (_ bv2147483647 32) ((_ extract 63 32) |v_skolemized_q#valueAsBitvector_107|)))) (and (not (bvsge .cse0 (_ bv1072010280 32))) (not (bvslt .cse0 (_ bv1043333120 32))) (= |c_tan_double_#in~x| (fp ((_ extract 63 63) |v_skolemized_q#valueAsBitvector_107|) ((_ extract 62 52) |v_skolemized_q#valueAsBitvector_107|) ((_ extract 51 0) |v_skolemized_q#valueAsBitvector_107|))))))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic BVFP)
(set-info :source "|