diff --git a/LinearScan/Verify.hs b/LinearScan/Verify.hs
--- a/LinearScan/Verify.hs
+++ b/LinearScan/Verify.hs
@@ -341,10 +341,9 @@
         (Vector0.vnth maxReg (rsAllocs maxReg st) reg)))
     (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)
 
-checkReservation :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId ->
-                    UseVerifier -> PhysReg -> Blocks.VarId -> Verified 
-                    a1 a2 ()
-checkReservation maxReg mDict pc useVerifier reg var =
+checkReservation :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> PhysReg
+                    -> Blocks.VarId -> Verified a1 a2 ()
+checkReservation maxReg mDict pc reg var =
   Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
     let {
      err = errorT maxReg mDict pc (VarNotReservedForReg var ( reg)
@@ -357,17 +356,12 @@
        Prelude.Just var' ->
         Monad.unless (State0.coq_StateT_Monad mDict)
           (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce var) var') err;
-       Prelude.Nothing ->
-        case useVerifier of {
-         VerifyEnabledStrict -> err;
-         _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}})
-      (isReserved maxReg mDict reg))
+       Prelude.Nothing -> err}) (isReserved maxReg mDict reg))
     (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict)
 
-releaseReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier
-              -> PhysReg -> Blocks.VarId -> Prelude.Bool -> Verified 
-              a1 a2 ()
-releaseReg maxReg mDict pc useVerifier reg var fromSplit =
+releaseReg :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> PhysReg ->
+              Blocks.VarId -> Prelude.Bool -> Verified a1 a2 ()
+releaseReg maxReg mDict pc reg var fromSplit =
   Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
     Monad.bind (State0.coq_StateT_Monad mDict) (\st ->
       case Ssr.prop
@@ -383,20 +377,10 @@
               (Lens.set (\_ -> reservation) Prelude.Nothing))
             (rsStack maxReg st))) mDict;
        Prelude.Nothing ->
-        let {
-         err = errorT maxReg mDict pc (VarNotReservedForReg var ( reg)
-                 (Lens.view (Lens.stepdownl' (\_ -> reservation))
-                   (Vector0.vnth maxReg (rsAllocs maxReg st) reg))
-                 ((Prelude.succ) ((Prelude.succ) 0)))}
-        in
-        case useVerifier of {
-         VerifyEnabledStrict -> err;
-         _ ->
-          case Lens.view (Lens.stepdownl' (\_ -> reservation))
-                 (Vector0.vnth maxReg (rsAllocs maxReg st) reg) of {
-           Prelude.Just v -> err;
-           Prelude.Nothing ->
-            Applicative.pure (State0.coq_StateT_Applicative mDict) ()}}})
+        errorT maxReg mDict pc (VarNotReservedForReg var ( reg)
+          (Lens.view (Lens.stepdownl' (\_ -> reservation))
+            (Vector0.vnth maxReg (rsAllocs maxReg st) reg)) ((Prelude.succ)
+          ((Prelude.succ) 0)))})
       (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))
     (addMove maxReg mDict pc (Resolve.RSFreeReg ( reg) var fromSplit))
 
@@ -676,7 +660,7 @@
               (checkResidency maxReg mDict pc useVerifier reg var);
            UsePos.Temp ->
             Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
-              checkReservation maxReg mDict pc useVerifier reg var)
+              checkReservation maxReg mDict pc reg var)
               (checkAllocation maxReg mDict pc intervals (Prelude.Just
                 (Prelude.Just reg)) var (Prelude.pred pc) ((Prelude.succ)
                 ((Prelude.succ) 0)));
@@ -733,7 +717,7 @@
               (checkResidency maxReg mDict pc useVerifier reg var);
            UsePos.Temp ->
             Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
-              checkReservation maxReg mDict pc useVerifier reg var)
+              checkReservation maxReg mDict pc reg var)
               (checkAllocation maxReg mDict pc intervals (Prelude.Just
                 (Prelude.Just reg)) var (Prelude.pred pc) ((Prelude.succ)
                 ((Prelude.succ) 0)));
@@ -781,8 +765,7 @@
             (Monad.unless (State0.coq_StateT_Monad mDict)
               (Eqtype.eq_op (Fintype.ordinal_eqType maxReg)
                 (unsafeCoerce fromReg) (unsafeCoerce toReg))
-              (releaseReg maxReg mDict pc useVerifier fromReg fromVar
-                Prelude.False));
+              (releaseReg maxReg mDict pc fromReg fromVar Prelude.False));
          Resolve.Transfer fromReg fromVar toReg ->
           Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
             Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->
@@ -791,8 +774,7 @@
             (Monad.unless (State0.coq_StateT_Monad mDict)
               (Eqtype.eq_op (Fintype.ordinal_eqType maxReg)
                 (unsafeCoerce fromReg) (unsafeCoerce toReg))
-              (releaseReg maxReg mDict pc useVerifier fromReg fromVar
-                Prelude.False));
+              (releaseReg maxReg mDict pc fromReg fromVar Prelude.False));
          Resolve.Spill fromReg toSpillSlot fromSplit ->
           Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
             Monad.bind (State0.coq_StateT_Monad mDict) (\check ->
@@ -808,20 +790,25 @@
                Prelude.False ->
                 Applicative.pure (State0.coq_StateT_Applicative mDict) acc})
               (isResident maxReg mDict fromReg))
-            (releaseReg maxReg mDict pc useVerifier fromReg toSpillSlot
-              fromSplit);
+            (releaseReg maxReg mDict pc fromReg toSpillSlot fromSplit);
          Resolve.Restore fromSpillSlot toReg fromSplit ->
-          Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
-            Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->
-              Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->
-                Monad.bind (State0.coq_StateT_Monad mDict) (\x2 ->
-                  Applicative.pure (State0.coq_StateT_Applicative mDict)
-                    (Seq.rcons acc mv))
-                  (assignReg maxReg mDict pc useVerifier toReg fromSpillSlot))
-                (freeStack maxReg mDict pc useVerifier fromSpillSlot))
-              (addMove maxReg mDict pc
-                (Resolve.weakenResolvingMove maxReg mv)))
-            (reserveReg maxReg mDict pc toReg fromSpillSlot fromSplit);
+          Monad.bind (State0.coq_StateT_Monad mDict) (\check ->
+            Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
+              Monad.bind (State0.coq_StateT_Monad mDict) (\x0 ->
+                Monad.bind (State0.coq_StateT_Monad mDict) (\x1 ->
+                  Monad.bind (State0.coq_StateT_Monad mDict) (\x2 ->
+                    Applicative.pure (State0.coq_StateT_Applicative mDict)
+                      (Seq.rcons acc mv))
+                    (assignReg maxReg mDict pc useVerifier toReg
+                      fromSpillSlot))
+                  (freeStack maxReg mDict pc useVerifier fromSpillSlot))
+                (addMove maxReg mDict pc
+                  (Resolve.weakenResolvingMove maxReg mv)))
+              (Monad.unless (State0.coq_StateT_Monad mDict)
+                (Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType) check
+                  (unsafeCoerce (Prelude.Just fromSpillSlot)))
+                (reserveReg maxReg mDict pc toReg fromSpillSlot fromSplit)))
+            (isReserved maxReg mDict toReg);
          Resolve.AllocReg toVar toReg fromSplit ->
           Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
             Applicative.pure (State0.coq_StateT_Applicative mDict) acc)
@@ -829,8 +816,7 @@
          Resolve.FreeReg fromReg fromVar fromSplit ->
           Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
             Applicative.pure (State0.coq_StateT_Applicative mDict) acc)
-            (releaseReg maxReg mDict pc useVerifier fromReg fromVar
-              fromSplit);
+            (releaseReg maxReg mDict pc fromReg fromVar fromSplit);
          Resolve.AllocStack toVar ->
           Monad.bind (State0.coq_StateT_Monad mDict) (\x ->
             Applicative.pure (State0.coq_StateT_Applicative mDict) acc)
diff --git a/linearscan.cabal b/linearscan.cabal
--- a/linearscan.cabal
+++ b/linearscan.cabal
@@ -1,5 +1,5 @@
 name:          linearscan
-version:       0.10.0
+version:       0.10.1
 synopsis:      Linear scan register allocator, formally verified in Coq
 homepage:      http://github.com/jwiegley/linearscan
 license:       BSD3