From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 25 Feb 2022 06:27:29 +0000 (-0600)
Subject: Add regression for fixed transcendental regression (#8155)
X-Git-Tag: cvc5-1.0.0~380
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=80d5c9502ce6924c28c3d27d22625bd7c47686c0;p=cvc5.git

Add regression for fixed transcendental regression (#8155)

Fixes #7938.
---

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)