∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w curr : ℕ} {aig : Std.Sat.AIG α} {cin : aig.Ref}
  {lhs rhs : aig.RefVec w},
  aig.decls.size ≤ (Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go aig lhs rhs curr cin).aig.decls.size