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 : Sat.AIG BVBit) (pred : BVPred) (assign : BVExpr.Assignment) : ⟦assign.toAIGAssignment, bitblast aig pred⟧ = eval assign pred