diff --git a/quickcheck-dynamic/quickcheck-dynamic.cabal b/quickcheck-dynamic/quickcheck-dynamic.cabal
index eabc03f5..ea419ed1 100644
--- a/quickcheck-dynamic/quickcheck-dynamic.cabal
+++ b/quickcheck-dynamic/quickcheck-dynamic.cabal
@@ -83,6 +83,7 @@ library
     , mtl
     , QuickCheck
     , random
+    , singletons
 
 test-suite quickcheck-dynamic-test
   import:         lang
diff --git a/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic.hs b/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic.hs
index 30713f27..4a3f6ec5 100644
--- a/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic.hs
+++ b/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic.hs
@@ -60,10 +60,10 @@ instance Monad (DL s) where
 instance MonadFail (DL s) where
   fail = errorDL
 
-action :: (Typeable a, Eq (Action s a), Show (Action s a)) => Action s a -> DL s (Var a)
+action :: (Typeable a, Eq (Action s Symbolic a), Show (Action s Symbolic a)) => Action s Symbolic a -> DL s (Var Symbolic a)
 action cmd = DL $ \_ k -> DL.after cmd k
 
-failingAction :: (Typeable a, Eq (Action s a), Show (Action s a)) => Action s a -> DL s ()
+failingAction :: (Typeable a, Eq (Action s Symbolic a), Show (Action s Symbolic a)) => Action s Symbolic a -> DL s ()
 failingAction cmd = DL $ \_ k -> DL.afterNegative cmd (k ())
 
 anyAction :: DL s ()
@@ -90,13 +90,13 @@ weight w = DL $ \s k -> DL.weight w (k () s)
 getSize :: DL s Int
 getSize = DL $ \s k -> DL.withSize $ \n -> k n s
 
-getModelStateDL :: DL s s
+getModelStateDL :: DL s (s Symbolic)
 getModelStateDL = DL $ \s k -> k (underlyingState s) s
 
 getVarContextDL :: DL s VarContext
 getVarContextDL = DL $ \s k -> k (vars s) s
 
-forAllVar :: forall a s. Typeable a => DL s (Var a)
+forAllVar :: forall a s. Typeable a => DL s (Var Symbolic a)
 forAllVar = do
   xs <- ctxAtType <$> getVarContextDL
   forAllQ $ elementsQ xs
@@ -114,7 +114,7 @@ errorDL name = DL $ \_ _ -> DL.errorDL name
 assert :: String -> Bool -> DL s ()
 assert name b = if b then return () else errorDL name
 
-assertModel :: String -> (s -> Bool) -> DL s ()
+assertModel :: String -> (s Symbolic -> Bool) -> DL s ()
 assertModel name p = assert name . p =<< getModelStateDL
 
 monitorDL :: (Property -> Property) -> DL s ()
diff --git a/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic/Internal.hs b/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic/Internal.hs
index d8388927..2a1fbc6c 100644
--- a/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic/Internal.hs
+++ b/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic/Internal.hs
@@ -32,8 +32,8 @@ data DynLogic s
     Stopping (DynLogic s)
   | -- | After a specific action the predicate should hold
     forall a.
-    (Eq (Action s a), Show (Action s a), Typeable a) =>
-    After (ActionWithPolarity s a) (Var a -> DynPred s)
+    (Eq (Action s Symbolic a), Show (Action s Symbolic a), Typeable a) =>
+    After (ActionWithPolarity s a) (Var Symbolic a -> DynPred s)
   | Error String (DynPred s)
   | -- | Adjust the probability of picking a branch
     Weight Double (DynLogic s)
@@ -65,18 +65,18 @@ afterAny :: (Annotated s -> DynFormula s) -> DynFormula s
 afterAny f = DynFormula $ \n -> AfterAny $ \s -> unDynFormula (f s) n
 
 afterPolar
-  :: (Typeable a, Eq (Action s a), Show (Action s a))
+  :: (Typeable a, Eq (Action s Symbolic a), Show (Action s Symbolic a))
   => ActionWithPolarity s a
-  -> (Var a -> Annotated s -> DynFormula s)
+  -> (Var Symbolic a -> Annotated s -> DynFormula s)
   -> DynFormula s
 afterPolar act f = DynFormula $ \n -> After act $ \x s -> unDynFormula (f x s) n
 
 -- | Given `f` must be `True` after /some/ action.
 -- `f` is passed the state resulting from executing the `Action`.
 after
-  :: (Typeable a, Eq (Action s a), Show (Action s a))
-  => Action s a
-  -> (Var a -> Annotated s -> DynFormula s)
+  :: (Typeable a, Eq (Action s Symbolic a), Show (Action s Symbolic a))
+  => Action s Symbolic a
+  -> (Var Symbolic a -> Annotated s -> DynFormula s)
   -> DynFormula s
 after act f = afterPolar (ActionWithPolarity act PosPolarity) f
 
@@ -84,8 +84,8 @@ after act f = afterPolar (ActionWithPolarity act PosPolarity) f
 -- `f` is passed the state resulting from executing the `Action`
 -- as a negative action.
 afterNegative
-  :: (Typeable a, Eq (Action s a), Show (Action s a))
-  => Action s a
+  :: (Typeable a, Eq (Action s Symbolic a), Show (Action s Symbolic a))
+  => Action s Symbolic a
   -> (Annotated s -> DynFormula s)
   -> DynFormula s
 afterNegative act f = afterPolar (ActionWithPolarity act NegPolarity) (const f)
@@ -127,7 +127,7 @@ withSize :: (Int -> DynFormula s) -> DynFormula s
 withSize f = DynFormula $ \n -> unDynFormula (f n) n
 
 -- | Prioritise doing this if we are
--- trying to stop generation.
+-- trying to stop Symbolic.
 toStop :: DynFormula s -> DynFormula s
 toStop (DynFormula f) = DynFormula $ Stopping . f
 
@@ -154,7 +154,7 @@ always p s = withSize $ \n -> toStop (p s) ||| p s ||| weight (fromIntegral n) (
 
 data FailingAction s
   = ErrorFail String
-  | forall a. (Typeable a, Eq (Action s a)) => ActionFail (ActionWithPolarity s a)
+  | forall a. (Typeable a, Eq (Action s Symbolic a)) => ActionFail (ActionWithPolarity s a)
 
 instance StateModel s => HasVariables (FailingAction s) where
   getAllVariables ErrorFail{} = mempty
@@ -329,7 +329,7 @@ usedVariables = go initialAnnotatedState
 -- properties at controlled times, so they are likely to fail if
 -- invoked at other times.
 class StateModel s => DynLogicModel s where
-  restricted :: Action s a -> Bool
+  restricted :: Action s Symbolic a -> Bool
   restricted _ = False
 
 restrictedPolar :: DynLogicModel s => ActionWithPolarity s a -> Bool
@@ -392,7 +392,7 @@ withDLScriptPrefix f k test =
 
 -- | Validate generated test case.
 --
--- Test case generation does not always produce a valid test case. In
+-- Test case Symbolic does not always produce a valid test case. In
 -- some cases, we did not find a suitable test case matching some
 -- `DynFormula` and we are `Stuck`, hence we want to discard the test
 -- case and start over ; in other cases we found a genuine issue with
diff --git a/quickcheck-dynamic/src/Test/QuickCheck/Extras.hs b/quickcheck-dynamic/src/Test/QuickCheck/Extras.hs
index ea5b51c7..a11e0806 100644
--- a/quickcheck-dynamic/src/Test/QuickCheck/Extras.hs
+++ b/quickcheck-dynamic/src/Test/QuickCheck/Extras.hs
@@ -2,6 +2,7 @@ module Test.QuickCheck.Extras where
 
 import Control.Monad.Reader
 import Control.Monad.State
+import Test.QuickCheck
 import Test.QuickCheck.Monadic
 
 runPropertyStateT :: Monad m => PropertyM (StateT s m) a -> s -> PropertyM m (a, s)
@@ -13,3 +14,7 @@ runPropertyReaderT :: Monad m => PropertyM (ReaderT e m) a -> e -> PropertyM m a
 runPropertyReaderT p e = MkPropertyM $ \k -> do
   m <- unPropertyM p $ fmap lift . k
   return $ runReaderT m e
+
+-- | Lifts a plain property into a monadic property.
+liftProperty :: Monad m => Property -> PropertyM m ()
+liftProperty prop = MkPropertyM (\k -> fmap (prop .&&.) <$> k ())
diff --git a/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs b/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs
index ccb7360d..1679b46b 100644
--- a/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs
+++ b/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs
@@ -11,7 +11,6 @@ module Test.QuickCheck.StateModel (
   module Test.QuickCheck.StateModel.Variables,
   StateModel (..),
   RunModel (..),
-  PostconditionM (..),
   WithUsedVars (..),
   Annotated (..),
   Step (..),
@@ -25,8 +24,6 @@ module Test.QuickCheck.StateModel (
   Env,
   Generic,
   IsPerformResult,
-  monitorPost,
-  counterexamplePost,
   stateAfter,
   runActions,
   lookUpVar,
@@ -40,16 +37,15 @@ module Test.QuickCheck.StateModel (
 ) where
 
 import Control.Monad
-import Control.Monad.Reader
-import Control.Monad.Writer (WriterT, runWriterT, tell)
 import Data.Data
+import Data.Kind (Type)
 import Data.List
-import Data.Monoid (Endo (..))
 import Data.Set qualified as Set
 import Data.Void
 import GHC.Generics
 import Test.QuickCheck as QC
 import Test.QuickCheck.DynamicLogic.SmartShrinking
+import Test.QuickCheck.Extras (liftProperty)
 import Test.QuickCheck.Monadic
 import Test.QuickCheck.StateModel.Variables
 
@@ -78,10 +74,10 @@ import Test.QuickCheck.StateModel.Variables
 --    a negative action one can define `failureNextState` - but it is generally recommended to let this be
 --    as simple an action as possible.
 class
-  ( forall a. Show (Action state a)
-  , forall a. HasVariables (Action state a)
-  , Show state
-  , HasVariables state
+  ( forall a. Show (Action state Symbolic a)
+  , forall a. HasVariables (Action state Symbolic a)
+  , Show (state Symbolic)
+  , HasVariables (state Symbolic)
   ) =>
   StateModel state
   where
@@ -93,14 +89,17 @@ class
   --
   -- @
   --   data Action RegState a where
-  --     Spawn      ::                           Action RegState ThreadId
-  --     Register   :: String -> Var ThreadId -> Action RegState ()
-  --     KillThread :: Var ThreadId           -> Action RegState ()
+  --     Spawn      ::                                 Action RegState phase ThreadId
+  --     Register   :: String -> Var phase ThreadId -> Action RegState phase ()
+  --     KillThread :: Var phase ThreadId           -> Action RegState phase ()
   -- @
   --
   -- The @Spawn@ action should produce a @ThreadId@, whereas the @KillThread@ action does not return
   -- anything.
-  data Action state a
+  --
+  -- Note that the @phase@ type parameter should be given to any @'Var'@ inside
+  -- the actions.
+  data Action (state :: Phase -> Type) (phase :: Phase) a
 
   -- | The type of errors that actions can throw. If this is defined as anything
   -- other than `Void` `perform` is required to return `Either (Error state) a`
@@ -115,48 +114,55 @@ class
   --
   -- Default implementation uses a poor-man's string manipulation method to extract the
   -- constructor name from the value.
-  actionName :: Action state a -> String
+  actionName :: Action state Symbolic a -> String
   actionName = head . words . show
 
   -- | Generator for `Action` depending on `state`.
-  arbitraryAction :: VarContext -> state -> Gen (Any (Action state))
+  arbitraryAction :: VarContext -> state Symbolic -> Gen (Any (Action state Symbolic))
 
   -- | Shrinker for `Action`.
   -- Defaults to no-op but as usual, defining a good shrinker greatly enhances the usefulness
   -- of property-based testing.
-  shrinkAction :: Typeable a => VarContext -> state -> Action state a -> [Any (Action state)]
+  shrinkAction :: Typeable a => VarContext -> state Symbolic -> Action state Symbolic a -> [Any (Action state Symbolic)]
   shrinkAction _ _ _ = []
 
   -- | Initial state of generated traces.
-  initialState :: state
+  --
+  -- Note that this function should be able to generate both the 'Symbolic' and
+  -- 'Dynamic' initial states.
+  initialState :: state phase
 
   -- | Transition function for the model.
-  -- The `Var a` parameter is useful to keep reference to actual value of type `a` produced
-  -- by `perform`ing the `Action` inside the `state` so that further actions can use `Lookup`
-  -- to retrieve that data. This allows the model to be ignorant of those values yet maintain
-  -- some references that can be compared and looked for.
-  nextState :: Typeable a => state -> Action state a -> Var a -> state
+  -- The `Var phase a` parameter is useful to keep reference to actual value of
+  -- type `a` produced by `perform`ing the `Action` inside the `state` so that
+  -- further actions can retrieve that data. This allows the model to be
+  -- ignorant of those values yet maintain some references that can be compared
+  -- and looked for.
+  --
+  -- Should you need some basic instances for the variable such as @Eq@, @Ord@,
+  -- or @Show@, the @'SingI'@ constraint allows you to concretize the phase.
+  nextState :: (SingI phase, Typeable a) => state phase -> Action state phase a -> Var phase a -> state phase
   nextState s _ _ = s
 
   -- | Transition function for negative actions. Note that most negative testing applications
   -- should not require an implementation of this function!
-  failureNextState :: Typeable a => state -> Action state a -> state
+  failureNextState :: Typeable a => state phase -> Action state phase a -> state phase
   failureNextState s _ = s
 
   -- | Precondition for filtering generated `Action`.
   -- This function is applied before the action is performed, it is useful to refine generators that
   -- can produce more values than are useful.
-  precondition :: state -> Action state a -> Bool
+  precondition :: state Symbolic -> Action state Symbolic a -> Bool
   precondition _ _ = True
 
   -- | Precondition for filtering an `Action` that can meaningfully run but is supposed to fail.
   -- An action will run as a _negative_ action if the `precondition` fails and `validFailingAction` succeeds.
-  -- A negative action should have _no effect_ on the model state. This may not be desierable in all
+  -- A negative action should have _no effect_ on the model state. This may not be desirable in all
   -- situations - in which case one can override this semantics for book-keeping in `failureNextState`.
-  validFailingAction :: state -> Action state a -> Bool
+  validFailingAction :: state Symbolic -> Action state Symbolic a -> Bool
   validFailingAction _ _ = False
 
-deriving instance (forall a. Show (Action state a)) => Show (Any (Action state))
+deriving instance (forall a. Show (Action state Symbolic a)) => Show (Any (Action state Symbolic))
 
 -- | The result required of `perform` depending on the `Error` type
 -- of a state model. If there are no errors, `Error state = Void`, and
@@ -174,30 +180,7 @@ instance {-# OVERLAPPING #-} IsPerformResult Void a where
 instance {-# OVERLAPPABLE #-} (PerformResult e a ~ Either e a) => IsPerformResult e a where
   performResultToEither = id
 
-newtype PostconditionM m a = PostconditionM {runPost :: WriterT (Endo Property, Endo Property) m a}
-  deriving (Functor, Applicative, Monad)
-
-instance MonadTrans PostconditionM where
-  lift = PostconditionM . lift
-
-evaluatePostCondition :: Monad m => PostconditionM m Bool -> PropertyM m ()
-evaluatePostCondition post = do
-  (b, (Endo mon, Endo onFail)) <- run . runWriterT . runPost $ post
-  monitor mon
-  unless b $ monitor onFail
-  assert b
-
--- | Apply the property transformation to the property after evaluating
--- the postcondition. Useful for collecting statistics while avoiding
--- duplication between `monitoring` and `postcondition`.
-monitorPost :: Monad m => (Property -> Property) -> PostconditionM m ()
-monitorPost m = PostconditionM $ tell (Endo m, mempty)
-
--- | Acts as `Test.QuickCheck.counterexample` if the postcondition fails.
-counterexamplePost :: Monad m => String -> PostconditionM m ()
-counterexamplePost c = PostconditionM $ tell (mempty, Endo $ counterexample c)
-
-class (forall a. Show (Action state a), Monad m) => RunModel state m where
+class (forall a. Show (Action state Dynamic a), Monad m) => RunModel state m where
   -- | Perform an `Action` in some `state` in the `Monad` `m`.  This
   -- is the function that's used to exercise the actual stateful
   -- implementation, usually through various side-effects as permitted
@@ -208,57 +191,65 @@ class (forall a. Show (Action state a), Monad m) => RunModel state m where
   --
   -- The `Lookup` parameter provides an /environment/ to lookup `Var
   -- a` instances from previous steps.
-  perform :: Typeable a => state -> Action state a -> LookUp -> m (PerformResult (Error state) a)
+  perform :: Typeable a => Action state Dynamic a -> m (PerformResult (Error state) a)
+
+  -- | Convert a symbolic action to a dynamic one by means of the 'LookUp'
+  -- function.
+  toDynAction :: Action state Symbolic a -> LookUp -> Action state Dynamic a
 
   -- | Postcondition on the `a` value produced at some step.
   -- The result is `assert`ed and will make the property fail should it be `False`. This is useful
   -- to check the implementation produces expected values.
-  postcondition :: (state, state) -> Action state a -> LookUp -> a -> PostconditionM m Bool
-  postcondition _ _ _ _ = pure True
+  postcondition :: (state Dynamic, state Dynamic) -> Action state Dynamic a -> a -> Property
+  postcondition _ _ _ = property True
 
   -- | Postcondition on the result of running a _negative_ `Action`.
-  -- The result is `assert`ed and will make the property fail should it be `False`. This is useful
+  -- The resulting property is exercised when running the SUT. This is useful
   -- to check the implementation produces e.g. the expected errors or to check that the SUT hasn't
   -- been updated during the execution of the negative action.
-  postconditionOnFailure :: (state, state) -> Action state a -> LookUp -> Either (Error state) a -> PostconditionM m Bool
-  postconditionOnFailure _ _ _ _ = pure True
+  postconditionOnFailure :: (state Dynamic, state Dynamic) -> Action state Dynamic a -> Either (Error state) a -> Property
+  postconditionOnFailure _ _ _ = property True
 
-  -- | Allows the user to attach additional information to the `Property` at each step of the process.
+  -- | Allows the user to attach additional information to the `Property` after each succesful run of an action.
   -- This function is given the full transition that's been executed, including the start and ending
   -- `state`, the `Action`, the current environment to `Lookup` and the value produced by `perform`
   -- while executing this step.
-  monitoring :: (state, state) -> Action state a -> LookUp -> Either (Error state) a -> Property -> Property
-  monitoring _ _ _ _ prop = prop
+  --
+  -- This is just a convenience as this information can as well be attached
+  -- to the property defined in @'postcondition'@ or @'postconditonOnFailure'@
+  -- with the same result.
+  monitoring :: (state Dynamic, state Dynamic) -> Action state Dynamic a -> Either (Error state) a -> Property -> Property
+  monitoring _ _ _ prop = prop
 
   -- | Allows the user to attach additional information to the `Property` if a positive action fails.
-  monitoringFailure :: state -> Action state a -> LookUp -> Error state -> Property -> Property
-  monitoringFailure _ _ _ _ prop = prop
+  monitoringFailure :: state Dynamic -> Action state Dynamic a -> Error state -> Property -> Property
+  monitoringFailure _ _ _ prop = prop
 
-type LookUp = forall a. Typeable a => Var a -> a
+type LookUp = forall a. Typeable a => Var Symbolic a -> Var Dynamic a
 
 type Env = [EnvEntry]
 
 data EnvEntry where
-  (:==) :: Typeable a => Var a -> a -> EnvEntry
+  (:==) :: Typeable a => Var Symbolic a -> Var Dynamic a -> EnvEntry
 
 infix 5 :==
 
-pattern (:=?) :: forall a. Typeable a => Var a -> a -> EnvEntry
+pattern (:=?) :: forall a. Typeable a => Var Symbolic a -> Var Dynamic a -> EnvEntry
 pattern v :=? val <- (viewAtType -> Just (v, val))
 
-viewAtType :: forall a. Typeable a => EnvEntry -> Maybe (Var a, a)
-viewAtType ((v :: Var b) :== val)
+viewAtType :: forall a. Typeable a => EnvEntry -> Maybe (Var Symbolic a, Var Dynamic a)
+viewAtType ((v :: Var Symbolic b) :== val)
   | Just Refl <- eqT @a @b = Just (v, val)
   | otherwise = Nothing
 
-lookUpVarMaybe :: forall a. Typeable a => Env -> Var a -> Maybe a
+lookUpVarMaybe :: forall a. Typeable a => Env -> Var Symbolic a -> Maybe (Var Dynamic a)
 lookUpVarMaybe [] _ = Nothing
-lookUpVarMaybe (((v' :: Var b) :== a) : env) v =
+lookUpVarMaybe (((v' :: Var Symbolic b) :== a) : env) v =
   case eqT @a @b of
     Just Refl | v == v' -> Just a
     _ -> lookUpVarMaybe env v
 
-lookUpVar :: Typeable a => Env -> Var a -> a
+lookUpVar :: Typeable a => Env -> Var Symbolic a -> Var Dynamic a
 lookUpVar env v = case lookUpVarMaybe env v of
   Nothing -> error $ "Variable " ++ show v ++ " is not bound at type " ++ show (typeRep v) ++ "!"
   Just a -> a
@@ -274,27 +265,27 @@ instance Show Polarity where
   show PosPolarity = "+"
   show NegPolarity = "-"
 
-data ActionWithPolarity state a = Eq (Action state a) =>
+data ActionWithPolarity state a = Eq (Action state Symbolic a) =>
   ActionWithPolarity
-  { polarAction :: Action state a
+  { polarAction :: Action state Symbolic a
   , polarity :: Polarity
   }
 
-instance HasVariables (Action state a) => HasVariables (ActionWithPolarity state a) where
+instance HasVariables (Action state Symbolic a) => HasVariables (ActionWithPolarity state a) where
   getAllVariables = getAllVariables . polarAction
 
-deriving instance Eq (Action state a) => Eq (ActionWithPolarity state a)
+deriving instance Eq (Action state Symbolic a) => Eq (ActionWithPolarity state a)
 
 data Step state where
   (:=)
-    :: (Typeable a, Eq (Action state a), Show (Action state a))
-    => Var a
+    :: (Typeable a, Eq (Action state Symbolic a), Show (Action state Symbolic a))
+    => Var Symbolic a
     -> ActionWithPolarity state a
     -> Step state
 
 infix 5 :=
 
-instance (forall a. HasVariables (Action state a)) => HasVariables (Step state) where
+instance (forall a. HasVariables (Action state Symbolic a)) => HasVariables (Step state) where
   getAllVariables (var := act) = Set.insert (Some var) $ getAllVariables (polarAction act)
 
 funName :: Polarity -> String
@@ -407,18 +398,18 @@ instance forall state. StateModel state => Arbitrary (Actions state) where
 
 -- Running state models
 
-data Annotated state = Metadata
+data Annotated (state :: Phase -> Type) = Metadata
   { vars :: VarContext
-  , underlyingState :: state
+  , underlyingState :: state Symbolic
   }
 
-instance Show state => Show (Annotated state) where
+instance Show (state Symbolic) => Show (Annotated state) where
   show (Metadata ctx s) = show ctx ++ " |- " ++ show s
 
 initialAnnotatedState :: StateModel state => Annotated state
 initialAnnotatedState = Metadata mempty initialState
 
-actionWithPolarity :: (StateModel state, Eq (Action state a)) => Annotated state -> Action state a -> ActionWithPolarity state a
+actionWithPolarity :: (StateModel state, Eq (Action state Symbolic a)) => Annotated state -> Action state Symbolic a -> ActionWithPolarity state a
 actionWithPolarity s a =
   let p
         | precondition (underlyingState s) a = PosPolarity
@@ -438,7 +429,7 @@ computeNextState
   :: (StateModel state, Typeable a)
   => Annotated state
   -> ActionWithPolarity state a
-  -> Var a
+  -> Var Symbolic a
   -> Annotated state
 computeNextState s a v
   | polarity a == PosPolarity = Metadata (extendContext (vars s) v) (nextState (underlyingState s) (polarAction a) v)
@@ -492,13 +483,13 @@ runActions
      , forall a. IsPerformResult e a
      )
   => Actions state
-  -> PropertyM m (Annotated state, Env)
+  -> PropertyM m (Annotated state, state Dynamic, Env)
 runActions (Actions_ rejected (Smart _ actions)) = do
-  (finalState, env) <- runSteps initialAnnotatedState [] actions
+  (finalState, finalDynState, env) <- runSteps (initialAnnotatedState, initialState) [] actions
   unless (null rejected) $
     monitor $
       tabulate "Actions rejected by precondition" rejected
-  return (finalState, env)
+  return (finalState, finalDynState, env)
 
 -- | Core function to execute a sequence of `Step` given some initial `Env`ironment
 -- and `Annotated` state.
@@ -509,14 +500,14 @@ runSteps
      , e ~ Error state
      , forall a. IsPerformResult e a
      )
-  => Annotated state
+  => (Annotated state, state Dynamic)
   -> Env
   -> [Step state]
-  -> PropertyM m (Annotated state, Env)
-runSteps s env [] = return (s, reverse env)
-runSteps s env ((v := act) : as) = do
+  -> PropertyM m (Annotated state, state Dynamic, Env)
+runSteps (s, sd) env [] = return (s, sd, reverse env)
+runSteps (s, sd) env (((v :: Var Symbolic a) := act) : as) = do
   pre $ computePrecondition s act
-  ret <- run $ performResultToEither <$> perform (underlyingState s) action (lookUpVar env)
+  ret <- run $ performResultToEither <$> perform action'
   let name = show polar ++ actionName action
   monitor $ tabulate "Actions" [name]
   monitor $ tabulate "Action polarity" [show polar]
@@ -524,51 +515,48 @@ runSteps s env ((v := act) : as) = do
     (PosPolarity, Left err) ->
       positiveActionFailed err
     (PosPolarity, Right val) -> do
-      (s', env') <- positiveActionSucceeded ret val
-      runSteps s' env' as
+      (s', sd', env') <- positiveActionSucceeded ret val
+      runSteps (s', sd') env' as
     (NegPolarity, _) -> do
-      (s', env') <- negativeActionResult ret
-      runSteps s' env' as
+      (s', sd', env') <- negativeActionResult ret
+      runSteps (s', sd') env' as
   where
     polar = polarity act
 
     action = polarAction act
+    action' = toDynAction @state @m action (lookUpVar env)
 
     positiveActionFailed err = do
       monitor $
         monitoringFailure @state @m
-          (underlyingState s)
-          action
-          (lookUpVar env)
+          sd
+          action'
           err
       stop False
 
     positiveActionSucceeded ret val = do
-      (s', env', stateTransition) <- computeNewState ret
-      evaluatePostCondition $
-        postcondition
-          stateTransition
-          action
-          (lookUpVar env)
+      (s', sd', env') <- computeNewState ret
+      liftProperty $
+        postcondition @state @m
+          (sd, sd')
+          action'
           val
-      pure (s', env')
+      pure (s', sd', env')
 
     negativeActionResult ret = do
-      (s', env', stateTransition) <- computeNewState ret
-      evaluatePostCondition $
-        postconditionOnFailure
-          stateTransition
-          action
-          (lookUpVar env)
+      (s', sd', env') <- computeNewState ret
+      liftProperty $
+        postconditionOnFailure @state @m
+          (sd, sd')
+          action'
           ret
-      pure (s', env')
+      pure (s', sd', env')
 
     computeNewState ret = do
       let var = unsafeCoerceVar v
           s' = computeNextState s act var
-          env'
-            | Right val <- ret = (var :== val) : env
-            | otherwise = env
-          stateTransition = (underlyingState s, underlyingState s')
-      monitor $ monitoring @state @m stateTransition action (lookUpVar env') ret
-      pure (s', env', stateTransition)
+          (env', sd')
+            | Right val <- ret = ((var :== DynamicVar val) : env, nextState sd action' (DynamicVar val))
+            | otherwise = (env, failureNextState sd action')
+      monitor $ monitoring @state @m (sd, sd') action' ret
+      pure (s', sd', env')
diff --git a/quickcheck-dynamic/src/Test/QuickCheck/StateModel/Variables.hs b/quickcheck-dynamic/src/Test/QuickCheck/StateModel/Variables.hs
index f2cb825d..0d4641c1 100644
--- a/quickcheck-dynamic/src/Test/QuickCheck/StateModel/Variables.hs
+++ b/quickcheck-dynamic/src/Test/QuickCheck/StateModel/Variables.hs
@@ -3,10 +3,11 @@
 {-# LANGUAGE UndecidableInstances #-}
 
 module Test.QuickCheck.StateModel.Variables (
-  Var,
   Any (..),
+  Var (..),
   HasVariables (..),
   HasNoVariables (..),
+  SymbolicVar,
   VarContext,
   mkVar,
   ctxAtType,
@@ -18,6 +19,14 @@ module Test.QuickCheck.StateModel.Variables (
   isEmptyCtx,
   unsafeCoerceVar,
   unsafeNextVarIndex,
+
+  -- * Phases
+  Phase (..),
+
+  -- ** Singletons
+  SingI,
+  SPhase (SDynamic, SSymbolic),
+  sing,
 ) where
 
 import Data.Data
@@ -28,31 +37,68 @@ import Data.Map qualified as Map
 import Data.Ord
 import Data.Set (Set)
 import Data.Set qualified as Set
+import Data.Singletons
 import GHC.Generics
 import GHC.TypeLits
 import GHC.Word
 import Test.QuickCheck as QC
 
+-- | The phases of testing
+--
+-- During generation of tests, we will use 'Symbolic' actions and variables. These variables
+-- represent the result of performing a call and should not be inspected.
+--
+-- During test execution, we wil use 'Dynamic' actions and variables, where these
+-- references are concretized in real values.
+data Phase = Symbolic | Dynamic
+
+data SPhase :: Phase -> Type where
+  SDynamic :: SPhase 'Dynamic
+  SSymbolic :: SPhase 'Symbolic
+
+type instance Sing @Phase = SPhase
+
+instance SingI Dynamic where
+  sing = SDynamic
+
+instance SingI Symbolic where
+  sing = SSymbolic
+
 -- | A symbolic variable for a value of type `a`
-newtype Var a = Var Int
+newtype SymbolicVar a = Var Int
   deriving (Eq, Ord, Typeable, Data)
 
-mkVar :: Int -> Var a
-mkVar = Var
+-- | A variable that will be 'Symbolic' or 'Dynamic'
+data Var phase a where
+  SymbolicVar :: SymbolicVar a -> Var Symbolic a
+  DynamicVar :: a -> Var Dynamic a
+
+deriving instance Eq (Var Symbolic a)
+deriving instance Ord (Var Symbolic a)
+deriving instance Show (Var Symbolic a)
+
+deriving instance Eq a => Eq (Var Dynamic a)
+deriving instance Ord a => Ord (Var Dynamic a)
+deriving instance Show a => Show (Var Dynamic a)
 
-instance Show (Var a) where
+mkVar :: Int -> Var Symbolic a
+mkVar = SymbolicVar . Var
+
+instance Show (SymbolicVar a) where
   show (Var i) = "var" ++ show i
 
 -- | This type class gives you a way to get all the symbolic variables that
 -- appear in a value.
 class HasVariables a where
-  getAllVariables :: a -> Set (Any Var)
+  getAllVariables :: a -> Set (Any (Var Symbolic))
 
 instance HasVariables a => HasVariables (Smart a) where
   getAllVariables (Smart _ a) = getAllVariables a
 
-instance Typeable a => HasVariables (Var a) where
+instance Typeable a => HasVariables (Var Symbolic a) where
   getAllVariables = Set.singleton . Some
+instance Typeable a => HasVariables (SymbolicVar a) where
+  getAllVariables = Set.singleton . Some . SymbolicVar
 
 instance (HasVariables k, HasVariables v) => HasVariables (Map k v) where
   getAllVariables = getAllVariables . Map.toList
@@ -94,22 +140,24 @@ instance (forall a. Ord (f a)) => Ord (Any f) where
       Just Refl -> compare a a'
       Nothing -> compare (typeRep a) (typeRep a')
 
-newtype VarContext = VarCtx (Set (Any Var))
-  deriving (Semigroup, Monoid) via Set (Any Var)
+newtype VarContext = VarCtx (Set (Any (Var Symbolic)))
+  deriving (Semigroup, Monoid) via Set (Any (Var Symbolic))
 
 instance Show VarContext where
   show (VarCtx vs) =
     "[" ++ intercalate ", " (map showBinding . sortBy (comparing getIdx) $ Set.toList vs) ++ "]"
     where
-      getIdx (Some (Var i)) = i
-      showBinding :: Any Var -> String
+      getIdx :: Any (Var Symbolic) -> Int
+      getIdx (Some (SymbolicVar (Var i))) = i
+
+      showBinding :: Any (Var Symbolic) -> String
       -- The use of typeRep here is on purpose to avoid printing `Var` unnecessarily.
       showBinding (Some v) = show v ++ " :: " ++ show (typeRep v)
 
 isEmptyCtx :: VarContext -> Bool
 isEmptyCtx (VarCtx ctx) = null ctx
 
-isWellTyped :: Typeable a => Var a -> VarContext -> Bool
+isWellTyped :: Typeable a => Var Symbolic a -> VarContext -> Bool
 isWellTyped v (VarCtx ctx) = not (null ctx) && Some v `Set.member` ctx
 
 -- TODO: check the invariant that no variable index is used
@@ -118,26 +166,26 @@ isWellTyped v (VarCtx ctx) = not (null ctx) && Some v `Set.member` ctx
 -- cause an issue, but it might be good practise to crash
 -- if the invariant is violated anyway as it is evidence that
 -- something is horribly broken at the use site).
-extendContext :: Typeable a => VarContext -> Var a -> VarContext
+extendContext :: Typeable a => VarContext -> Var Symbolic a -> VarContext
 extendContext (VarCtx ctx) v = VarCtx $ Set.insert (Some v) ctx
 
 allVariables :: HasVariables a => a -> VarContext
 allVariables = VarCtx . getAllVariables
 
-ctxAtType :: Typeable a => VarContext -> [Var a]
+ctxAtType :: Typeable a => VarContext -> [Var Symbolic a]
 ctxAtType (VarCtx vs) = [v | Some (cast -> Just v) <- Set.toList vs]
 
-arbitraryVar :: Typeable a => VarContext -> Gen (Var a)
+arbitraryVar :: Typeable a => VarContext -> Gen (Var Symbolic a)
 arbitraryVar = elements . ctxAtType
 
-shrinkVar :: Typeable a => VarContext -> Var a -> [Var a]
+shrinkVar :: Typeable a => VarContext -> Var Symbolic a -> [Var Symbolic a]
 shrinkVar ctx v = filter (< v) $ ctxAtType ctx
 
-unsafeCoerceVar :: Var a -> Var b
-unsafeCoerceVar (Var i) = Var i
+unsafeCoerceVar :: Var Symbolic a -> Var Symbolic b
+unsafeCoerceVar (SymbolicVar (Var i)) = SymbolicVar (Var i)
 
 unsafeNextVarIndex :: VarContext -> Int
-unsafeNextVarIndex (VarCtx vs) = 1 + maximum (0 : [i | Some (Var i) <- Set.toList vs])
+unsafeNextVarIndex (VarCtx vs) = 1 + maximum (0 : [i | Some (SymbolicVar (Var i)) <- Set.toList vs])
 
 -- NOTE: This trick is taken from this blog post:
 -- https://blog.csongor.co.uk/report-stuck-families/
@@ -159,7 +207,7 @@ instance
   getAllVariables = genericGetAllVariables . from
 
 class GenericHasVariables f where
-  genericGetAllVariables :: f k -> Set (Any Var)
+  genericGetAllVariables :: f k -> Set (Any (Var Symbolic))
 
 instance GenericHasVariables f => GenericHasVariables (M1 i c f) where
   genericGetAllVariables = genericGetAllVariables . unM1
diff --git a/quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs b/quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs
index aa68c99b..9180fd0d 100644
--- a/quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs
+++ b/quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs
@@ -11,17 +11,17 @@ import Test.QuickCheck.StateModel
 
 -- A very simple model with a single action that always succeed in
 -- predictable way. This model is useful for testing the runtime.
-newtype SimpleCounter = SimpleCounter {count :: Int}
+newtype SimpleCounter (phase :: Phase) = SimpleCounter {count :: Int}
   deriving (Eq, Show, Generic)
 
-deriving instance Eq (Action SimpleCounter a)
-deriving instance Show (Action SimpleCounter a)
-instance HasVariables (Action SimpleCounter a) where
+deriving instance Eq (Action SimpleCounter phase a)
+deriving instance Show (Action SimpleCounter phase a)
+instance HasVariables (Action SimpleCounter Symbolic a) where
   getAllVariables _ = mempty
 
 instance StateModel SimpleCounter where
-  data Action SimpleCounter a where
-    IncSimple :: Action SimpleCounter Int
+  data Action SimpleCounter phase a where
+    IncSimple :: Action SimpleCounter phase Int
 
   arbitraryAction _ _ = pure $ Some IncSimple
 
@@ -30,23 +30,25 @@ instance StateModel SimpleCounter where
   nextState SimpleCounter{count} IncSimple _ = SimpleCounter (count + 1)
 
 instance RunModel SimpleCounter (ReaderT (IORef Int) IO) where
-  perform _ IncSimple _ = do
+  perform IncSimple = do
     ref <- ask
     lift $ atomicModifyIORef' ref (\count -> (succ count, count))
 
+  toDynAction IncSimple _ = IncSimple
+
 -- A very simple model with a single action whose postcondition fails in a
 -- predictable way. This model is useful for testing the runtime.
-newtype FailingCounter = FailingCounter {failingCount :: Int}
+newtype FailingCounter (phase :: Phase) = FailingCounter {failingCount :: Int}
   deriving (Eq, Show, Generic)
 
-deriving instance Eq (Action FailingCounter a)
-deriving instance Show (Action FailingCounter a)
-instance HasVariables (Action FailingCounter a) where
+deriving instance Eq (Action FailingCounter Symbolic a)
+deriving instance Show (Action FailingCounter phase a)
+instance HasVariables (Action FailingCounter Symbolic a) where
   getAllVariables _ = mempty
 
 instance StateModel FailingCounter where
-  data Action FailingCounter a where
-    Inc' :: Action FailingCounter Int
+  data Action FailingCounter phase a where
+    Inc' :: Action FailingCounter phase Int
 
   arbitraryAction _ _ = pure $ Some Inc'
 
@@ -55,25 +57,27 @@ instance StateModel FailingCounter where
   nextState FailingCounter{failingCount} Inc' _ = FailingCounter (failingCount + 1)
 
 instance RunModel FailingCounter (ReaderT (IORef Int) IO) where
-  perform _ Inc' _ = do
+  perform Inc' = do
     ref <- ask
     lift $ atomicModifyIORef' ref (\count -> (succ count, count))
 
-  postcondition (_, FailingCounter{failingCount}) _ _ _ = pure $ failingCount < 4
+  toDynAction Inc' _ = Inc'
+
+  postcondition (_, FailingCounter{failingCount}) _ _ = property $ failingCount < 4
 
 -- A generic but simple counter model
-data Counter = Counter Int
+data Counter (phase :: Phase) = Counter Int
   deriving (Show, Generic)
 
-deriving instance Show (Action Counter a)
-deriving instance Eq (Action Counter a)
-instance HasVariables (Action Counter a) where
+deriving instance Show (Action Counter phase a)
+deriving instance Eq (Action Counter phase a)
+instance HasVariables (Action Counter Symbolic a) where
   getAllVariables _ = mempty
 
 instance StateModel Counter where
-  data Action Counter a where
-    Inc :: Action Counter ()
-    Reset :: Action Counter Int
+  data Action Counter phase a where
+    Inc :: Action Counter phase ()
+    Reset :: Action Counter phase Int
 
   initialState = Counter 0
 
@@ -83,15 +87,18 @@ instance StateModel Counter where
   nextState _ Reset _ = Counter 0
 
 instance RunModel Counter (ReaderT (IORef Int) IO) where
-  perform _ Inc _ = do
+  perform Inc = do
     ref <- ask
     lift $ modifyIORef ref succ
-  perform _ Reset _ = do
+  perform Reset = do
     ref <- ask
     lift $ do
       n <- readIORef ref
       writeIORef ref 0
       pure n
 
-  postcondition (Counter n, _) Reset _ res = pure $ n == res
-  postcondition _ _ _ _ = pure True
+  toDynAction Inc _ = Inc
+  toDynAction Reset _ = Reset
+
+  postcondition (Counter n, _) Reset res = n === res
+  postcondition _ _ _ = property True
diff --git a/quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs b/quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs
index a723ace6..08799daa 100644
--- a/quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs
+++ b/quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE UndecidableInstances #-}
+
 module Spec.DynamicLogic.RegistryModel where
 
 import Control.Concurrent
@@ -22,27 +24,30 @@ import Test.QuickCheck.DynamicLogic
 import Test.QuickCheck.Extras
 import Test.QuickCheck.StateModel
 
-data RegState = RegState
-  { regs :: Map String (Var ThreadId)
-  , dead :: [Var ThreadId]
+data RegState (phase :: Phase) = RegState
+  { regs :: Map String (Var phase ThreadId)
+  , dead :: [Var phase ThreadId]
   }
-  deriving (Show, Generic)
+  deriving (Generic)
+
+deriving instance Show (RegState Symbolic)
+deriving instance Show (RegState Dynamic)
 
-deriving instance Show (Action RegState a)
-deriving instance Eq (Action RegState a)
+deriving instance Show (Var phase ThreadId) => Show (Action RegState phase a)
+deriving instance Eq (Var phase ThreadId) => Eq (Action RegState phase a)
 
-instance HasVariables (Action RegState a) where
+instance HasVariables (Action RegState Symbolic a) where
   getAllVariables (Register _ v) = getAllVariables v
   getAllVariables (KillThread v) = getAllVariables v
   getAllVariables _ = mempty
 
 instance StateModel RegState where
-  data Action RegState a where
-    Spawn :: Action RegState ThreadId
-    WhereIs :: String -> Action RegState (Maybe ThreadId)
-    Register :: String -> Var ThreadId -> Action RegState ()
-    Unregister :: String -> Action RegState ()
-    KillThread :: Var ThreadId -> Action RegState ()
+  data Action RegState phase a where
+    Spawn :: Action RegState phase ThreadId
+    WhereIs :: String -> Action RegState phase (Maybe ThreadId)
+    Register :: String -> Var phase ThreadId -> Action RegState phase ()
+    Unregister :: String -> Action RegState phase ()
+    KillThread :: Var phase ThreadId -> Action RegState phase ()
 
   type Error RegState = SomeException
 
@@ -100,54 +105,59 @@ instance StateModel RegState where
   nextState s (Register name tid) _step = s{regs = Map.insert name tid (regs s)}
   nextState s (Unregister name) _step =
     s{regs = Map.delete name (regs s)}
-  nextState s (KillThread tid) _ =
+  nextState s (KillThread tid :: Action RegState phase a) _ =
     s
       { dead = tid : dead s
-      , regs = Map.filter (/= tid) (regs s)
+      , regs = case sing @phase of
+          SDynamic -> Map.filter (/= tid) (regs s)
+          SSymbolic -> Map.filter (/= tid) (regs s)
       }
   nextState s WhereIs{} _ = s
 
 type RegM = ReaderT Registry IO
 
 instance RunModel RegState RegM where
-  perform _ Spawn _ = do
+  perform Spawn = do
     tid <- lift $ forkIO (threadDelay 10000000)
     pure $ Right tid
-  perform _ (Register name tid) env = do
+  perform (Register name (DynamicVar tid)) = do
     reg <- ask
-    lift $ try $ register reg name (env tid)
-  perform _ (Unregister name) _ = do
+    lift $ try $ register reg name tid
+  perform (Unregister name) = do
     reg <- ask
     lift $ try $ unregister reg name
-  perform _ (WhereIs name) _ = do
+  perform (WhereIs name) = do
     reg <- ask
     res <- lift $ whereis reg name
     pure $ Right res
-  perform _ (KillThread tid) env = do
-    lift $ killThread (env tid)
+  perform (KillThread (DynamicVar tid)) = do
+    lift $ killThread tid
     lift $ threadDelay 100
     pure $ Right ()
 
-  postcondition (s, _) (WhereIs name) env mtid = do
-    pure $ (env <$> Map.lookup name (regs s)) == mtid
-  postcondition _ _ _ _ = pure True
+  toDynAction Spawn _ = Spawn
+  toDynAction (Register n v) l = Register n (l v)
+  toDynAction (Unregister n) _ = Unregister n
+  toDynAction (WhereIs n) _ = WhereIs n
+  toDynAction (KillThread v) l = KillThread (l v)
 
-  postconditionOnFailure (s, _) act@Register{} _ res = do
-    monitorPost $
-      tabulate
-        "Reason for -Register"
-        [why s act]
-    pure $ isLeft res
-  postconditionOnFailure _s _ _ _ = pure True
-
-  monitoring (_s, s') act@(showDictAction -> ShowDict) _ res =
-    counterexample (show res ++ " <- " ++ show act ++ "\n  -- State: " ++ show s')
+  postcondition (s, s') act@(WhereIs name) mtid =
+    counterexample (show mtid ++ " <- " ++ show act ++ "\n  -- State: " ++ show s')
       . tabulate "Registry size" [show $ Map.size (regs s')]
+      $ Map.lookup name (regs s) === fmap DynamicVar mtid
+  postcondition _ _ _ = property True
+
+  postconditionOnFailure (s, _) act@Register{} res =
+    tabulate
+      "Reason for -Register"
+      [why s act]
+      $ isLeft res
+  postconditionOnFailure _s _ _ = property True
 
 data ShowDict a where
   ShowDict :: Show a => ShowDict a
 
-showDictAction :: forall a. Action RegState a -> ShowDict a
+showDictAction :: forall a phase. Action RegState phase a -> ShowDict a
 showDictAction Spawn{} = ShowDict
 showDictAction WhereIs{} = ShowDict
 showDictAction Register{} = ShowDict
@@ -157,7 +167,7 @@ showDictAction KillThread{} = ShowDict
 instance DynLogicModel RegState where
   restricted _ = False
 
-why :: RegState -> Action RegState a -> String
+why :: RegState Dynamic -> Action RegState Dynamic a -> String
 why s (Register name tid) =
   unwords $
     ["name already registered" | name `Map.member` regs s]
@@ -168,10 +178,10 @@ why _ _ = "(impossible)"
 arbitraryName :: Gen String
 arbitraryName = elements allNames
 
-probablyRegistered :: RegState -> Gen String
+probablyRegistered :: RegState phase -> Gen String
 probablyRegistered s = oneof $ map pure (Map.keys $ regs s) ++ [arbitraryName]
 
-probablyUnregistered :: RegState -> Gen String
+probablyUnregistered :: RegState phase -> Gen String
 probablyUnregistered s = elements $ allNames ++ (allNames \\ Map.keys (regs s))
 
 shrinkName :: String -> [String]
@@ -193,7 +203,7 @@ propDL d = forAllDL d prop_Registry
 
 -- DL helpers
 
-unregisterNameAndTid :: String -> Var ThreadId -> DL RegState ()
+unregisterNameAndTid :: String -> Var Symbolic ThreadId -> DL RegState ()
 unregisterNameAndTid name tid = do
   s <- getModelStateDL
   sequence_
@@ -202,7 +212,7 @@ unregisterNameAndTid name tid = do
     , name' == name || tid' == tid
     ]
 
-unregisterTid :: Var ThreadId -> DL RegState ()
+unregisterTid :: Var Symbolic ThreadId -> DL RegState ()
 unregisterTid tid = do
   s <- getModelStateDL
   sequence_
@@ -211,18 +221,18 @@ unregisterTid tid = do
     , tid' == tid
     ]
 
-getAlive :: DL RegState [Var ThreadId]
+getAlive :: DL RegState [Var Symbolic ThreadId]
 getAlive = do
   s <- getModelStateDL
   ctx <- getVarContextDL
   pure $ ctxAtType @ThreadId ctx \\ dead s
 
-pickThread :: DL RegState (Var ThreadId)
+pickThread :: DL RegState (Var Symbolic ThreadId)
 pickThread = do
   tids <- ctxAtType @ThreadId <$> getVarContextDL
   forAllQ $ elementsQ tids
 
-pickAlive :: DL RegState (Var ThreadId)
+pickAlive :: DL RegState (Var Symbolic ThreadId)
 pickAlive = do
   alive <- getAlive
   forAllQ $ elementsQ alive
diff --git a/quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs b/quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs
index 12add896..46114ebf 100644
--- a/quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs
+++ b/quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs
@@ -12,6 +12,7 @@ import Test.QuickCheck.Extras (runPropertyReaderT)
 import Test.QuickCheck.Monadic (assert, monadicIO, monitor, pick)
 import Test.QuickCheck.StateModel (
   Actions,
+  Var (..),
   lookUpVarMaybe,
   mkVar,
   runActions,
@@ -55,14 +56,14 @@ prop_returnsFinalState :: Actions SimpleCounter -> Property
 prop_returnsFinalState actions@(Actions as) =
   monadicIO $ do
     ref <- lift $ newIORef (0 :: Int)
-    (s, _) <- runPropertyReaderT (runActions actions) ref
+    (s, _, _) <- runPropertyReaderT (runActions actions) ref
     assert $ count (underlyingState s) == length as
 
 prop_variablesIndicesAre1Based :: Actions SimpleCounter -> Property
 prop_variablesIndicesAre1Based actions@(Actions as) =
   noShrinking $ monadicIO $ do
     ref <- lift $ newIORef (0 :: Int)
-    (_, env) <- runPropertyReaderT (runActions actions) ref
+    (_, _, env) <- runPropertyReaderT (runActions actions) ref
     act <- pick $ choose (0, length as - 1)
     monitor $
       counterexample $
@@ -71,7 +72,7 @@ prop_variablesIndicesAre1Based actions@(Actions as) =
           , "Actions:  " <> show as
           , "Act:  " <> show act
           ]
-    assert $ null as || lookUpVarMaybe env (mkVar $ act + 1) == Just act
+    assert $ null as || lookUpVarMaybe env (mkVar $ act + 1) == Just (DynamicVar act)
 
 prop_failsOnPostcondition :: Actions FailingCounter -> Property
 prop_failsOnPostcondition actions =