diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2019-10-03 15:23:58 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-03 15:23:58 -0700 |
commit | 167947ab81094de28251bb885c8cf84e7168c43b (patch) | |
tree | 385bc47f48611c535309721c8b933f3117a2e9ed /src/smt | |
parent | 76ddd08e3805ca262d732ce78db165272ef0852e (diff) |
Disable proofs for unsupported logics (#3327)
This commit makes CVC4 complain if the user asked for proofs for an unsupported logic (in this contest, ALL is considered unsupported).
Changes in the regression script are introduced as well, in order to only request proofs for regressions in supported logics.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f451d12bd..918539f4f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2238,6 +2238,10 @@ void SmtEngine::setDefaults() { if (options::proof()) { + if (d_logic > LogicInfo("QF_AUFBVLRA")) { + throw OptionException( + "Proofs are only supported for sub-logics of QF_AUFBVLIA."); + } if (options::bitvectorAlgebraicSolver()) { if (options::bitvectorAlgebraicSolver.wasSetByUser()) @@ -4494,14 +4498,6 @@ void SmtEngine::checkProof() std::string logicString = d_logic.getLogicString(); - if (!(d_logic <= LogicInfo("QF_AUFBVLRA"))) - { - // This logic is not yet supported - Notice() << "Notice: no proof-checking for " << logicString << " proofs yet" - << endl; - return; - } - std::stringstream pfStream; pfStream << proof::plf_signatures << endl; |