diff options
author | Guy <katz911@gmail.com> | 2016-06-01 17:41:17 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-01 17:41:17 -0700 |
commit | de0dd1dc966b05467f1a5443ff33094262f5076a (patch) | |
tree | 46a8539229fc31226b416755e6a88c18476ecffc /src/smt/smt_engine_check_proof.cpp | |
parent | 89ba584531115b7f6d47088d7614368ea05ab9d8 (diff) |
Revert "Merging proof branch"
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
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; } |