diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-03 20:29:26 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-04-03 18:29:26 -0700 |
| commit | eaebc10c50ca44644edd430ed3f555092a0fb27a (patch) | |
| tree | e1944b5c0a2e9fbb38beb2f308009b563ab4a2bd /test | |
| parent | fee2021bb7419630853cbd0b20afa1af5e2eb1e9 (diff) | |
Option to turn arbitrary input into sygus (#1704)
Preprocessing pass that turns an arbitrary (e.g. smt2) input into a sygus conjecture, which is helpful for Horn clause solving.
This includes improvements to the robustness of the sygus solver.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/sygus-infer-nested.smt2 | 5 |
2 files changed, 6 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index c3d02bbd6..4fb9065c6 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1266,6 +1266,7 @@ REG1_TESTS = \ regress1/quantifiers/smtlibe99bbe.smt2 \ regress1/quantifiers/smtlibf957ea.smt2 \ regress1/quantifiers/stream-x2014-09-18-unsat.smt2 \ + regress1/quantifiers/sygus-infer-nested.smt2 \ regress1/quantifiers/symmetric_unsat_7.smt2 \ regress1/quantifiers/z3.620661-no-fv-trigger.smt2 \ regress1/rels/addr_book_1.cvc \ diff --git a/test/regress/regress1/quantifiers/sygus-infer-nested.smt2 b/test/regress/regress1/quantifiers/sygus-infer-nested.smt2 new file mode 100644 index 000000000..a1e449fa3 --- /dev/null +++ b/test/regress/regress1/quantifiers/sygus-infer-nested.smt2 @@ -0,0 +1,5 @@ +; COMMAND-LINE: --sygus-inference --no-check-models +(set-logic LIA) +(set-info :status sat) +(assert (forall ((x Int) (y Int)) (or (<= x (+ y 1)) (exists ((z Int)) (and (> z y) (< z x)))))) +(check-sat) |