From 167947ab81094de28251bb885c8cf84e7168c43b Mon Sep 17 00:00:00 2001 From: yoni206 Date: Thu, 3 Oct 2019 15:23:58 -0700 Subject: 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. --- src/smt/smt_engine.cpp | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) (limited to 'src/smt') 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; -- cgit v1.2.3