in the alethe proofs, ignore reflexivity for patterns

HanielB · Feb 16, 2024 · c6e809f · c6e809f
1 parent 57a9bac
commit c6e809f
Showing 1 changed file with 10 additions and 8 deletions.
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
@@ -1195,17 +1195,19 @@ bool AletheProofPostprocessCallback::update(Node res,
     {
       if (res[0].isClosure())
       {
-        std::vector<Node> vpis;
-        for (size_t i = 0, size = res[0][0].getNumChildren(); i < size; i++)
+        for (size_t i = 0, size = res[0][0].getNumChildren(); i < size; ++i)
         {
           new_args.push_back(res[0][0][i].eqNode(res[1][0][i]));
         }
-        return addAletheStep(AletheRule::ANCHOR_BIND,
-                             res,
-                             nm->mkNode(Kind::SEXPR, d_cl, res),
-                             children,
-                             new_args,
-                             *cdp);
+        Kind k = res[0].getKind();
+        return addAletheStep(
+            AletheRule::ANCHOR_BIND,
+            res,
+            nm->mkNode(Kind::SEXPR, d_cl, res),
+            // be sure to ignore premise for pattern
+            (k == Kind::FORALL || k == Kind::EXISTS) ? std::vector<Node>{children[0]} : children,
+            new_args,
+            *cdp);
       }
       return addAletheStep(AletheRule::CONG,
                            res,