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 4216fa0875d63acb500463be0a31efa718993589..414de41ceaeafefe000603c419902ace6bdaeb3e 100644 (file)
--- 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);