Revert "Merging proof branch"

This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.

1 files changed, 8 insertions, 15 deletions

diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp
index 808f5162c..5634a4651 100644
--- a/src/smt/smt_engine_check_proof.cpp
+++ b/src/smt/smt_engine_check_proof.cpp
@@ -63,21 +63,14 @@ void SmtEngine::checkProof() {
 
   Chat() << "checking proof..." << 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;
+  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;
     return;
   }