From ee576b76441b9ab423cfaaa744a25487d0cd829a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 12 Apr 2022 16:54:25 -0500 Subject: [PATCH] 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. --- src/proof/lfsc/lfsc_post_processor.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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++) -- 2.30.2