1 files changed, 4 insertions, 8 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f451d12bd..918539f4f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2238,6 +2238,10 @@ void SmtEngine::setDefaults() {
 
   if (options::proof())
   {
+    if (d_logic > LogicInfo("QF_AUFBVLRA")) {
+        throw OptionException(
+            "Proofs are only supported for sub-logics of QF_AUFBVLIA."); 
+    }
     if (options::bitvectorAlgebraicSolver())
     {
       if (options::bitvectorAlgebraicSolver.wasSetByUser())
@@ -4494,14 +4498,6 @@ void SmtEngine::checkProof()
 
   std::string logicString = d_logic.getLogicString();
 
-  if (!(d_logic <= LogicInfo("QF_AUFBVLRA")))
-  {
-    // This logic is not yet supported
-    Notice() << "Notice: no proof-checking for " << logicString << " proofs yet"
-             << endl;
-    return;
-  }
-
   std::stringstream pfStream;
 
   pfStream << proof::plf_signatures << endl;