diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-09 16:17:46 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-12-09 16:17:46 -0600 |
commit | 2b4e146c3a090e21b64d48ebb4308e5ec58a8c4b (patch) | |
tree | c26a2845b3b34ffbe10d3eb54c175a57a11d9afc /src | |
parent | 33c5eb093a7f032a7d9c9263da595eb53fdd223b (diff) |
Disable sygus inference when combined with incremental and proofs (#3539)
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c034f6f23..80296f400 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1338,6 +1338,19 @@ void SmtEngine::setDefaults() { << endl; options::unconstrainedSimp.set(false); } + if (options::sygusInference()) + { + if (options::sygusInference.wasSetByUser()) + { + throw OptionException( + "sygus inference not supported with unsat cores/proofs/incremental " + "solving"); + } + Notice() << "SmtEngine: turning off sygus inference to support unsat " + "cores/proofs/incremental solving" + << std::endl; + options::sygusInference.set(false); + } } else { |