diff options
Diffstat (limited to 'test/regress/regress1/nl/NAVIGATION2.smt2')
-rw-r--r-- | test/regress/regress1/nl/NAVIGATION2.smt2 | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/test/regress/regress1/nl/NAVIGATION2.smt2 b/test/regress/regress1/nl/NAVIGATION2.smt2 new file mode 100644 index 000000000..445b8a21e --- /dev/null +++ b/test/regress/regress1/nl/NAVIGATION2.smt2 @@ -0,0 +1,23 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :source |printed by MathSAT|) +(declare-fun X () Real) + +(assert (let ((.def_44 (* (- (/ 11 10)) X))) +(let ((.def_45 (exp .def_44))) +(let ((.def_50 (* 250 .def_45))) +(let ((.def_40 (* (- (/ 13 10)) X))) +(let ((.def_41 (exp .def_40))) +(let ((.def_52 (* 173 .def_41))) +(let ((.def_53 (+ .def_52 .def_50))) +(let ((.def_54 (* 250 X))) +(let ((.def_55 (+ .def_54 .def_53))) +(let ((.def_56 (<= .def_55 (/ 595 2)))) +(let ((.def_57 (not .def_56))) +(let ((.def_31 (<= 0 X))) +(let ((.def_32 (not .def_31))) +(let ((.def_58 (or .def_32 .def_57))) +(let ((.def_59 (not .def_58))) +.def_59)))))))))))))))) +(check-sat) |