finish translation

HanielB · Feb 1, 2025 · a602f0e · a602f0e
1 parent 650d090
commit a602f0e
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
@@ -535,6 +535,15 @@ bool AletheProofPostprocessCallback::update(Node res,
                            newArgs,
                            *cdp);
     }
+    case ProofRule::SAT_REFUTATION:
+    {
+      return addAletheStep(AletheRule::SAT_REFUTATION,
+                           res,
+                           nm->mkNode(Kind::SEXPR, d_cl, res),
+                           children,
+                           args,
+                           *cdp);
+    }
     // ======== Resolution and N-ary Resolution
     // Because the RESOLUTION rule is merely a special case of CHAIN_RESOLUTION,
     // the same translation can be used for both.