From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 10 Apr 2014 22:34:44 +0000 (-0400)
Subject: Fix the build; --check-proof works for UF but not for the new UFC logic.
X-Git-Tag: cvc5-1.0.0~6970
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9042fc86692b6dc67ed5ba6bd721752d9a5c5389;p=cvc5.git

Fix the build; --check-proof works for UF but not for the new UFC logic.
---

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;
   }