diff options
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/set_defaults.cpp | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index e3b1163fc..23ae65044 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -266,6 +266,11 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) << std::endl; } } + // !!!!!!!!!!!!!!!! temporary, to support CI check for old proof system + if (options::proof()) + { + options::proofNew.set(false); + } // sygus inference may require datatypes if (!smte.isInternalSubsolver()) @@ -877,6 +882,16 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) } if (options::ufHo()) { + // if higher-order, disable proof production + if (options::proofNew()) + { + if (options::proofNew.wasSetByUser()) + { + Warning() << "SmtEngine: turning off proof production (not yet " + "supported with --uf-ho)\n"; + } + options::proofNew.set(false); + } // if higher-order, then current variants of model-based instantiation // cannot be used if (options::mbqiMode() != options::MbqiMode::NONE) @@ -1108,6 +1123,16 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) { options::cegqiPreRegInst.set(true); } + // not compatible with proofs + if (options::proofNew()) + { + if (options::proofNew.wasSetByUser()) + { + Notice() << "SmtEngine: setting proof-new to false to support SyGuS" + << std::endl; + } + options::proofNew.set(false); + } } // counterexample-guided instantiation for non-sygus // enable if any possible quantifiers with arithmetic, datatypes or bitvectors @@ -1464,6 +1489,11 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) "division. " "Try --bv-div-zero-const to interpret division by zero as a constant."); } + // !!!!!!!!!!!!!!!! temporary, until proof-new is functional + if (options::proofNew()) + { + throw OptionException("--proof-new is not yet supported."); + } } } // namespace smt |