From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 14 Jul 2021 03:09:07 +0000 (-0700)
Subject: bv: Add missing BV_EAGER_ATOM proof rule. (#6874)
X-Git-Tag: cvc5-1.0.0~1495
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4890b90d346b8382ce2de697e2e086c3e59de774;p=cvc5.git

bv: Add missing BV_EAGER_ATOM proof rule. (#6874)

Fixes an issue with --proof-eager-checking and --bitblast=eager.
---

diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp
index 4216fa087..414de41ce 100644
--- a/src/theory/bv/bv_solver_simple.cpp
+++ b/src/theory/bv/bv_solver_simple.cpp
@@ -123,6 +123,8 @@ bool BVSolverSimple::preNotifyFact(
     }
     else
     {
+      d_bitblaster->getProofGenerator()->addRewriteStep(
+          fact, n, PfRule::BV_EAGER_ATOM, {}, {fact});
       TrustNode tlem =
           TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator());
       d_im.trustedLemma(tlem, InferenceId::BV_SIMPLE_LEMMA);