fix resolution handling in the Alethe post-processor when pivots have…

… Skolems
HanielB · Mar 2, 2024 · c9e8950 · c9e8950
1 parent 5e80e14
commit c9e8950
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
@@ -2431,7 +2431,7 @@ bool AletheProofPostprocessCallback::updatePost(
         polIdx = 2 * (i - 1) + 3 + 1;
         pivIdx = 2 * (i - 1) + 3;
         if (children[i].getKind() == Kind::OR
-            && (args[polIdx] != d_false || args[pivIdx] != children[i]))
+            && (args[polIdx] != d_false || args[pivIdx] != d_anc.convert(children[i])))
         {
           // the arguments will have been converted to witness form already, so
           // we also check whether after conversion the child is still not the
@@ -2480,7 +2480,7 @@ bool AletheProofPostprocessCallback::updatePost(
         // premise is a singleton but the rule concluding it yields a clause.
         else if (children[i].getKind() == Kind::OR)
         {
-          Assert(args[polIdx] == d_false && args[pivIdx] == children[i]);
+          Assert(args[polIdx] == d_false && args[pivIdx] == d_anc.convert(children[i]));
           if (maybeReplacePremiseProof(children[i], cdp))
           {
             hasUpdated = true;