diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index df1f6d4c69c7b4c166d53cd3a37fe7ebf57f7c11..85bbedc67506a4b65651b5e75b42c0eaeac521bc 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -34,7 +34,7 @@ Proof.
     iDestruct (own_cnt_valid_2 with "Hcnt' Hcnt")
       as %[?%nat_included _]%auth_both_valid_discrete; lia. }
   iMod (box_empty with "Hbox") as "[HP Hbox]"=>//.
-  { (* FIXME [solve_ndisj] fails *) set_solver-. }
+  { (* FIXME [solve_ndisj] fails *) set_solver+. }
   { intros i s. by rewrite lookup_fmap fmap_Some=> -[? [/HB -> ->]]. }
   rewrite lft_vs_unfold; iDestruct "Hvs" as (n) "[Hcnt Hvs]".
   iDestruct (big_sepS_filter_acc (.⊂ κ) _ _ (dom _ I) with "Halive")
@@ -42,7 +42,7 @@ Proof.
   { intros κ'. rewrite elem_of_dom. eauto. }
   iApply fupd_trans. iApply fupd_mask_mono; last
   iMod ("Hvs" $! I with "[HI Halive] HP Hκ") as "(Hinv & HQ & Hcnt')".
-  { set_solver-. }
+  { set_solver+. }
   { rewrite lft_vs_inv_unfold. iFrame. }
   rewrite lft_vs_inv_unfold; iDestruct "Hinv" as "(HI&Halive)".
   iSpecialize ("Halive'" with "Halive").
diff --git a/theories/lifetime/model/reborrow.v b/theories/lifetime/model/reborrow.v
index 27ee3e79b5184d040f895be01e894a553db966a2..f8502152a37af379eac16b89ba94bb97db92daf1 100644
--- a/theories/lifetime/model/reborrow.v
+++ b/theories/lifetime/model/reborrow.v
@@ -82,7 +82,7 @@ Proof.
     rewrite /to_borUR lookup_fmap. by rewrite HB. }
   iMod (slice_fill _ _ false with "Hislice HP Hbox")
      as "Hbox".
-  { set_solver-. }
+  { set_solver+. }
   { by rewrite lookup_fmap HB. }
   iDestruct (@big_sepM_delete with "HB") as "[Hcnt HB]"; first done.
   rewrite /=. iDestruct "Hcnt" as "[% H1â—¯]".
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 238dd508fb7872f26256cec465fd8933ebe27df1..c85c868c70a8664e251b7e3822259b54564650bf 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -92,7 +92,7 @@ Section arc.
     iMod ("Hν†" with "Hν") as "H". iModIntro. iNext. iApply fupd_trans.
     iMod "H" as "#Hν".
     iMod fupd_mask_subseteq as "Hclose2"; last iMod ("Hvs" with "Hν") as "$".
-    { set_solver-. }
+    { set_solver+. }
     iIntros "{$Hν} !>".
     iMod "Hclose2" as "_". iApply "Hclose". auto.
   Qed.
@@ -397,7 +397,7 @@ Section arc.
     (* All right, we are done preparing our context. Let's get going. *)
     iMod (lft_create with "LFT") as (ν) "[Hν Hν†]"; first done.
     wp_bind (_ +ₗ _)%E. iSpecialize ("Hν†" with "Hν").
-    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+..|].
     wp_op. iIntros "#H† !>". rewrite shift_loc_0. wp_write. wp_op. wp_write. wp_write.
     iApply (type_type _ _ _ [ #lrc ◁ box (weak ty)]
             with "[] LFT HE Hna HL Hk [>-]"); last first.
@@ -771,7 +771,7 @@ Section arc.
       iDestruct "Hpersist" as "(? & ? & H†)". wp_bind (_ <- _)%E.
       iDestruct "Hdrop" as "[Hν Hdrop]". iSpecialize ("H†" with "Hν").
       iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); first done.
-      { set_solver-. (* FIXME [solve_ndisj] fails *) }
+      { set_solver+. (* FIXME [solve_ndisj] fails *) }
       iDestruct "Hown" as (???) "(_ & Hlen & _)". wp_write. iIntros "(#Hν & Hown & H†)!>".
       wp_seq. wp_op. wp_op. iDestruct "Hown" as (?) "[H↦ Hown]".
       iDestruct (ty_size_eq with "Hown") as %?. rewrite Max.max_0_r.
@@ -875,7 +875,7 @@ Section arc.
       iDestruct "Hpersist" as "(Ha & _ & H†)". wp_bind (_ <- _)%E.
       iSpecialize ("H†" with "Hν").
       iApply wp_mask_mono; last iApply (wp_step_fupd with "H†"); first done.
-      { (* FIXME [solve_ndisj] fails *) set_solver-. }
+      { (* FIXME [solve_ndisj] fails *) set_solver+. }
       wp_write. iIntros "(#Hν & Hown & H†) !>". wp_seq. wp_op. wp_op.
       rewrite -(firstn_skipn ty.(ty_size) vl0) heap_mapsto_vec_app.
       iDestruct "Hr1" as "[Hr1 Hr2]". iDestruct "Hown" as (vl) "[Hrc' Hown]".
@@ -950,7 +950,7 @@ Section arc.
     wp_apply (is_unique_spec with "Hi Htoks"). iIntros ([]) "H"; wp_if.
     - iDestruct "H" as "(Hrc & Hrc1 & Hν)". iSpecialize ("Hc" with "Hν"). wp_bind Skip.
       iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); first done.
-      { (* FIXME [solve_ndisj] fails *) set_solver-. }
+      { (* FIXME [solve_ndisj] fails *) set_solver+. }
       wp_seq. iIntros "(#Hν & Hown & H†) !>". wp_seq.
       iMod ("Hclose2" with "[Hrc Hrc1 H†] Hown") as "[Hb Hα]".
       { iIntros "!> Hown !>". iLeft. iFrame. }
@@ -1036,7 +1036,7 @@ Section arc.
     - iIntros "(Hrc0 & Hrc1 & HP1)". wp_case. wp_bind (_ +â‚— _)%E.
       iSpecialize ("Hc" with "HP1").
       iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); first done.
-      { (* FIXME [solve_ndisj] fails *) set_solver-. }
+      { (* FIXME [solve_ndisj] fails *) set_solver+. }
       wp_op. iIntros "(#Hν & Hrc2 & H†)". iModIntro.
       iMod ("Hclose2" with "[Hrc'↦ Hrc0 Hrc1 H†] Hrc2") as "[Hb Hα1]".
       { iIntros "!> Hrc2". iExists [_]. rewrite heap_mapsto_vec_singleton.
@@ -1052,7 +1052,7 @@ Section arc.
       iApply type_jump; solve_typing.
     - iIntros "[Hν Hweak]". wp_case. iSpecialize ("Hc" with "Hν"). wp_bind (new _). 
       iApply wp_mask_mono; last iApply (wp_step_fupd with "Hc"); first done.
-      { (* FIXME [solve_ndisj] fails *) set_solver-. }
+      { (* FIXME [solve_ndisj] fails *) set_solver+. }
       wp_apply wp_new=>//. lia. iIntros (l) "(H† & Hlvl) (#Hν & Hown & H†') !>".
       rewrite -!lock Nat2Z.id.
       wp_let. wp_op. rewrite !heap_mapsto_vec_cons shift_loc_assoc shift_loc_0.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 10251242c7f592d4226ff923c5fa9f8b9d929abd..e2ed4647477cfce84bb80db1a36d93fd0006b868 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -299,7 +299,7 @@ Section code.
                last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
              iModIntro. iNext. iMod "H†".
              iMod fupd_mask_subseteq as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
-             { set_solver-. }
+             { set_solver+. }
              iMod "Hclose2" as "_". iModIntro.
              iMod ("Hclose" with "[Hst $Hna]") as "$"; first by iExists _; iFrame.
              iModIntro. iNext. iDestruct "Hty" as (vl) "[??]". iExists _. iFrame.
@@ -314,7 +314,7 @@ Section code.
                   last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
                 iModIntro. iNext. iMod "H†".
                 iMod fupd_mask_subseteq as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
-                { set_solver-. }
+                { set_solver+. }
                 iMod "Hclose2" as "_". iModIntro.
                 iMod (own_update_2 with "Hst Htok") as "Hst".
                 { apply auth_update_dealloc, prod_local_update_1,
@@ -335,7 +335,7 @@ Section code.
             last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
           iModIntro. iNext. iMod "H†".
           iMod fupd_mask_subseteq as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
-          { set_solver-. }
+          { set_solver+. }
           iMod "Hclose2" as "_". iModIntro.
           iMod ("Hclose" with "[Hst $Hna Hl1 Hl2]") as "$";
             first by iExists _; iFrame; iFrame.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 5f2f3df241ec6ec6e1eba6011dcfe6c7daa25ade..dfea77e5d76f7cbfae005a429ce72d38cf44a792 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -463,7 +463,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+..|].
     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 9e16fc4f5043d53925d0631d433142e778b64070..a77c45b8ce2cfb03e778c86f3473405273c80cea 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -179,10 +179,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 3cb95d6b9b896c66f74cda8f77b52f7bb9f0a6bb..72219bfa2efdb0dd75c56ebf90c224b43a1f5d8f 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -151,11 +151,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 f2f279ec3440f67854a8f73d7e06d80f34d0c816..17320a4946e3e873f6e38b20aceab30dc68fec4d 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -204,7 +204,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.
             * done.
           + iExists _. iFrame. by rewrite Qp_div_2. }
@@ -284,7 +284,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.
           * 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 4b1c9d04f0f2a1ee34bd11bd136d60dd983e1d19..4dc1d3bd17825f81b81d1f71062592624284fef8 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -149,11 +149,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"); [set_solver-|]. wp_seq. iIntros "{Hb} Hb !>".
+    iApply (wp_step_fupd with "INV"); [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/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index f1d4d70e84df5f9840e295edf92d062bfa234741..e5ac1c55c47d3a7afd40fa6913bf9ca726b2faee 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -96,14 +96,14 @@ Section rwlockreadguard_functions.
           iCombine "Hν" "Hν'" as "Hν". iDestruct "Hq" as %->.
           iApply (step_fupd_mask_mono ((↑lftN ∪ lft_userE) ∪ (⊤ ∖ ↑rwlockN ∖ ↑lftN ∖ lft_userE)));
             last iApply (step_fupd_mask_frame_r _ (lft_userE)).
-          { set_solver-. }
+          { set_solver+. }
           { solve_ndisj. }
           { rewrite difference_difference. apply: disjoint_difference_r1. done. }
           { (* FIXME [solve_ndisj] fails. *)
             apply: disjoint_difference_r1. done. }
           iMod ("H†" with "Hν") as "H†". iModIntro. iNext. iMod "H†".
           iMod fupd_mask_subseteq as "Hclose"; last iMod ("Hh" with "H†") as "Hb".
-          { set_solver-. }
+          { set_solver+. }
           iMod "Hclose" as "_". iIntros "!> Hlx". iExists None. iFrame.
           iApply (own_update_2 with "H● H◯"). apply auth_update_dealloc.
           rewrite -(right_id None op (Some _)). apply cancel_local_update_unit, _.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 4eba7c32762b73c276f8804491c6dabe8e342e7f..d3e564c7daf85c22a2d0ca798291bad818ec3d6f 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -220,7 +220,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"); first set_solver-. wp_seq.
+    iApply (wp_step_fupd with "Hend"); first 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.