Fix type issue for LFSC null terminator (#8607)

This fixes an assertion failure when producing LFSC proofs in debug mode.

The issue currently does not impact the correctness of the code, although this will be important if subtypes are eliminated.

diff --git a/src/proof/lfsc/lfsc_post_processor.cpp b/src/proof/lfsc/lfsc_post_processor.cpp
index fd5f37b6f3fe2cf1bacf40c042344fe64a14dec9..34190ab7ed0a6a83b7d30a867df889c6f21acb88 100644 (file)
--- a/src/proof/lfsc/lfsc_post_processor.cpp
+++ b/src/proof/lfsc/lfsc_post_processor.cpp
@@ -335,7 +335,7 @@ bool LfscProofPostprocessCallback::update(Node res,
     case PfRule::ARITH_SUM_UB:
     {
       // proof of null terminator base 0 = 0
-      Node zero = d_tproc.getNullTerminator(ADD);
+      Node zero = d_tproc.getNullTerminator(ADD, res[0].getType());
       Node cur = zero.eqNode(zero);
       cdp->addStep(cur, PfRule::REFL, {}, {zero});
       for (size_t i = 0, size = children.size(); i < size; i++)