From 1f2c1cf362ea4adee56ae150e9e3002dfc137a96 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Thu, 28 Sep 2023 12:51:16 -0300 Subject: [PATCH] 2 --- src/proof/alethe/alethe_post_processor.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 21c618d8a48..87e7743559c 100644 --- 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