diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-26 11:24:31 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-26 16:24:31 +0000 |
| commit | aa09c24adf024eee0a72ba5b5d9119c71e17d2a0 (patch) | |
| tree | e3c29ac467ab6e63ed04c26b4dfd116f61ff0b74 /test | |
| parent | a05f07c298692ced47c73918876b173bc0fc431d (diff) | |
Disable sygus-inst when incremental (#7485)
Fixes #7385.
Option --sygus-inst relies on the quantifier-free sygus extension of datatypes, which does not support incremental mode. Updating it to support incremental is a long term project.
Until this is complete, --sygus-inst should not be run in incremental mode.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/issue7385-sygus-inst-i.smt2 | 9 |
2 files changed, 10 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 2cf9554e2..8263152dd 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1960,6 +1960,7 @@ set(regress_1_tests regress1/quantifiers/issue6699-nc-shadow.smt2 regress1/quantifiers/issue6775-vts-int.smt2 regress1/quantifiers/issue6845-nl-lemma-tc.smt2 + regress1/quantifiers/issue7385-sygus-inst-i.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lia-witness-div-pp.smt2 diff --git a/test/regress/regress1/quantifiers/issue7385-sygus-inst-i.smt2 b/test/regress/regress1/quantifiers/issue7385-sygus-inst-i.smt2 new file mode 100644 index 000000000..26fc1cf7e --- /dev/null +++ b/test/regress/regress1/quantifiers/issue7385-sygus-inst-i.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: -i +; EXPECT: sat +(set-logic NIRA) +(push) +(assert (exists ((q29 Int) (q30 Bool) (q35 Bool)) (= (= 0 q29) (= q35 q30)))) +(push) +(pop) +(pop) +(check-sat) |