projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a05f07c) | patch
Disable sygus-inst when incremental (#7485)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 26 Oct 2021 16:24:31 +0000 (11:24 -0500)
committerGitHub <noreply@github.com>
Tue, 26 Oct 2021 16:24:31 +0000 (16:24 +0000)
commitaa09c24adf024eee0a72ba5b5d9119c71e17d2a0
treee3c29ac467ab6e63ed04c26b4dfd116f61ff0b74tree
parenta05f07c298692ced47c73918876b173bc0fc431dcommit | 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.
src/smt/set_defaults.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/quantifiers/issue7385-sygus-inst-i.smt2 [new file with mode: 0644] blob