This module contains the incremental BitVec theory solver for the CEGAR loop. It implements incremental bitblasting, CNF generation and SAT solving. Once it determines UNSAT it will construct a proof for the goal and close it by contradiction.

def Lean.Meta.Tactic.BVDecide.Cegar.checkBitVec : CegarM (Except (Array (Expr × Bool × Std.Tactic.BVDecide.BVExpr.PackedBitVec)) LratCert)

Equations

• One or more equations did not get rendered due to their size.