From 80d5c9502ce6924c28c3d27d22625bd7c47686c0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 25 Feb 2022 00:27:29 -0600 Subject: [PATCH] Add regression for fixed transcendental regression (#8155) Fixes #7938. --- test/regress/CMakeLists.txt | 1 + test/regress/regress0/nl/nta/issue7938-tf-model.smt2 | 9 +++++++++ 2 files changed, 10 insertions(+) create mode 100644 test/regress/regress0/nl/nta/issue7938-tf-model.smt2 diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 71219634b..fd3e7dd3a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -789,6 +789,7 @@ set(regress_0_tests regress0/nl/nta/exp-n0.5-ub.smt2 regress0/nl/nta/exp-neg2-unsat-unsound.smt2 regress0/nl/nta/exp1-ub.smt2 + regress0/nl/nta/issue7938-tf-model.smt2 regress0/nl/nta/issue8147-unc-model.smt2 regress0/nl/nta/real-pi.smt2 regress0/nl/nta/sin-sym.smt2 diff --git a/test/regress/regress0/nl/nta/issue7938-tf-model.smt2 b/test/regress/regress0/nl/nta/issue7938-tf-model.smt2 new file mode 100644 index 000000000..eff66c77d --- /dev/null +++ b/test/regress/regress0/nl/nta/issue7938-tf-model.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL) +(set-info :status sat) +(declare-const x3 Bool) +(declare-const x Real) +(declare-const x5 Real) +(declare-fun s () Real) +(assert (exists ((S Real)) (= s (sin 1.0)))) +(assert (xor (and (= 0.0 (/ x5 0.0)) (= x (- 0.0 1 (/ 0.0 x))) (= x 1)) x3)) +(check-sat) -- 2.30.2