diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-05 15:01:23 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-05 15:01:23 -0500 |
| commit | b329aff2cdee935377cbe88c289d083fb10c2af8 (patch) | |
| tree | ce4dacecef35c6b6fe43126160d64ae685ee4f26 /test/regress/regress0/nl | |
| parent | c1723f63f0124635a017295502f16c5e7739bec4 (diff) | |
Non-linear supported in ALL logics. Minor fixes for set logic with sygus.
Diffstat (limited to 'test/regress/regress0/nl')
| -rw-r--r-- | test/regress/regress0/nl/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/nl/all-logic.smt2 | 8 |
2 files changed, 10 insertions, 1 deletions
diff --git a/test/regress/regress0/nl/Makefile.am b/test/regress/regress0/nl/Makefile.am index 0da1816b0..53e04a1ef 100644 --- a/test/regress/regress0/nl/Makefile.am +++ b/test/regress/regress0/nl/Makefile.am @@ -48,7 +48,8 @@ TESTS = \ disj-eval.smt2 \ bug698.smt2 \ real-div-ufnra.smt2 \ - div-mod-partial.smt2 + div-mod-partial.smt2 \ + all-logic.smt2 # unsolved : garbage_collect.cvc diff --git a/test/regress/regress0/nl/all-logic.smt2 b/test/regress/regress0/nl/all-logic.smt2 new file mode 100644 index 000000000..700e5d919 --- /dev/null +++ b/test/regress/regress0/nl/all-logic.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-info :status unsat) + +(declare-fun x () Real) + +(assert (< (* x x) 0.0)) + +(check-sat) |