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 | |
| parent | c1723f63f0124635a017295502f16c5e7739bec4 (diff) | |
Non-linear supported in ALL logics. Minor fixes for set logic with sygus.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/expect/scrub.09.p | 2 | ||||
| -rw-r--r-- | test/regress/regress0/nl/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/nl/all-logic.smt2 | 8 |
3 files changed, 11 insertions, 2 deletions
diff --git a/test/regress/regress0/expect/scrub.09.p b/test/regress/regress0/expect/scrub.09.p index ee765a91a..0297b1155 100644 --- a/test/regress/regress0/expect/scrub.09.p +++ b/test/regress/regress0/expect/scrub.09.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --cegqi-si=all --no-dump-synth +% COMMAND-LINE: % SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' % EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. % EXPECT: The fact in question: TERM 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) |