Add regression for fixed transcendental regression (#8155)

Fixes #7938.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 71219634bb7b92b031489e0840ae69ca93055115..fd3e7dd3ae5e019991c75ffd1881aa74518aa9be 100644 (file)
--- 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 (file)
index 0000000..eff66c7
--- /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)