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 a731ff024a0feb4b9eaa243c4da5b657b234cb10..4c218b48c9fc05e4d34e5482a36cb7b698e3dcef 100644 (file)
--- 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;
   }