From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 12 Apr 2022 21:54:25 +0000 (-0500)
Subject: Fix type issue for LFSC null terminator (#8607)
X-Git-Tag: cvc5-1.0.1~269
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ee576b76441b9ab423cfaaa744a25487d0cd829a;p=cvc5.git

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 fd5f37b6f..34190ab7e 100644
--- 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++)