diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-20 12:53:12 -0600 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-20 10:53:12 -0800 |
| commit | 05a2414a2742ee0c7e5af40ac9c725cb49d1f196 (patch) | |
| tree | 8392f1b56aedc1a9ea107790cf7741af64b6607f /test/regress/regress0/nl | |
| parent | 4ef569cfd91bccabb6e704dcc4ecd55a9fa0a8ea (diff) | |
Minor fixes and additions for transcendental functions (#1612)
Also adds parsing support for PI in smt2 with syntax "real.pi".
Diffstat (limited to 'test/regress/regress0/nl')
| -rw-r--r-- | test/regress/regress0/nl/Makefile.am | 4 | ||||
| -rw-r--r-- | test/regress/regress0/nl/nta/real-pi.smt2 | 7 | ||||
| -rw-r--r-- | test/regress/regress0/nl/nta/sqrt-simple.smt2 | 6 |
3 files changed, 16 insertions, 1 deletions
diff --git a/test/regress/regress0/nl/Makefile.am b/test/regress/regress0/nl/Makefile.am index c10b65931..0347dbd8b 100644 --- a/test/regress/regress0/nl/Makefile.am +++ b/test/regress/regress0/nl/Makefile.am @@ -35,7 +35,9 @@ TESTS = \ nta/tan-rewrite.smt2 \ nta/exp1-ub.smt2 \ nta/exp-n0.5-ub.smt2 \ - nta/exp-n0.5-lb.smt2 + nta/exp-n0.5-lb.smt2 \ + nta/real-pi.smt2 \ + nta/sqrt-simple.smt2 # unsolved : garbage_collect.cvc diff --git a/test/regress/regress0/nl/nta/real-pi.smt2 b/test/regress/regress0/nl/nta/real-pi.smt2 new file mode 100644 index 000000000..a303f48b1 --- /dev/null +++ b/test/regress/regress0/nl/nta/real-pi.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --nl-ext --no-check-models +; EXPECT: sat +(set-logic QF_NRA) +(set-info :status sat) +(assert (<= 3.0 real.pi)) +(assert (<= real.pi 4.0)) +(check-sat) diff --git a/test/regress/regress0/nl/nta/sqrt-simple.smt2 b/test/regress/regress0/nl/nta/sqrt-simple.smt2 new file mode 100644 index 000000000..ade068152 --- /dev/null +++ b/test/regress/regress0/nl/nta/sqrt-simple.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x () Real) +(assert (> x 0.0)) +(assert (not (= (* (sqrt x) (sqrt x)) x))) +(check-sat) |