diff options
Diffstat (limited to 'src/smt/set_defaults.cpp')
| -rw-r--r-- | src/smt/set_defaults.cpp | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index d663352f7..a7e8e6212 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -291,8 +291,10 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) // sygus inference may require datatypes if (!smte.isInternalSubsolver()) { - if (options::produceAbducts() || options::sygusInference() - || options::sygusRewSynthInput() || options::sygusInst()) + if (options::produceAbducts() + || options::produceInterpols() != options::ProduceInterpols::NONE + || options::sygusInference() || options::sygusRewSynthInput() + || options::sygusInst()) { // since we are trying to recast as sygus, we assume the input is sygus is_sygus = true; @@ -316,6 +318,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) if ((options::checkModels() || options::checkSynthSol() || options::produceAbducts() + || options::produceInterpols() != options::ProduceInterpols::NONE || options::modelCoresMode() != options::ModelCoresMode::NONE || options::blockModelsMode() != options::BlockModelsMode::NONE) && !options::produceAssertions()) |