[proofs] [alethe] Alethe format requires at least THEORY_REWRITE gran…

…ularity
HanielB · Feb 16, 2024 · 17e9da1 · 17e9da1
1 parent c38a5db
commit 17e9da1
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
@@ -184,6 +184,15 @@ void SetDefaults::setDefaultsPre(Options& opts)
                      options::UnsatCoresMode::SAT_PROOF,
                      "enabling proofs");
     }
+    if (opts.proof.proofFormatMode == options::ProofFormatMode::ALETHE
+        && opts.proof.proofGranularityMode
+               < options::ProofGranularityMode::THEORY_REWRITE)
+    {
+      SET_AND_NOTIFY(Proof,
+                     proofGranularityMode,
+                     options::ProofGranularityMode::THEORY_REWRITE,
+                     "Alethe requires granularity at least theory-rewrite");
+    }
   }
   if (!opts.smt.produceProofs)
   {