[alethe] Fix AND_INTRO

HanielB · Jan 30, 2025 · 14f54d8 · 14f54d8
1 parent 05bddb3
commit 14f54d8
Showing 1 changed file with 4 additions and 7 deletions.
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
@@ -830,16 +830,13 @@ bool AletheProofPostprocessCallback::update(Node res,
       std::vector<Node> new_children = {vp1};
       new_children.insert(new_children.end(), children.begin(), children.end());
       std::vector<Node> newArgs;
-      if (d_resPivots)
+      for (const Node& child : children)
       {
-        for (const Node& child : children)
-        {
-          newArgs.push_back(child);
-          newArgs.push_back(d_false);
-        }
+        newArgs.push_back(child);
+        newArgs.push_back(d_false);
       }
       return addAletheStep(AletheRule::AND_NEG, vp1, vp1, {}, {}, *cdp)
-             && addAletheStep(AletheRule::RESOLUTION,
+             && addAletheStep(AletheRule::RESOLUTION_OR,
                               res,
                               nm->mkNode(Kind::SEXPR, d_cl, res),
                               new_children,