diff options
Diffstat (limited to 'src/smt/smt_engine_check_proof.cpp')
-rw-r--r-- | src/smt/smt_engine_check_proof.cpp | 23 |
1 files changed, 8 insertions, 15 deletions
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp index 808f5162c..5634a4651 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -63,21 +63,14 @@ void SmtEngine::checkProof() { Chat() << "checking proof..." << endl; - std::string logicString = d_logic.getLogicString(); - - if (!( - // Pure logics - logicString == "QF_UF" || - logicString == "QF_AX" || - logicString == "QF_BV" || - // Non-pure logics - logicString == "QF_AUF" || - logicString == "QF_UFBV" || - logicString == "QF_ABV" || - logicString == "QF_AUFBV" - )) { - // This logic is not yet supported - Notice() << "Notice: no proof-checking for " << logicString << " proofs yet" << endl; + if ( !(d_logic.isPure(theory::THEORY_BOOL) || + d_logic.isPure(theory::THEORY_BV) || + d_logic.isPure(theory::THEORY_ARRAY) || + (d_logic.isPure(theory::THEORY_UF) && + ! d_logic.hasCardinalityConstraints())) || + d_logic.isQuantified()) { + // no checking for these yet + Notice() << "Notice: no proof-checking for non-UF/Bool/BV proofs yet" << endl; return; } |