diff --git a/src/Std/Sat/AIG/If.lean b/src/Std/Sat/AIG/If.lean
index 0e1ec1810c..649a7dde04 100644
--- a/src/Std/Sat/AIG/If.lean
+++ b/src/Std/Sat/AIG/If.lean
@@ -116,7 +116,7 @@ structure IfInput (aig : AIG α) (w : Nat) where
 
 def ite (aig : AIG α) (input : IfInput aig w) : RefVecEntry α w :=
   let ⟨discr, lhs, rhs⟩ := input
-  go aig 0 (by omega) discr lhs rhs .empty
+  go aig 0 (by omega) discr lhs rhs (.emptyWithCapacity w)
 where
   go {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : Ref aig)
       (lhs rhs : RefVec aig w) (s : RefVec aig curr) : RefVecEntry α w :=
diff --git a/src/Std/Sat/AIG/RefVec.lean b/src/Std/Sat/AIG/RefVec.lean
index fe7d2146b2..ca3b2b907a 100644
--- a/src/Std/Sat/AIG/RefVec.lean
+++ b/src/Std/Sat/AIG/RefVec.lean
@@ -21,6 +21,15 @@ def empty : RefVec aig 0 where
   hlen := by simp
   hrefs := by intros; contradiction
 
+def emptyWithCapacity (c : Nat) : RefVec aig 0 where
+  refs := Array.emptyWithCapacity c
+  hlen := by simp
+  hrefs := by intros; contradiction
+
+@[simp]
+theorem emptyWithCapacity_eq : emptyWithCapacity (aig := aig) c = empty := by
+  rfl
+
 @[inline]
 def cast' {aig1 aig2 : AIG α} (s : RefVec aig1 len)
     (h :
diff --git a/src/Std/Sat/AIG/RefVecOperator/Map.lean b/src/Std/Sat/AIG/RefVecOperator/Map.lean
index cf1b5c85a0..0f60aa90ad 100644
--- a/src/Std/Sat/AIG/RefVecOperator/Map.lean
+++ b/src/Std/Sat/AIG/RefVecOperator/Map.lean
@@ -52,7 +52,7 @@ attribute [instance] MapTarget.chainable
 
 @[specialize]
 def map (aig : AIG α) (target : MapTarget aig len) : RefVecEntry α len :=
-  go aig 0 (by omega) .empty target.vec target.func
+  go aig 0 (by omega) (.emptyWithCapacity len) target.vec target.func
 where
   @[specialize]
   go {len : Nat} (aig : AIG α) (idx : Nat) (hidx : idx ≤ len) (s : RefVec aig idx)
diff --git a/src/Std/Sat/AIG/RefVecOperator/Zip.lean b/src/Std/Sat/AIG/RefVecOperator/Zip.lean
index 58bdd28212..a8dd69ae91 100644
--- a/src/Std/Sat/AIG/RefVecOperator/Zip.lean
+++ b/src/Std/Sat/AIG/RefVecOperator/Zip.lean
@@ -81,7 +81,7 @@ attribute [instance] ZipTarget.chainable
 
 @[specialize]
 def zip (aig : AIG α) (target : ZipTarget aig len) : RefVecEntry α len :=
-  go aig 0 .empty (by omega) target.input.lhs target.input.rhs target.func
+  go aig 0 (.emptyWithCapacity len) (by omega) target.input.lhs target.input.rhs target.func
 where
   @[specialize]
   go (aig : AIG α) (idx : Nat) (s : RefVec aig idx) (hidx : idx ≤ len)
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.lean
index 99b6f02beb..6fdc9af129 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.lean
@@ -22,7 +22,7 @@ namespace bitblast
 variable [Hashable α] [DecidableEq α]
 
 def blastConst (aig : AIG α) (val : BitVec w) : AIG.RefVecEntry α w :=
-  go aig val 0 .empty (by omega)
+  go aig val 0 (.emptyWithCapacity w) (by omega)
 where
   go (aig : AIG α) (val : BitVec w) (curr : Nat) (s : AIG.RefVec aig curr) (hcurr : curr ≤ w) :
       AIG.RefVecEntry α w :=
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
index 982afc42e4..429c30a85c 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
@@ -166,7 +166,7 @@ def blastAdd (aig : AIG α) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry 
   let cin := res.ref
   let input := input.cast <| AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
   let ⟨lhs, rhs⟩ := input
-  go aig lhs rhs 0 (by omega) cin .empty
+  go aig lhs rhs 0 (by omega) cin (.emptyWithCapacity w)
 where
   go (aig : AIG α) (lhs rhs : AIG.RefVec aig w) (curr : Nat) (hcurr : curr ≤ w) (cin : AIG.Ref aig)
       (s : AIG.RefVec aig curr) :
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Extract.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Extract.lean
index 7420e0fa08..781c0c9320 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Extract.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Extract.lean
@@ -32,7 +32,7 @@ def blastExtract (aig : AIG α) (target : ExtractTarget aig newWidth) :
   let aig := res.aig
   let falseRef := res.ref
   let input := input.cast <| AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
-  ⟨aig, go input start falseRef 0 (by omega) .empty⟩
+  ⟨aig, go input start falseRef 0 (by omega) (.emptyWithCapacity newWidth)⟩
 where
   go {aig : AIG α} {w : Nat} (input : AIG.RefVec aig w) (start : Nat) (falseRef : AIG.Ref aig)
       (curr : Nat) (hcurr : curr ≤ newWidth) (s : AIG.RefVec aig curr) :
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Replicate.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Replicate.lean
index 00d94be04a..d6bd4ac839 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Replicate.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Replicate.lean
@@ -29,7 +29,7 @@ structure ReplicateTarget (aig : AIG α) (combined : Nat) where
 def blastReplicate (aig : AIG α) (target : ReplicateTarget aig newWidth) :
     AIG.RefVecEntry α newWidth :=
   let ⟨n, inner, h⟩ := target
-  let ref := go n inner 0 (by omega) .empty
+  let ref := go n inner 0 (by omega) (.emptyWithCapacity newWidth)
   ⟨aig, h ▸ ref⟩
 where
   go {aig : AIG α} {w : Nat} (n : Nat) (input : AIG.RefVec aig w) (curr : Nat) (hcurr : curr ≤ n)
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateLeft.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateLeft.lean
index bf3995db4f..a675757a7c 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateLeft.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateLeft.lean
@@ -25,7 +25,7 @@ variable [Hashable α] [DecidableEq α]
 def blastRotateLeft (aig : AIG α) (target : AIG.ShiftTarget aig w) :
     AIG.RefVecEntry α w :=
   let ⟨input, distance⟩ := target
-  ⟨aig, go input distance 0 (by omega) .empty⟩
+  ⟨aig, go input distance 0 (by omega) (.emptyWithCapacity w)⟩
 where
   go {aig : AIG α} (input : AIG.RefVec aig w) (distance : Nat) (curr : Nat) (hcurr : curr ≤ w)
       (s : AIG.RefVec aig curr) :
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateRight.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateRight.lean
index 76798d21c1..30b30a36f3 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateRight.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateRight.lean
@@ -25,7 +25,7 @@ variable [Hashable α] [DecidableEq α]
 def blastRotateRight (aig : AIG α) (target : AIG.ShiftTarget aig w) :
     AIG.RefVecEntry α w :=
   let ⟨input, distance⟩ := target
-  ⟨aig, go input distance 0 (by omega) .empty⟩
+  ⟨aig, go input distance 0 (by omega) (.emptyWithCapacity w)⟩
 where
   go {aig : AIG α} (input : AIG.RefVec aig w) (distance : Nat) (curr : Nat) (hcurr : curr ≤ w)
       (s : AIG.RefVec aig curr) :
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.lean
index 776938ba76..93547c9684 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.lean
@@ -28,7 +28,7 @@ variable [Hashable α] [DecidableEq α]
 def blastShiftLeftConst (aig : AIG α) (target : AIG.ShiftTarget aig w) :
     AIG.RefVecEntry α w :=
   let ⟨input, distance⟩ := target
-  go aig input distance 0 (by omega) .empty
+  go aig input distance 0 (by omega) (.emptyWithCapacity w)
 where
   go (aig : AIG α) (input : AIG.RefVec aig w) (distance : Nat) (curr : Nat) (hcurr : curr ≤ w)
       (s : AIG.RefVec aig curr) :
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean
index 1bb6fa6ffa..4a673c628a 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean
@@ -28,7 +28,7 @@ variable [Hashable α] [DecidableEq α]
 def blastShiftRightConst (aig : AIG α) (target : AIG.ShiftTarget aig w) :
     AIG.RefVecEntry α w :=
   let ⟨input, distance⟩ := target
-  go aig input distance 0 (by omega) .empty
+  go aig input distance 0 (by omega) (.emptyWithCapacity w)
 where
   go (aig : AIG α) (input : AIG.RefVec aig w) (distance : Nat) (curr : Nat) (hcurr : curr ≤ w)
       (s : AIG.RefVec aig curr) :
@@ -99,7 +99,7 @@ instance : AIG.LawfulVecOperator α AIG.ShiftTarget blastShiftRightConst where
 def blastArithShiftRightConst (aig : AIG α) (target : AIG.ShiftTarget aig w) :
     AIG.RefVecEntry α w :=
   let ⟨input, distance⟩ := target
-  ⟨aig, go input distance 0 (by omega) .empty⟩
+  ⟨aig, go input distance 0 (by omega) (.emptyWithCapacity w)⟩
 where
   go {aig : AIG α} (input : AIG.RefVec aig w) (distance : Nat) (curr : Nat) (hcurr : curr ≤ w)
       (s : AIG.RefVec aig curr) :
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean
index c1a97962b5..eab57ee38f 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean
@@ -33,9 +33,9 @@ structure ShiftConcatInput (aig : AIG α) (len : Nat) where
 
 def blastShiftConcat (aig : AIG α) (input : ShiftConcatInput aig w) : AIG.RefVecEntry α w :=
   let ⟨lhs, bit⟩ := input
-  let bit := AIG.RefVec.empty.push bit
+  let bit := AIG.RefVec.emptyWithCapacity (w + 1) |>.push bit
   let new := bit.append lhs
-  blastZeroExtend aig ⟨_, new⟩
+  blastZeroExtend aig ⟨1 + w, new⟩
 
 instance : AIG.LawfulVecOperator α ShiftConcatInput blastShiftConcat where
   le_size := by
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ZeroExtend.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ZeroExtend.lean
index 66d6d8e084..edcb56f7fe 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ZeroExtend.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ZeroExtend.lean
@@ -24,7 +24,7 @@ variable [Hashable α] [DecidableEq α]
 def blastZeroExtend (aig : AIG α) (target : AIG.ExtendTarget aig newWidth) :
     AIG.RefVecEntry α newWidth :=
   let ⟨width, input⟩ := target
-  go aig width input newWidth 0 (by omega) .empty
+  go aig width input newWidth 0 (by omega) (.emptyWithCapacity newWidth)
 where
   go (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w) (newWidth : Nat) (curr : Nat)
       (hcurr : curr ≤ newWidth) (s : AIG.RefVec aig curr) :
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Var.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Var.lean
index 2e148fd8ad..4ac50f1cbe 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Var.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Var.lean
@@ -23,7 +23,7 @@ structure BVVar (width : Nat) where
   ident : Nat
 
 def blastVar (aig : AIG BVBit) (var : BVVar w) : AIG.RefVecEntry BVBit w :=
-  go aig w var.ident 0 .empty (by omega)
+  go aig w var.ident 0 (.emptyWithCapacity w) (by omega)
 where
   go (aig : AIG BVBit) (w : Nat) (a : Nat) (curr : Nat) (s : AIG.RefVec aig curr)
     (hcurr : curr ≤ w) :