2

HanielB · Sep 28, 2023 · 1f2c1cf · 1f2c1cf
1 parent d24ebd7
commit 1f2c1cf
Showing 1 changed file with 1 addition and 4 deletions.
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
@@ -1347,10 +1347,7 @@ bool AletheProofPostprocessCallback::update(Node res,
         // variable. So we must take the suffix of variables from that one (note
         // that when i == 1 the suffix is all the variables)
         Node curSkolemizing =
-            i == 1 ? quant
-                   : nm->mkNode(quantKind,
-                                nm->mkNode(Kind::BOUND_VAR_LIST, ithBVars),
-                                quant[1]);
+            i == 1 ? quant : nm->mkNode(quantKind, ithBVars, quant[1]);
         // The choice term is for the (i-1)-th variable defined as the
         // quantifier with the suffix from the i-th variable. This is the same
         // as the term we skolemized in the previous iteration. Note that for