From ed8c4f9a3dc6339b6418da4d0673e57e08e5060f Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sun, 1 Oct 2017 11:57:52 -0500
Subject: Refactor check function in last call effort of non-linear extension.
 (#1175)

---
 test/regress/regress0/nl/Makefile.am      | 3 ++-
 test/regress/regress0/nl/nta/cos1-tc.smt2 | 8 ++++++++
 2 files changed, 10 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress0/nl/nta/cos1-tc.smt2

(limited to 'test/regress/regress0/nl')

diff --git a/test/regress/regress0/nl/Makefile.am b/test/regress/regress0/nl/Makefile.am
index a9cfae23a..7e4b391cc 100644
--- a/test/regress/regress0/nl/Makefile.am
+++ b/test/regress/regress0/nl/Makefile.am
@@ -65,7 +65,8 @@ TESTS =	\
   nta/tan-rewrite2.smt2 \
   nta/tan-rewrite.smt2 \
   nta/arrowsmith-050317.smt2 \
-  nta/sin-init-tangents.smt2
+  nta/sin-init-tangents.smt2 \
+  nta/cos1-tc.smt2
 
 # unsolved : garbage_collect.cvc
 
diff --git a/test/regress/regress0/nl/nta/cos1-tc.smt2 b/test/regress/regress0/nl/nta/cos1-tc.smt2
new file mode 100644
index 000000000..80d3eec89
--- /dev/null
+++ b/test/regress/regress0/nl/nta/cos1-tc.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: unknown
+(set-logic UFNRA)
+(declare-fun f (Real) Real)
+
+(assert (= (f 0.0) (cos 1)))
+
+(check-sat)
-- 
cgit v1.2.3