diff options
author | Guy <katz911@gmail.com> | 2016-06-01 17:33:41 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-01 17:33:41 -0700 |
commit | 89ba584531115b7f6d47088d7614368ea05ab9d8 (patch) | |
tree | aae1792c05c0a67c521160226deb451ca861822c /src/smt/smt_engine_check_proof.cpp | |
parent | 324ca0376c960c75f621f0102eeaa1186589dda7 (diff) |
Merging proof branch
Diffstat (limited to 'src/smt/smt_engine_check_proof.cpp')
-rw-r--r-- | src/smt/smt_engine_check_proof.cpp | 23 |
1 files changed, 15 insertions, 8 deletions
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp index 5634a4651..808f5162c 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -63,14 +63,21 @@ void SmtEngine::checkProof() { Chat() << "checking proof..." << 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; + 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; return; } |