From 4890b90d346b8382ce2de697e2e086c3e59de774 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Tue, 13 Jul 2021 20:09:07 -0700 Subject: [PATCH] bv: Add missing BV_EAGER_ATOM proof rule. (#6874) Fixes an issue with --proof-eager-checking and --bitblast=eager. --- src/theory/bv/bv_solver_simple.cpp | 2 ++ 1 file changed, 2 insertions(+) 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); -- 2.30.2