This module contains the verification of the bitblaster for predicates over BitVec expressions (BVPred) from Impl.Pred.

@[simp]

theorem Std.Tactic.BVDecide.BVPred.denote_bitblast (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (pred : Std.Tactic.BVDecide.BVPred) (assign : Std.Tactic.BVDecide.BVExpr.Assignment) : ⟦assign.toAIGAssignment, Std.Tactic.BVDecide.BVPred.bitblast aig pred⟧ = Std.Tactic.BVDecide.BVPred.eval assign pred