diff options
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine_check_proof.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp index a731ff024..4c218b48c 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -57,10 +57,11 @@ void SmtEngine::checkProof() { Chat() << "checking proof..." << endl; - if(!d_logic.isPure(theory::THEORY_BOOL) && - !d_logic.isPure(theory::THEORY_UF)) { + if( ! ( d_logic.isPure(theory::THEORY_BOOL) || + ( d_logic.isPure(theory::THEORY_UF) && + ! d_logic.hasCardinalityConstraints() ) ) ) { // no checking for these yet - Notice() << "Notice: no proof-checking for non-UF proofs yet" << endl; + Notice() << "Notice: no proof-checking for non-UF/Bool proofs yet" << endl; return; } |