diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 0750228b59bc6b239ee19bde7b888ab52ea90781..d228d2ad678e26629159370fbc07ae5bae439017 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -34,7 +34,7 @@ Proof.
     rewrite /lft_inv_dead; iDestruct "Hdead" as (R Vinh) "(_ & _ & Hcnt' & _)".
     iDestruct (own_cnt_valid_2 with "Hcnt' Hcnt")
       as %[?%nat_included _]%auth_both_valid_discrete; lia. }
-  iMod (box_empty with "Hbox") as "[HP Hbox]"=>//; first set_solver.
+  iMod (box_empty with "Hbox") as "[HP Hbox]"=>//; first set_solver+.
   { intros i s. by rewrite lookup_fmap fmap_Some=>-[? [/HB [?[-> ?]] ->]] /=. }
   rewrite lft_vs_unfold; iDestruct "Hvs" as (Vκ n) "(% & Hcnt & Hvs)".
   iDestruct (big_sepS_filter_acc (.⊂ κ) _ _ (dom _ I) with "Halive")
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 5f358ab2a7c9550e9af722b1e8b3ee6b3f0bc30c..6df9fa6724bed909f19144800490416c22b094da 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -469,7 +469,7 @@ Section code.
     wp_op. rewrite shift_loc_0. wp_write. wp_op. wp_write.
     iMod (lft_create with "LFT") as (ν) "[Hν #Hν†]"; first done.
     iPoseProof ("Hν†" with "Hν") as "H†". wp_bind (_ <- _)%E.
-    iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); [set_solver-..|].
+    iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); [set_solver+..|].
     iApply (wp_mask_mono _ (↑histN)); [set_solver+|]. wp_write. iIntros "#Hν !>". wp_seq.
     iApply (type_type _ _ _ [ #lw ◁ box (weak ty)]
         with "[] LFT HE Hna HL Hk [> -]"); last first.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 642303b4618f8ca08c28cf0ee7a3fe1d1e67819d..1efbe3bba48da4a9b2b5ce649e1e17499fd5fa70 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -178,10 +178,10 @@ Section ref_functions.
         { apply auth_update_dealloc.
           rewrite -(agree_idemp (to_agree _)) !pair_op Some_op.
           apply (cancel_local_update_unit (reading_stR q ν)), _. }
-        iApply step_fupd_intro; first set_solver-. iExists (q+q'')%Qp. iFrame.
+        iApply step_fupd_intro; first set_solver+. iExists (q+q'')%Qp. iFrame.
         by rewrite assoc (comm _ q0 q). }
     wp_bind Endlft. iApply (wp_mask_mono _ (↑lftN ∪ lft_userE)); first done.
-    iApply (wp_step_fupd with "INV"); [set_solver-..|]. wp_seq.
+    iApply (wp_step_fupd with "INV"); [set_solver+..|]. wp_seq.
     iIntros "INV !>". wp_seq. iMod ("Hcloseβ" with "[$INV] Hna") as "[Hβ Hna]".
     iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
     iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)] with "[] LFT HE Hna HL Hk");
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 1ddebc8d8933636ea00d737b1bd0807a6b9d5f0d..6d60ef565534de864f9fd3799bc7eb4482c89b6d 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -150,11 +150,11 @@ Section refcell.
       iExists γ, _. iFrame "Hst Hn Hshr".
       iSplitR "Htok2"; last by iExists _; iFrame; rewrite Qp_div_2.
       iIntros "!> !> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
-      iApply fupd_mask_mono; last iApply "Hh". set_solver-. rewrite -lft_dead_or. auto.
+      iApply fupd_mask_mono; last iApply "Hh". set_solver+. rewrite -lft_dead_or. auto.
     - iMod (own_alloc (● (refcell_st_to_R $ Some (static, true, (1/2)%Qp, n)))) as (γ) "Hst".
       { by apply auth_auth_valid. }
       iFrame "Htok'". iExists γ, _. iFrame. iSplitR.
-      { rewrite -step_fupd_intro. auto. set_solver-. }
+      { rewrite -step_fupd_intro. auto. set_solver+. }
       iSplitR; [|done]. iExists (1/2)%Qp. rewrite Qp_div_2. iSplitR; [done|].
       iApply lft_tok_static.
   Qed.
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index cbb23dcbad48d96f690b8dce8917a66cb787d25c..138cd08a804aee6ef8afc0c09b8c08d901f177b3 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -203,7 +203,7 @@ Section refcell_functions.
           + iIntros "!> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro.
             iNext. iMod "Hν".
             iMod fupd_mask_subseteq as "Hclose"; last iMod ("Hh" with "[Hν]") as "$".
-            { set_solver-. }
+            { set_solver+. }
             * rewrite -lft_dead_or. auto.
             * iMod "Hclose". done.
           + iExists _. iFrame. by rewrite Qp_div_2. }
@@ -283,7 +283,7 @@ Section refcell_functions.
       { iExists _. iFrame. iNext. iSplitL "Hbh".
         - iIntros "Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
           iMod fupd_mask_subseteq as "Hclose"; last iMod ("Hbh" with "[Hν]") as "$".
-          { set_solver-. }
+          { set_solver+. }
           * rewrite -lft_dead_or. auto.
           * iMod "Hclose". done.
         - iSplitL; [|done]. iExists _. iFrame. by rewrite Qp_div_2. }
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 4e431eaaa8ccded2effedb5892fc2d4721d4f23f..94722140447ea863db22e0ea492d4fa8315f057f 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -148,11 +148,11 @@ Section refmut_functions.
         iDestruct "INV" as "(H† & Hq & _)".
         rewrite /= (_:Z.neg (1%positive ⋅ n') + 1 = Z.neg n');
           last (rewrite pos_op_plus; lia). iFrame.
-        iApply step_fupd_intro; [set_solver-|]. iSplitL; [|done].
+        iApply step_fupd_intro; [set_solver+|]. iSplitL; [|done].
         iDestruct "Hq" as (q' ?) "?". iExists (q+q')%Qp. iFrame.
         rewrite assoc (comm _ q'' q) //. }
     wp_bind Endlft. iApply (wp_mask_mono _ (↑lftN ∪ lft_userE)); first done.
-    iApply (wp_step_fupd with "INV"); [done|set_solver-|]. wp_seq. iIntros "{Hb} Hb !>".
+    iApply (wp_step_fupd with "INV"); [done|set_solver+|]. wp_seq. iIntros "{Hb} Hb !>".
     iMod ("Hcloseβ" with "Hb Hna") as "[Hβ Hna]".
     iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL". wp_seq.
     iApply (type_type _ _ _ [ #lx ◁ box (uninit 2)]
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 4e81d04ad33518c35f918acac50a420c07b4f8aa..d7c12c479d433b83f36c1467bcc3c2ab145fe8ad 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -223,7 +223,7 @@ Section typing_rules.
     iDestruct "Hκ" as (Λ) "(% & Htok & Hend)".
     iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
     iApply (wp_mask_mono _ (↑lftN ∪ lft_userE)); first done.
-    iApply (wp_step_fupd with "Hend"); [done|set_solver-|]. wp_seq.
+    iApply (wp_step_fupd with "Hend"); [done|set_solver+|]. wp_seq.
     iIntros "#Hdead !>". wp_seq. iApply ("He" with "LFT HE Htl HL HC [> -]").
     iApply (Hub with "[] HT"). simpl in *. subst κ. rewrite -lft_dead_or. auto.
   Qed.