diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-03-14 16:32:25 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-14 16:32:25 -0500 |
| commit | fef57367d28a62251cac47010cc6e80cd416832e (patch) | |
| tree | ab4617644ca96b4d73f0e60d956314b8b19fbb2d /test/regress/regress0/nl | |
| parent | d4046f5e2e32d07c34b65fbcdfffae6a24d8c399 (diff) | |
Use zero slope tangent planes for transcendental functions (#2803)
Diffstat (limited to 'test/regress/regress0/nl')
| -rw-r--r-- | test/regress/regress0/nl/nta/exp-neg2-unsat-unsound.smt2 | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test/regress/regress0/nl/nta/exp-neg2-unsat-unsound.smt2 b/test/regress/regress0/nl/nta/exp-neg2-unsat-unsound.smt2 new file mode 100644 index 000000000..69c36179a --- /dev/null +++ b/test/regress/regress0/nl/nta/exp-neg2-unsat-unsound.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models +; EXPECT: sat +(set-logic QF_NRAT) +(declare-fun x () Real) +(assert (or +(and (<= (exp x) 0.01) (= x (- 2.0))) +(and (> (exp x) 0.2) (= x (- 1.0))) +) +) +(check-sat) |