From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 10 Jul 2017 21:52:10 +0000 (-0500)
Subject: Add nl regression.
X-Git-Tag: cvc5-1.0.0~5728
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c24193a66e81f08cca82cb834fbd21ef630e1bcb;p=cvc5.git

Add nl regression.
---

diff --git a/test/regress/regress0/nl/Makefile.am b/test/regress/regress0/nl/Makefile.am
index e8bff57bd..a9cfae23a 100644
--- a/test/regress/regress0/nl/Makefile.am
+++ b/test/regress/regress0/nl/Makefile.am
@@ -50,6 +50,7 @@ TESTS =	\
   real-div-ufnra.smt2 \
   div-mod-partial.smt2 \
   all-logic.smt2 \
+  sqrt-problem-1.smt2 \
   nta/bad-050217.smt2 \
   nta/cos-bound.smt2 \
   nta/cos-sig-value.smt2 \
diff --git a/test/regress/regress0/nl/sqrt-problem-1.smt2 b/test/regress/regress0/nl/sqrt-problem-1.smt2
new file mode 100644
index 000000000..e74af3a2d
--- /dev/null
+++ b/test/regress/regress0/nl/sqrt-problem-1.smt2
@@ -0,0 +1,41 @@
+; COMMAND-LINE: --nl-ext-tplanes
+; EXPECT: unsat
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun X () Real)
+(declare-fun |sqrt{10}| () Real)
+(declare-fun |sqrt{8}| () Real)
+(assert (let ((.def_48 (<= X (to_real 300))))
+(let ((.def_47 (<= (to_real (- 300)) X)))
+(let ((.def_49 (and .def_47 .def_48)))
+(let ((.def_44 (<= |sqrt{10}| (to_real 300))))
+(let ((.def_43 (<= (to_real (- 300)) |sqrt{10}|)))
+(let ((.def_45 (and .def_43 .def_44)))
+(let ((.def_40 (<= |sqrt{8}| (to_real 300))))
+(let ((.def_39 (<= (to_real (- 300)) |sqrt{8}|)))
+(let ((.def_41 (and .def_39 .def_40)))
+(let ((.def_35 (<= (to_real 0) |sqrt{8}|)))
+(let ((.def_31 (* |sqrt{8}| |sqrt{8}|)))
+(let ((.def_33 (= .def_31 (to_real 3))))
+(let ((.def_29 (<= (to_real 0) |sqrt{10}|)))
+(let ((.def_26 (* |sqrt{10}| |sqrt{10}|)))
+(let ((.def_27 (= X .def_26)))
+(let ((.def_21 (<= X (to_real 2))))
+(let ((.def_19 (<= (to_real 0) X)))
+(let ((.def_22 (and .def_19 .def_21)))
+(let ((.def_23 (not .def_22)))
+(let ((.def_11 (+ |sqrt{10}| |sqrt{8}|)))
+(let ((.def_15 (<= (/ 63 20) .def_11)))
+(let ((.def_16 (not .def_15)))
+(let ((.def_24 (or .def_16 .def_23)))
+(let ((.def_25 (not .def_24)))
+(let ((.def_28 (and .def_25 .def_27)))
+(let ((.def_30 (and .def_28 .def_29)))
+(let ((.def_34 (and .def_30 .def_33)))
+(let ((.def_36 (and .def_34 .def_35)))
+(let ((.def_42 (and .def_36 .def_41)))
+(let ((.def_46 (and .def_42 .def_45)))
+(let ((.def_50 (and .def_46 .def_49)))
+.def_50))))))))))))))))))))))))))))))))
+(check-sat)
+(exit)