diff options
Diffstat (limited to 'src/smt/set_defaults.cpp')
-rw-r--r-- | src/smt/set_defaults.cpp | 28 |
1 files changed, 4 insertions, 24 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 93196fde4..98fbfe1b3 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -73,7 +73,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } if (options::checkUnsatCoresNew()) { - options::proofNew.set(true); + options::proof.set(true); } if (options::bitvectorAigSimplifications.wasSetByUser()) { @@ -872,16 +872,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } 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) @@ -1095,16 +1085,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { options::nlExtTangentPlanes.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 @@ -1394,10 +1374,10 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) "division. " "Try --bv-div-zero-const to interpret division by zero as a constant."); } - // !!!!!!!!!!!!!!!! temporary, until proof-new is functional - if (options::proofNew()) + // !!!!!!!!!!!!!!!! temporary, until proofs are functional + if (options::proof()) { - throw OptionException("--proof-new is not yet supported."); + throw OptionException("--proof is not yet supported."); } if (logic == LogicInfo("QF_UFNRA")) |