diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-20 17:18:02 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-20 17:18:02 -0500 |
| commit | b967cc5c8d84023c1b821c59b7bca736ffda6bed (patch) | |
| tree | b1900e3817888a0ff321d70da4a31796db82b0ee /test/regress/regress1 | |
| parent | 16c2fe5ec2ebb29da131aa590a4a0b79b1e94dc9 (diff) | |
Fixes for sygus inference on quantifier free problems (#3202)
Diffstat (limited to 'test/regress/regress1')
| -rw-r--r-- | test/regress/regress1/sygus/issue3199.smt2 | 7 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/issue3200.smt2 | 7 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/issue3201.smt2 | 8 |
3 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/issue3199.smt2 b/test/regress/regress1/sygus/issue3199.smt2 new file mode 100644 index 000000000..b4681e35e --- /dev/null +++ b/test/regress/regress1/sygus/issue3199.smt2 @@ -0,0 +1,7 @@ +; EXPECT: sat +; COMMAND-LINE: --sygus-inference +(set-logic QF_LRA) +(declare-fun v () Real) +(assert (= v 0)) +(check-sat) +(exit) diff --git a/test/regress/regress1/sygus/issue3200.smt2 b/test/regress/regress1/sygus/issue3200.smt2 new file mode 100644 index 000000000..8eb144c61 --- /dev/null +++ b/test/regress/regress1/sygus/issue3200.smt2 @@ -0,0 +1,7 @@ +; EXPECT: sat +; COMMAND-LINE: --sygus-inference +(set-logic ALL) +(declare-fun v () Real) +(assert (= (* v v) 0)) +(check-sat) +(exit) diff --git a/test/regress/regress1/sygus/issue3201.smt2 b/test/regress/regress1/sygus/issue3201.smt2 new file mode 100644 index 000000000..99a555010 --- /dev/null +++ b/test/regress/regress1/sygus/issue3201.smt2 @@ -0,0 +1,8 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-inference +(set-logic ALL) +(declare-fun v () Bool) +(assert false) +(assert v) +(check-sat) +(exit) |