diff --git a/_CoqProject b/_CoqProject
index 80e5f22d8549d0d8c2cca5c92572011c3b53cea2..d90fb6ab6d0e3e1446f985916c89119d7d7301b2 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,8 +1,8 @@
 # Search paths for all packages. They must all match the regex
 # `-Q $PACKAGE[/ ]` so that we can filter out the right ones for each package.
 -Q stdpp stdpp
+-Q stdpp_bitvector stdpp.bitvector
 -Q stdpp_unstable stdpp.unstable
--Q stdpp_bitvector stdpp.bv
 # Fixing this one requires Coq 8.19
 -arg -w -arg -argument-scope-delimiter
 
@@ -56,6 +56,7 @@ stdpp/telescopes.v
 stdpp/binders.v
 stdpp/ssreflect.v
 
-stdpp_bitvector/bitblast.v
 stdpp_bitvector/bitvector.v
 stdpp_bitvector/bitvector_tactics.v
+
+stdpp_unstable/bitblast.v
diff --git a/coq-stdpp-bitvector.opam b/coq-stdpp-bitvector.opam
index 6d8d5eb57644e6dda20230437ac6cb390feec44c..e36c977c65e643278a2211ceca3270e0b4fa9c01 100644
--- a/coq-stdpp-bitvector.opam
+++ b/coq-stdpp-bitvector.opam
@@ -7,12 +7,15 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/stdpp/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/iris/stdpp.git"
 version: "dev"
 
-synopsis: "std++ bitvector"
+synopsis: "A library for bitvectors based on std++"
 description: """
-Needs description
+This library provides the `bv n` type for representing n-bit bitvectors (i.e.,
+fixed-size integers with n bits). It comes with definitions for the standard operations
+(e.g., the operations exposed by SMT-LIB) and some basic automation for solving bitvector
+goals based on the lia tactic.
 """
 tags: [
-  "logpath:stdpp.bv"
+  "logpath:stdpp.bitvector"
 ]
 
 depends: [
diff --git a/coq-stdpp-unstable.opam b/coq-stdpp-unstable.opam
index f0332325ee882f49e76753df2442735bb04b025e..936f6220f6c45495e7137c933e4885c73ba6313e 100644
--- a/coq-stdpp-unstable.opam
+++ b/coq-stdpp-unstable.opam
@@ -18,6 +18,7 @@ tags: [
 
 depends: [
   "coq-stdpp" {= version}
+  "coq-stdpp-bitvector" {= version}
 ]
 
 build: ["./make-package" "stdpp_unstable" "-j%{jobs}%"]
diff --git a/stdpp_bitvector/bitvector.v b/stdpp_bitvector/bitvector.v
index 767a7c1f3b2a052f0e97c2617b9dea9026c30e71..10105bef82ee1ac0b60d9fdc2816105a243c34e7 100644
--- a/stdpp_bitvector/bitvector.v
+++ b/stdpp_bitvector/bitvector.v
@@ -1,6 +1,4 @@
-(** This file is still experimental. See its tracking issue
-https://gitlab.mpi-sws.org/iris/stdpp/-/issues/145 for details on remaining
-issues before stabilization. This file is maintained by Michael Sammler. *)
+(** This file is maintained by Michael Sammler. *)
 From stdpp Require Export numbers.
 From stdpp Require Import countable finite.
 From stdpp Require Import options.
diff --git a/stdpp_bitvector/bitvector_tactics.v b/stdpp_bitvector/bitvector_tactics.v
index 65c8bcd58f0ad42c24dda6f3202c41870286373e..e6a6fa02ad2c579a9c8c04dd56292221bcf43018 100644
--- a/stdpp_bitvector/bitvector_tactics.v
+++ b/stdpp_bitvector/bitvector_tactics.v
@@ -1,8 +1,5 @@
-(** This file is still experimental. See its tracking issue
-https://gitlab.mpi-sws.org/iris/stdpp/-/issues/146 for details on remaining
-issues before stabilization. This file is maintained by Michael Sammler. *)
-From stdpp.bv Require Export bitvector.
-From stdpp.bv Require Import bitblast.
+(** This file is maintained by Michael Sammler. *)
+From stdpp.bitvector Require Export bitvector.
 From stdpp Require Import options.
 
 (** * bitvector tactics *)
@@ -63,30 +60,7 @@ Tactic Notation "reduce_closed" constr(x) :=
   change_no_check x with r in *
 .
 
-(** * bitblast instances *)
-Lemma bitblast_bool_to_Z b n:
-  Bitblast (bool_to_Z b) n (bool_decide (n = 0) && b).
-Proof.
-  constructor. destruct b; simpl_bool; repeat case_bool_decide;
-    subst; try done; rewrite ?Z.bits_0; by destruct n.
-Qed.
-Global Hint Resolve bitblast_bool_to_Z | 10 : bitblast.
-
-Lemma bitblast_bounded_bv_unsigned n (b : bv n):
-  BitblastBounded (bv_unsigned b) (Z.of_N n).
-Proof. constructor. apply bv_unsigned_in_range. Qed.
-Global Hint Resolve bitblast_bounded_bv_unsigned | 15 : bitblast.
-
-Lemma bitblast_bv_wrap z1 n n1 b1:
-  Bitblast z1 n b1 →
-  Bitblast (bv_wrap n1 z1) n (bool_decide (n < Z.of_N n1) && b1).
-Proof.
-  intros [<-]. constructor.
-  destruct (decide (0 ≤ n)); [by rewrite bv_wrap_spec| rewrite !Z.testbit_neg_r; [|lia..]; btauto].
-Qed.
-Global Hint Resolve bitblast_bv_wrap | 10 : bitblast.
-
-(* The following two lemmas are proven using [bitblast]. *)
+(** * General lemmas *)
 Lemma bv_extract_concat_later m n1 n2 s l (b1 : bv n1) (b2 : bv n2):
   (n2 ≤ s)%N →
   (m = n1 + n2)%N →
@@ -94,7 +68,11 @@ Lemma bv_extract_concat_later m n1 n2 s l (b1 : bv n1) (b2 : bv n2):
 Proof.
   intros ? ->. apply bv_eq.
   rewrite !bv_extract_unsigned, bv_concat_unsigned, !bv_wrap_land by done.
-  bitblast. f_equal. lia.
+  apply Z.bits_inj_iff' => ??.
+  rewrite !Z.land_spec, !Z.shiftr_spec, Z.lor_spec, Z.shiftl_spec, Z.ones_spec; [|lia..].
+  case_bool_decide; rewrite ?andb_false_r, ?andb_true_r; [|done].
+  rewrite <-(bv_wrap_bv_unsigned _ b2), bv_wrap_spec_high, ?orb_false_r; [|lia].
+  f_equal. lia.
 Qed.
 Lemma bv_extract_concat_here m n1 n2 s (b1 : bv n1) (b2 : bv n2):
   s = 0%N →
@@ -103,7 +81,11 @@ Lemma bv_extract_concat_here m n1 n2 s (b1 : bv n1) (b2 : bv n2):
 Proof.
   intros -> ->. apply bv_eq.
   rewrite !bv_extract_unsigned, bv_concat_unsigned, !bv_wrap_land by done.
-  bitblast. f_equal. lia.
+  apply Z.bits_inj_iff' => ??.
+  rewrite !Z.land_spec, !Z.shiftr_spec, Z.lor_spec, Z.shiftl_spec, Z.ones_spec; [|lia..].
+  case_bool_decide; rewrite ?andb_false_r, ?andb_true_r.
+  - rewrite (Z.testbit_neg_r (bv_unsigned b1)); [|lia]. simpl. f_equal. lia.
+  - rewrite <-(bv_wrap_bv_unsigned _ b2), bv_wrap_spec_high, ?orb_false_l; lia.
 Qed.
 
 (** * [bv_simplify] rewrite database *)
@@ -500,7 +482,7 @@ Tactic Notation "bv_simplify" ident(H) :=
   | not (_ =@{bv _} _) => apply bv_neq in H
   | _ => idtac
   end;
-  tactic bv_unfold in H;
+  do [bv_unfold] in H;
   autorewrite with bv_unfolded_simplify in H.
 Tactic Notation "bv_simplify" "select" open_constr(pat) :=
   select pat (fun H => bv_simplify H).
diff --git a/stdpp_bitvector/bitblast.v b/stdpp_unstable/bitblast.v
similarity index 96%
rename from stdpp_bitvector/bitblast.v
rename to stdpp_unstable/bitblast.v
index 37c97db3ebe39d86017c00a9bdbfe2d94e0d5333..46d7f8044d7d87b13b4ce045ce962def7ee78d30 100644
--- a/stdpp_bitvector/bitblast.v
+++ b/stdpp_unstable/bitblast.v
@@ -3,6 +3,7 @@ https://gitlab.mpi-sws.org/iris/stdpp/-/issues/141 for details on remaining
 issues before stabilization. This file is maintained by Michael Sammler. *)
 From Coq Require Import ssreflect.
 From Coq.btauto Require Export Btauto.
+From stdpp.bitvector Require Import bitvector.
 From stdpp Require Export tactics numbers list.
 From stdpp Require Import options.
 
@@ -406,7 +407,27 @@ Proof.
   - by apply Z.clearbit_eq.
 Qed.
 Global Hint Resolve bitblast_clearbit | 10 : bitblast.
+Lemma bitblast_bool_to_Z b n:
+  Bitblast (bool_to_Z b) n (bool_decide (n = 0) && b).
+Proof.
+  constructor. destruct b; simpl_bool; repeat case_bool_decide;
+    subst; try done; rewrite ?Z.bits_0; by destruct n.
+Qed.
+Global Hint Resolve bitblast_bool_to_Z | 10 : bitblast.
 
+(** Instances for [bv] *)
+Lemma bitblast_bv_wrap z1 n n1 b1:
+  Bitblast z1 n b1 →
+  Bitblast (bv_wrap n1 z1) n (bool_decide (n < Z.of_N n1) && b1).
+Proof.
+  intros [<-]. constructor.
+  destruct (decide (0 ≤ n)); [by rewrite bv_wrap_spec| rewrite !Z.testbit_neg_r; [|lia..]; btauto].
+Qed.
+Global Hint Resolve bitblast_bv_wrap | 10 : bitblast.
+Lemma bitblast_bounded_bv_unsigned n (b : bv n):
+  BitblastBounded (bv_unsigned b) (Z.of_N n).
+Proof. constructor. apply bv_unsigned_in_range. Qed.
+Global Hint Resolve bitblast_bounded_bv_unsigned | 15 : bitblast.
 
 (** * Tactics *)
 
diff --git a/tests/bitblast.v b/tests/bitblast.v
index 15bc7e09a2cbc4076cd1cf96831788562e510d66..e68bbfc8b5a4c4149e18f735a57eb107e9f7fe41 100644
--- a/tests/bitblast.v
+++ b/tests/bitblast.v
@@ -1,4 +1,4 @@
-From stdpp.bv Require Import bitblast.
+From stdpp.unstable Require Import bitblast.
 
 Local Open Scope Z_scope.
 
diff --git a/tests/bitvector.v b/tests/bitvector.v
index 5ea0529cd9d3018ab18bd5653c7adb7caa944304..2384f7d594c27fcbafe40b14f46014934ac6a7e4 100644
--- a/tests/bitvector.v
+++ b/tests/bitvector.v
@@ -1,5 +1,5 @@
 From stdpp Require Import strings.
-From stdpp.bv Require Import bitvector.
+From stdpp.bitvector Require Import bitvector.
 
 Check "notation_test".
 Check (BV 10 3 = BV 10 5).
diff --git a/tests/bitvector_tactics.v b/tests/bitvector_tactics.v
index a2ed007e74f2d97f0fedcafd0281d1517692b1c2..7046d7629953d28ae0565af97407ddc914900e1b 100644
--- a/tests/bitvector_tactics.v
+++ b/tests/bitvector_tactics.v
@@ -1,5 +1,6 @@
 From stdpp Require Import strings.
-From stdpp.bv Require Import bitblast bitvector_tactics.
+From stdpp.bitvector Require Import bitvector_tactics.
+From stdpp.unstable Require Import bitblast.
 Unset Mangle Names.
 
 Local Open Scope Z_scope.