From: ajreynol 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)