From 9042fc86692b6dc67ed5ba6bd721752d9a5c5389 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 10 Apr 2014 18:34:44 -0400 Subject: [PATCH] Fix the build; --check-proof works for UF but not for the new UFC logic. --- src/smt/smt_engine_check_proof.cpp | 7 ++++--- 1 file 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; } -- 2.30.2