diff options
| -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 { |