From aaf0ef51a56c0bccc3fb0db6301850ad3c219c93 Mon Sep 17 00:00:00 2001
From: Georgy Lukyanov <mail@geo2a.info>
Date: Wed, 23 Oct 2024 12:25:36 +0200
Subject: [PATCH] 4059 ensures substitution (#4060)

Fixes https://github.com/runtimeverification/haskell-backend/issues/4059

This PR improves Booster's handling of substitutions.

## Summary

Substitutions are special predicates: equations where the LHS is a
variable, for example `VAR ==Int TERM`. See
`Booster.Syntax.Json.Internalise.mbSubstitution` for the exact
specification of what is considered to be a substitution.

This PR changes the `Pattern` type to explicitly carry these special
substitution predicates:

```diff
+type Substitution = Map Variable Term
+
 -- | A term (configuration) constrained by a number of predicates.
 data Pattern = Pattern
     { term :: Term
     , constraints :: !(Set Predicate)
+    , substitution :: Substitution
     , ceilConditions :: ![Ceil]
     }
     deriving stock (Eq, Ord, Show, Generic, Data)
```

Substitution may appear out of three places:
- sent in the request body
- ensured as a post condition of a rewrite rule
- **NOT IMPLEMENTED** learned from the branching condition --- this is
something that will be added as part of #4058

The first source is handled by the pattern internalisation code. The
second and third sources are different, as the pattern has already been
internalised. All this sources can also produce generic (i.e.
non-substitution) constrains that should be added into the `constrains`
set of a `Pattern`. Substitutions, when produces, should be applied to
the `term` of the `Pattern` and added to the `substitution` field. This
PR makes sure we use the same code path for separating substitutions
from generic predicates everywhere. We use
`Booster.Syntax.Json.Internalise.mbSubstitution.mkSubstitution` to take
care of cyclic, which are broken up, and duplicate bindings, which are
treated as constraints.

With these changes, we can harmonize many (but not all) specialisations
of the integrations test responses, i.e. we do not need many of the
`*.booster-dev` and `*.kore-rpc-dev` response files.

## Changes to pattern simplification code

As the `Pattern` type has changed, we must adapt the
`ApplyEquations.evaluatePattern` and `ApplyEquations.evaluatePattern'`
functions to:
- consider `substitutions` as known truth together with all other
constraints (that's what we did before)
- simplify the substitution

We achieve that by doing the following:
- convert the substitution into equalities and assume it as know truth
- when constructing the new, simplified pattern, use the same code as
when internalising a pattern to partition predicates into the
substitution and non-substitution ones

## Changes to rewrite rule application code

The `Pattern.Rewrite.applyRule` function has been changed to:
- consider `substiontion` as known truth together with all other
constraints (that's what we did before) when checking requires/ensures
- extract the substitution from the ensured conditions and add it to the
rewritten pattern

---------

Co-authored-by: github-actions <github-actions@github.com>
---
 booster/library/Booster/JsonRpc.hs            |  72 ++--
 booster/library/Booster/JsonRpc/Utils.hs      |  11 +-
 booster/library/Booster/Log.hs                |   5 +-
 .../library/Booster/Pattern/ApplyEquations.hs |  27 +-
 booster/library/Booster/Pattern/Base.hs       |   8 +-
 booster/library/Booster/Pattern/Binary.hs     |   2 +-
 booster/library/Booster/Pattern/Bool.hs       |   3 +-
 booster/library/Booster/Pattern/Implies.hs    |  67 ++-
 booster/library/Booster/Pattern/Match.hs      |  11 +-
 booster/library/Booster/Pattern/Rewrite.hs    | 113 +++--
 .../library/Booster/Pattern/Substitution.hs   |  68 +++
 booster/library/Booster/Pattern/Util.hs       |  33 --
 booster/library/Booster/SMT/Interface.hs      |   3 +-
 .../Booster/Syntax/Json/Externalise.hs        |  15 +-
 .../Booster/Syntax/Json/Internalise.hs        | 140 +++---
 .../Booster/Syntax/ParsedKore/Internalise.hs  |  35 +-
 .../response-branching.kore-rpc-dev           | 400 ------------------
 .../response-infeasible-branching.booster-dev |  48 +--
 ...ponse-mutual-constraints-stuck.booster-dev | 134 ------
 ...se-mutual-constraints-terminal.booster-dev | 119 ------
 .../response-one-ques-substitution.json       | 112 +++--
 ...sponse-one-ques-substitution.kore-rpc-dev} | 112 ++---
 ...ues.booster-dev => response-one-ques.json} |   0
 .../response-one-ques.kore-rpc-dev            | 121 ------
 ...er-dev => response-two-ques-external.json} |   0
 .../response-two-ques-external.kore-rpc-dev   | 124 ------
 ...ponse-two-ques-internal-with-counter.json} |   0
 ...er-dev => response-two-ques-internal.json} |   0
 .../response-two-ques-internal.kore-rpc-dev   | 172 --------
 .../test-substitutions/README.md              |   1 +
 .../response-circular-equations.booster-dev   | 218 ++++------
 ...response-concrete-substitution.booster-dev | 168 --------
 ...onse-symbolic-bottom-predicate.booster-dev | 183 --------
 .../response-symbolic-bottom-predicate.json   |   2 +-
 ...response-symbolic-substitution.booster-dev | 168 --------
 .../response-test1.json                       |  48 +--
 .../response-test2.json                       |  50 +--
 booster/tools/booster/Proxy.hs                |   3 +-
 .../unit-tests/Test/Booster/Pattern/Binary.hs |   2 +-
 .../Test/Booster/Pattern/Substitution.hs      |  84 ++++
 .../unit-tests/Test/Booster/Pattern/Util.hs   |  56 ---
 41 files changed, 693 insertions(+), 2245 deletions(-)
 create mode 100644 booster/library/Booster/Pattern/Substitution.hs
 delete mode 100644 booster/test/rpc-integration/test-a-to-f/response-branching.kore-rpc-dev
 delete mode 100644 booster/test/rpc-integration/test-diamond/response-mutual-constraints-stuck.booster-dev
 delete mode 100644 booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal.booster-dev
 rename booster/test/rpc-integration/test-questionmark-vars/{response-one-ques-substitution.booster-dev => response-one-ques-substitution.kore-rpc-dev} (67%)
 rename booster/test/rpc-integration/test-questionmark-vars/{response-one-ques.booster-dev => response-one-ques.json} (100%)
 delete mode 100644 booster/test/rpc-integration/test-questionmark-vars/response-one-ques.kore-rpc-dev
 rename booster/test/rpc-integration/test-questionmark-vars/{response-two-ques-external.booster-dev => response-two-ques-external.json} (100%)
 delete mode 100644 booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.kore-rpc-dev
 rename booster/test/rpc-integration/test-questionmark-vars/{response-two-ques-internal-with-counter.booster-dev => response-two-ques-internal-with-counter.json} (100%)
 rename booster/test/rpc-integration/test-questionmark-vars/{response-two-ques-internal.booster-dev => response-two-ques-internal.json} (100%)
 delete mode 100644 booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.kore-rpc-dev
 delete mode 100644 booster/test/rpc-integration/test-substitutions/response-concrete-substitution.booster-dev
 delete mode 100644 booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev
 delete mode 100644 booster/test/rpc-integration/test-substitutions/response-symbolic-substitution.booster-dev
 create mode 100644 booster/unit-tests/Test/Booster/Pattern/Substitution.hs

diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs
index 979da2e731..48dafb6cf2 100644
--- a/booster/library/Booster/JsonRpc.hs
+++ b/booster/library/Booster/JsonRpc.hs
@@ -44,7 +44,7 @@ import Booster.Definition.Base qualified as Definition (RewriteRule (..))
 import Booster.LLVM as LLVM (API)
 import Booster.Log
 import Booster.Pattern.ApplyEquations qualified as ApplyEquations
-import Booster.Pattern.Base (Pattern (..), Sort (SortApp), Term, Variable)
+import Booster.Pattern.Base (Pattern (..), Sort (SortApp))
 import Booster.Pattern.Base qualified as Pattern
 import Booster.Pattern.Implies (runImplies)
 import Booster.Pattern.Pretty
@@ -55,12 +55,11 @@ import Booster.Pattern.Rewrite (
     RewriteTrace (..),
     performRewrite,
  )
+import Booster.Pattern.Substitution qualified as Substitution
 import Booster.Pattern.Util (
     freeVariables,
     sortOfPattern,
     sortOfTerm,
-    substituteInPredicate,
-    substituteInTerm,
  )
 import Booster.Prettyprinter (renderText)
 import Booster.SMT.Interface qualified as SMT
@@ -69,6 +68,7 @@ import Booster.Syntax.Json.Externalise
 import Booster.Syntax.Json.Internalise (
     InternalisedPredicates (..),
     TermOrPredicates (..),
+    extractSubstitution,
     internalisePattern,
     internaliseTermOrPredicate,
     logPatternError,
@@ -131,12 +131,14 @@ respond stateVar request =
                                         [ req.logSuccessfulRewrites
                                         , req.logFailedRewrites
                                         ]
-                        -- apply the given substitution before doing anything else
+                        -- apply the given substitution before doing anything else,
+                        -- as internalisePattern does not substitute
                         let substPat =
                                 Pattern
-                                    { term = substituteInTerm substitution term
-                                    , constraints = Set.fromList $ map (substituteInPredicate substitution) preds
+                                    { term = Substitution.substituteInTerm substitution term
+                                    , constraints = Set.fromList $ map (Substitution.substituteInPredicate substitution) preds
                                     , ceilConditions = ceils
+                                    , substitution
                                     }
                             -- remember all variables used in the substitutions
                             substVars =
@@ -166,7 +168,7 @@ respond stateVar request =
                         result <-
                             performRewrite rewriteConfig substPat
                         SMT.finaliseSolver solver
-                        pure $ execResponse req result substitution unsupported
+                        pure $ execResponse req result unsupported
             RpcTypes.AddModule RpcTypes.AddModuleRequest{_module, nameAsId = nameAsId'} -> Booster.Log.withContext CtxAddModule $ runExceptT $ do
                 -- block other request executions while modifying the server state
                 state <- liftIO $ takeMVar stateVar
@@ -244,20 +246,14 @@ respond stateVar request =
                                     RpcError.CouldNotVerifyPattern $
                                         map patternErrorToRpcError patternErrors
                     -- term and predicate (pattern)
-                    Right (TermAndPredicates pat substitution unsupported) -> do
+                    -- NOTE: the input substitution will have already been applied by internaliseTermOrPredicate
+                    Right (TermAndPredicates pat unsupported) -> do
                         unless (null unsupported) $ do
                             withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $ do
                                 logMessage ("ignoring unsupported predicate parts" :: Text)
-                        -- apply the given substitution before doing anything else
-                        let substPat =
-                                Pattern
-                                    { term = substituteInTerm substitution pat.term
-                                    , constraints = Set.map (substituteInPredicate substitution) pat.constraints
-                                    , ceilConditions = pat.ceilConditions
-                                    }
-                        ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPat >>= \case
+                        ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty pat >>= \case
                             (Right newPattern, _) -> do
-                                let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern substitution
+                                let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern
                                     tSort = externaliseSort (sortOfPattern newPattern)
                                     result = case catMaybes (mbPredicate : mbSubstitution : map Just unsupported) of
                                         [] -> term
@@ -281,23 +277,24 @@ respond stateVar request =
                                 withKorePatternContext (KoreJson.KJAnd (externaliseSort $ SortApp "SortBool" []) ps.unsupported) $ do
                                     logMessage ("ignoring unsupported predicate parts" :: Text)
                             -- apply the given substitution before doing anything else
-                            let predicates = map (substituteInPredicate ps.substitution) ps.boolPredicates
+                            let predicates = map (Substitution.substituteInPredicate ps.substitution) ps.boolPredicates
                             withContext CtxConstraint $
                                 ApplyEquations.simplifyConstraints
                                     def
                                     mLlvmLibrary
                                     solver
                                     mempty
-                                    predicates
+                                    (predicates <> Substitution.asEquations ps.substitution)
                                     >>= \case
-                                        (Right newPreds, _) -> do
+                                        (Right simplified, _) -> do
                                             let predicateSort =
                                                     fromMaybe (error "not a predicate") $
                                                         sortOfJson req.state.term
+                                                (simplifiedSubstitution, simplifiedPredicates) = extractSubstitution simplified
                                                 result =
-                                                    map (externalisePredicate predicateSort) newPreds
+                                                    map (externalisePredicate predicateSort) (Set.toList simplifiedPredicates)
                                                         <> map (externaliseCeil predicateSort) ps.ceilPredicates
-                                                        <> map (uncurry $ externaliseSubstitution predicateSort) (Map.toList ps.substitution)
+                                                        <> map (uncurry $ externaliseSubstitution predicateSort) (Map.assocs simplifiedSubstitution)
                                                         <> ps.unsupported
 
                                             pure $ Right (addHeader $ Syntax.KJAnd predicateSort result)
@@ -332,7 +329,7 @@ respond stateVar request =
                             -- term and predicates were sent. Only work on predicates
                             (boolPs, suppliedSubst) <-
                                 case things of
-                                    TermAndPredicates pat substitution unsupported -> do
+                                    TermAndPredicates pat unsupported -> do
                                         withContext CtxGetModel $
                                             logMessage' ("ignoring supplied terms and only checking predicates" :: Text)
 
@@ -341,7 +338,7 @@ respond stateVar request =
                                                 logMessage' ("ignoring unsupported predicates" :: Text)
                                                 withContext CtxDetail $
                                                     logMessage (Text.unwords $ map prettyPattern unsupported)
-                                        pure (Set.toList pat.constraints, substitution)
+                                        pure (Set.toList pat.constraints, pat.substitution)
                                     Predicates ps -> do
                                         unless (null ps.ceilPredicates && null ps.unsupported) $ do
                                             withContext CtxGetModel $ do
@@ -472,10 +469,9 @@ execStateToKoreJson RpcTypes.ExecuteState{term = t, substitution, predicate} =
 execResponse ::
     RpcTypes.ExecuteRequest ->
     (Natural, Seq (RewriteTrace ()), RewriteResult Pattern) ->
-    Map Variable Term ->
     [Syntax.KorePattern] ->
     Either ErrorObj (RpcTypes.API 'RpcTypes.Res)
-execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
+execResponse req (d, traces, rr) unsupported = case rr of
     RewriteBranch p nexts ->
         Right $
             RpcTypes.Execute
@@ -483,10 +479,10 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
                     { reason = RpcTypes.Branching
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported Nothing
+                    , state = toExecState p unsupported Nothing
                     , nextStates =
                         Just $
-                            map (\(_, muid, p') -> toExecState p' originalSubstitution unsupported (Just muid)) $
+                            map (\(_, muid, p') -> toExecState p' unsupported (Just muid)) $
                                 toList nexts
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -498,7 +494,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
                     { reason = RpcTypes.Stuck
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported Nothing
+                    , state = toExecState p unsupported Nothing
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -510,7 +506,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
                     { reason = RpcTypes.Vacuous
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported Nothing
+                    , state = toExecState p unsupported Nothing
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -522,8 +518,8 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
                     { reason = RpcTypes.CutPointRule
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported Nothing
-                    , nextStates = Just [toExecState next originalSubstitution unsupported Nothing]
+                    , state = toExecState p unsupported Nothing
+                    , nextStates = Just [toExecState next unsupported Nothing]
                     , rule = Just lbl
                     , unknownPredicate = Nothing
                     }
@@ -534,7 +530,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
                     { reason = RpcTypes.TerminalRule
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported Nothing
+                    , state = toExecState p unsupported Nothing
                     , nextStates = Nothing
                     , rule = Just lbl
                     , unknownPredicate = Nothing
@@ -546,7 +542,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
                     { reason = RpcTypes.DepthBound
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported Nothing
+                    , state = toExecState p unsupported Nothing
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -563,7 +559,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
                                     (logSuccessfulRewrites, logFailedRewrites)
                                     (RewriteStepFailed failure)
                          in logs <|> abortRewriteLog
-                    , state = toExecState p originalSubstitution unsupported Nothing
+                    , state = toExecState p unsupported Nothing
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -586,8 +582,8 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
                 xs@(_ : _) -> Just xs
 
 toExecState ::
-    Pattern -> Map Variable Term -> [Syntax.KorePattern] -> Maybe UniqueId -> RpcTypes.ExecuteState
-toExecState pat sub unsupported muid =
+    Pattern -> [Syntax.KorePattern] -> Maybe UniqueId -> RpcTypes.ExecuteState
+toExecState pat unsupported muid =
     RpcTypes.ExecuteState
         { term = addHeader t
         , predicate = addHeader <$> addUnsupported p
@@ -597,7 +593,7 @@ toExecState pat sub unsupported muid =
         , ruleId = getUniqueId <$> muid
         }
   where
-    (t, p, s) = externalisePattern pat sub
+    (t, p, s) = externalisePattern pat
     termSort = externaliseSort $ sortOfPattern pat
     allUnsupported = Syntax.KJAnd termSort unsupported
     addUnsupported
diff --git a/booster/library/Booster/JsonRpc/Utils.hs b/booster/library/Booster/JsonRpc/Utils.hs
index f27e3e7909..1a319cfd47 100644
--- a/booster/library/Booster/JsonRpc/Utils.hs
+++ b/booster/library/Booster/JsonRpc/Utils.hs
@@ -279,18 +279,9 @@ diffBy def pat1 pat2 =
             <> if null ps.unsupported
                 then ""
                 else BS.unlines ("Unsupported parts:" : map Json.encode ps.unsupported)
-    renderBS (TermAndPredicates p m u) =
+    renderBS (TermAndPredicates p u) =
         ( BS.pack . renderDefault $
             pretty (PrettyWithModifiers @['Decoded, 'Truncated] p)
-                <+> vsep
-                    ( map
-                        ( \(k, v) ->
-                            pretty (PrettyWithModifiers @['Decoded, 'Truncated] k)
-                                <+> "="
-                                <+> pretty (PrettyWithModifiers @['Decoded, 'Truncated] v)
-                        )
-                        (Map.toList m)
-                    )
         )
             <> if null u then "" else BS.unlines ("Unsupported parts: " : map Json.encode u)
     internalise =
diff --git a/booster/library/Booster/Log.hs b/booster/library/Booster/Log.hs
index 5e862f8345..8cf4e9b36d 100644
--- a/booster/library/Booster/Log.hs
+++ b/booster/library/Booster/Log.hs
@@ -69,6 +69,7 @@ import Booster.Pattern.Base (
     pattern AndTerm,
  )
 import Booster.Pattern.Pretty
+import Booster.Pattern.Substitution (asEquations)
 import Booster.Prettyprinter (renderOneLineText)
 import Booster.Syntax.Json (KorePattern, addHeader, prettyPattern)
 import Booster.Syntax.Json.Externalise (externaliseTerm)
@@ -185,8 +186,8 @@ withTermContext t@(Term attrs _) m =
         m
 
 withPatternContext :: LoggerMIO m => Pattern -> m a -> m a
-withPatternContext Pattern{term, constraints} m =
-    let t' = foldl' AndTerm term $ Set.toList $ Set.map coerce constraints -- FIXME
+withPatternContext Pattern{term, constraints, substitution} m =
+    let t' = foldl' AndTerm term . map coerce $ Set.toList constraints <> asEquations substitution
      in withTermContext t' m
 
 instance ToLogFormat KorePattern where
diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs
index a410afebe0..53b801fcc2 100644
--- a/booster/library/Booster/Pattern/ApplyEquations.hs
+++ b/booster/library/Booster/Pattern/ApplyEquations.hs
@@ -66,10 +66,12 @@ import Booster.Pattern.Bool
 import Booster.Pattern.Index qualified as Idx
 import Booster.Pattern.Match
 import Booster.Pattern.Pretty
+import Booster.Pattern.Substitution
 import Booster.Pattern.Util
 import Booster.Prettyprinter (renderOneLineText)
 import Booster.SMT.Interface qualified as SMT
 import Booster.Syntax.Json.Externalise (externaliseTerm)
+import Booster.Syntax.Json.Internalise (extractSubstitution)
 import Booster.Util (Bound (..))
 import Kore.JsonRpc.Types.ContextLog (CLContext (CLWithId), IdContext (CtxCached))
 import Kore.Util (showHashHex)
@@ -455,7 +457,15 @@ evaluatePattern ::
     Pattern ->
     io (Either EquationFailure Pattern, SimplifierCache)
 evaluatePattern def mLlvmLibrary smtSolver cache pat =
-    runEquationT def mLlvmLibrary smtSolver cache pat.constraints . evaluatePattern' $ pat
+    runEquationT
+        def
+        mLlvmLibrary
+        smtSolver
+        cache
+        -- interpret substitution as additional known constraints
+        (pat.constraints <> (Set.fromList . asEquations $ pat.substitution))
+        . evaluatePattern'
+        $ pat
 
 -- version for internal nested evaluation
 evaluatePattern' ::
@@ -469,7 +479,20 @@ evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do
     traverse_ simplifyAssumedPredicate . predicates =<< getState
     -- this may yield additional new constraints, left unevaluated
     evaluatedConstraints <- predicates <$> getState
-    pure Pattern{constraints = evaluatedConstraints, term = newTerm, ceilConditions}
+    -- The interface-level evaluatePattern puts pat.substitution together with pat.constraints
+    -- into the simplifier state as known truth. Here the substitution will bubble-up as part of
+    -- evaluatedConstraints. To avoid duplicating constraints (i.e. having equivalent entities
+    -- in pat.predicate and pat.substitution), we discard the old substitution here
+    -- and extract a possible simplified one from evaluatedConstraints.
+    let (simplifiedSubsitution, simplifiedConstraints) = extractSubstitution (Set.toList evaluatedConstraints)
+
+    pure
+        Pattern
+            { constraints = simplifiedConstraints
+            , term = newTerm
+            , ceilConditions
+            , substitution = simplifiedSubsitution
+            }
   where
     -- when TooManyIterations exception occurred while evaluating the top-level term,
     -- i.e. not in a recursive evaluation of a side-condition,
diff --git a/booster/library/Booster/Pattern/Base.hs b/booster/library/Booster/Pattern/Base.hs
index a2b4661614..f8991bc259 100644
--- a/booster/library/Booster/Pattern/Base.hs
+++ b/booster/library/Booster/Pattern/Base.hs
@@ -36,6 +36,7 @@ import Data.Functor.Foldable
 import Data.Hashable (Hashable)
 import Data.Hashable qualified as Hashable
 import Data.List as List (foldl', foldl1', sort)
+import Data.Map.Strict (Map)
 import Data.Set (Set)
 import Data.Set qualified as Set
 import GHC.Generics (Generic)
@@ -761,19 +762,22 @@ pattern KSeq sort a =
 
 --------------------
 
+type Substitution = Map Variable Term
+
 -- | A term (configuration) constrained by a number of predicates.
 data Pattern = Pattern
     { term :: Term
     , constraints :: !(Set Predicate)
+    , substitution :: Substitution
     , ceilConditions :: ![Ceil]
     }
     deriving stock (Eq, Ord, Show, Generic, Data)
     deriving anyclass (NFData)
 
 pattern Pattern_ :: Term -> Pattern
-pattern Pattern_ t <- Pattern t _ _
+pattern Pattern_ t <- Pattern t _ _ _
     where
-        Pattern_ t = Pattern t mempty mempty
+        Pattern_ t = Pattern t mempty mempty mempty
 
 pattern ConsApplication :: Symbol -> [Sort] -> [Term] -> Term
 pattern ConsApplication sym sorts args <-
diff --git a/booster/library/Booster/Pattern/Binary.hs b/booster/library/Booster/Pattern/Binary.hs
index c398e33878..9f8f9d2ac7 100644
--- a/booster/library/Booster/Pattern/Binary.hs
+++ b/booster/library/Booster/Pattern/Binary.hs
@@ -564,7 +564,7 @@ decodePattern mDef = do
                 preds <- forM preds' $ \case
                     BPredicate pIdx -> Predicate <$> getTerm pIdx
                     _ -> fail "Expecting a predicate"
-                pure $ Pattern trm (Set.fromList preds) mempty
+                pure $ Pattern trm (Set.fromList preds) mempty mempty
             _ -> fail "Expecting a term on the top of the stack"
 
 encodeMagicHeaderAndVersion :: Version -> Put
diff --git a/booster/library/Booster/Pattern/Bool.hs b/booster/library/Booster/Pattern/Bool.hs
index 39dd2cacc3..a232a86239 100644
--- a/booster/library/Booster/Pattern/Bool.hs
+++ b/booster/library/Booster/Pattern/Bool.hs
@@ -36,11 +36,10 @@ import Booster.Definition.Attributes.Base (
     pattern IsNotMacroOrAlias,
  )
 import Booster.Pattern.Base (
-    Pattern,
+    Pattern (..),
     Predicate (..),
     Symbol (Symbol),
     Term,
-    constraints,
     pattern DomainValue,
     pattern SortBool,
     pattern SortInt,
diff --git a/booster/library/Booster/Pattern/Implies.hs b/booster/library/Booster/Pattern/Implies.hs
index 0dd5a33f0e..92ec8d9cfb 100644
--- a/booster/library/Booster/Pattern/Implies.hs
+++ b/booster/library/Booster/Pattern/Implies.hs
@@ -26,7 +26,8 @@ import Booster.Pattern.Base (Pattern (..), Predicate (..))
 import Booster.Pattern.Bool (pattern TrueBool)
 import Booster.Pattern.Match (FailReason (..), MatchResult (..), MatchType (Implies), matchTerms)
 import Booster.Pattern.Pretty (FromModifiersT, ModifiersRep (..), pretty')
-import Booster.Pattern.Util (freeVariables, sortOfPattern, substituteInPredicate, substituteInTerm)
+import Booster.Pattern.Substitution (asEquations)
+import Booster.Pattern.Util (freeVariables, sortOfPattern)
 import Booster.Prettyprinter (renderDefault)
 import Booster.SMT.Interface qualified as SMT
 import Booster.Syntax.Json (addHeader, prettyPattern)
@@ -68,8 +69,10 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
                      in runExcept $
                             internalisePatternOrTopOrBottom DisallowAlias CheckSubsorts Nothing def existentials korePat
 
-                checkImplies patL substitutionL unsupportedL existsL patR substitutionR unsupportedR existsR = do
-                    let freeVarsL =
+                checkImplies patL unsupportedL existsL patR unsupportedR existsR = do
+                    let substitutionL = patL.substitution
+                        substitutionR = patR.substitution
+                        freeVarsL =
                             ( freeVariables patL.term
                                 <> (Set.unions $ Set.map (freeVariables . coerce) patL.constraints)
                                 <> (Set.fromList $ Map.keys substitutionL)
@@ -104,41 +107,26 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
                                     map (pack . show) $
                                         unsupportedL <> unsupportedR
                         | otherwise -> do
-                            let
-                                -- apply the given substitution before doing anything else
-                                substPatL =
-                                    Pattern
-                                        { term = substituteInTerm substitutionL patL.term
-                                        , constraints = Set.map (substituteInPredicate substitutionL) patL.constraints
-                                        , ceilConditions = patL.ceilConditions
-                                        }
-                                substPatR =
-                                    Pattern
-                                        { term = substituteInTerm substitutionR patR.term
-                                        , constraints = Set.map (substituteInPredicate substitutionR) patR.constraints
-                                        , ceilConditions = patR.ceilConditions
-                                        }
-
-                            SMT.isSat solver (Set.toList substPatL.constraints) >>= \case
+                            SMT.isSat solver (Set.toList patL.constraints) patL.substitution >>= \case
                                 SMT.IsUnsat ->
-                                    let sort = externaliseSort $ sortOfPattern substPatL
+                                    let sort = externaliseSort $ sortOfPattern patL
                                      in implies' (Kore.Syntax.KJBottom sort) sort antecedent.term consequent.term mempty
-                                _ -> checkImpliesMatchTerms existsL substPatL existsR substPatR
+                                _ -> checkImpliesMatchTerms existsL patL existsR patR
 
-                checkImpliesMatchTerms existsL substPatL existsR substPatR =
-                    case matchTerms Booster.Pattern.Match.Implies def substPatR.term substPatL.term of
+                checkImpliesMatchTerms existsL patL existsR patR =
+                    case matchTerms Booster.Pattern.Match.Implies def patR.term patL.term of
                         MatchFailed (SubsortingError sortError) ->
                             pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $
                                 show sortError
                         MatchFailed{} ->
                             doesNotImply
-                                (sortOfPattern substPatL)
-                                (externaliseExistTerm existsL substPatL.term)
-                                (externaliseExistTerm existsR substPatR.term)
+                                (sortOfPattern patL)
+                                (externaliseExistTerm existsL patL.term)
+                                (externaliseExistTerm existsR patR.term)
                         MatchIndeterminate remainder ->
-                            ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPatL >>= \case
+                            ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty patL >>= \case
                                 (Right simplifedSubstPatL, _) ->
-                                    if substPatL == simplifedSubstPatL
+                                    if patL == simplifedSubstPatL
                                         then -- we are being conservative here for now and returning an error.
                                         -- since we have already simplified the LHS, we may want to eventually return implise, but the condition
                                         -- will contain the remainder as an equality contraint, predicating the implication on that equality being true.
@@ -151,19 +139,20 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
                                                                 map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $
                                                                     NonEmpty.toList remainder
                                                         )
-                                        else checkImpliesMatchTerms existsL simplifedSubstPatL existsR substPatR
+                                        else checkImpliesMatchTerms existsL simplifedSubstPatL existsR patR
                                 (Left err, _) ->
                                     pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ err)
                         MatchSuccess subst -> do
                             let filteredConsequentPreds =
-                                    Set.map (substituteInPredicate subst) substPatR.constraints `Set.difference` substPatL.constraints
+                                    (patR.constraints <> (Set.fromList $ asEquations patR.substitution))
+                                        `Set.difference` (patL.constraints <> (Set.fromList $ asEquations patL.substitution))
 
                             if null filteredConsequentPreds
                                 then
                                     implies
-                                        (sortOfPattern substPatL)
-                                        (externaliseExistTerm existsL substPatL.term)
-                                        (externaliseExistTerm existsR substPatR.term)
+                                        (sortOfPattern patL)
+                                        (externaliseExistTerm existsL patL.term)
+                                        (externaliseExistTerm existsR patR.term)
                                         subst
                                 else
                                     ApplyEquations.evaluateConstraints def mLlvmLibrary solver mempty filteredConsequentPreds >>= \case
@@ -171,9 +160,9 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
                                             if all (== Predicate TrueBool) newPreds
                                                 then
                                                     implies
-                                                        (sortOfPattern substPatL)
-                                                        (externaliseExistTerm existsL substPatL.term)
-                                                        (externaliseExistTerm existsR substPatR.term)
+                                                        (sortOfPattern patL)
+                                                        (externaliseExistTerm existsL patL.term)
+                                                        (externaliseExistTerm existsR patR.term)
                                                         subst
                                                 else -- here we conservatively abort
                                                 -- an anlternative would be to return valid, putting the unknown constraints into the
@@ -204,10 +193,10 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
                 (Right IsTop{}, _) ->
                     pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly $
                         "The check implication step expects the antecedent term to be function-like."
-                ( Right (IsPattern (existsL, patL, substitutionL, unsupportedL))
-                    , Right (IsPattern (existsR, patR, substitutionR, unsupportedR))
+                ( Right (IsPattern (existsL, patL, unsupportedL))
+                    , Right (IsPattern (existsR, patR, unsupportedR))
                     ) ->
-                        checkImplies patL substitutionL unsupportedL existsL patR substitutionR unsupportedR existsR
+                        checkImplies patL unsupportedL existsL patR unsupportedR existsR
                 (Right IsPattern{}, Right (IsTop sort)) ->
                     implies' (Kore.Syntax.KJTop sort) sort antecedent.term consequent.term mempty
                 (Right IsPattern{}, Right (IsBottom sort)) ->
diff --git a/booster/library/Booster/Pattern/Match.hs b/booster/library/Booster/Pattern/Match.hs
index dd8d82caa0..b85985f7eb 100644
--- a/booster/library/Booster/Pattern/Match.hs
+++ b/booster/library/Booster/Pattern/Match.hs
@@ -8,7 +8,6 @@ module Booster.Pattern.Match (
     MatchResult (..),
     MatchType (..),
     FailReason (..),
-    Substitution,
     matchTerms,
     checkSubsort,
     SortError (..),
@@ -37,12 +36,12 @@ import Booster.Definition.Attributes.Base (KListDefinition, KMapDefinition, KSet
 import Booster.Definition.Base
 import Booster.Pattern.Base
 import Booster.Pattern.Pretty
+import Booster.Pattern.Substitution qualified as Substitution
 import Booster.Pattern.Util (
     checkSymbolIsAc,
     freeVariables,
     isConstructorSymbol,
     sortOfTerm,
-    substituteInTerm,
  )
 
 -- | Result of matching a pattern to a subject (a substitution or an indication of what went wrong)
@@ -119,8 +118,6 @@ instance FromModifiersT mods => Pretty (PrettyWithModifiers mods FailReason) whe
         SubjectVariableMatch t v ->
             hsep ["Cannot match variable in subject:", pretty' @mods v, pretty' @mods t]
 
-type Substitution = Map Variable Term
-
 {- | Attempts to find a simple unifying substitution for the given
    terms.
 
@@ -668,7 +665,7 @@ matchMaps
             -- before matching map keys.
                 enqueueMapProblem (KMap def patKeyVals patRest) (KMap def subjKeyVals subjRest)
             else do
-                let patternKeyVals = map (first (substituteInTerm st.mSubstitution)) patKeyVals
+                let patternKeyVals = map (first (Substitution.substituteInTerm st.mSubstitution)) patKeyVals
                 -- check for duplicate keys
                 checkDuplicateKeys patternKeyVals patRest
                 checkDuplicateKeys subjKeyVals subjRest
@@ -785,13 +782,13 @@ bindVariable matchType var term@(Term termAttrs _) = do
         Nothing -> do
             let
                 -- apply existing substitutions to term
-                term' = substituteInTerm currentSubst term
+                term' = Substitution.substituteInTerm currentSubst term
             when (var `Set.member` freeVariables term') $
                 failWith (VariableRecursion var term)
             let
                 -- substitute in existing substitution terms
                 currentSubst' =
-                    Map.map (substituteInTerm $ Map.singleton var term') currentSubst
+                    Map.map (Substitution.substituteInTerm $ Map.singleton var term') currentSubst
                 newSubst = Map.insert var term' currentSubst'
             modify $ \s -> s{mSubstitution = newSubst}
 
diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs
index 39d6f71c2f..47c16b6321 100644
--- a/booster/library/Booster/Pattern/Rewrite.hs
+++ b/booster/library/Booster/Pattern/Rewrite.hs
@@ -63,14 +63,15 @@ import Booster.Pattern.Match (
     MatchResult (MatchFailed, MatchIndeterminate, MatchSuccess),
     MatchType (Rewrite),
     SortError,
-    Substitution,
     matchTerms,
  )
 import Booster.Pattern.Pretty
+import Booster.Pattern.Substitution
 import Booster.Pattern.Util
 import Booster.Prettyprinter
 import Booster.SMT.Interface qualified as SMT
 import Booster.Syntax.Json.Externalise (externaliseTerm)
+import Booster.Syntax.Json.Internalise (extractSubstitution)
 import Booster.Util (Flag (..))
 
 newtype RewriteT io a = RewriteT
@@ -279,8 +280,8 @@ applyRule pat@Pattern{ceilConditions} rule =
             getPrettyModifiers >>= \case
                 ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> do
                     def <- lift getDefinition
-                    -- unify terms
-                    subst <- withContext CtxMatch $ case matchTerms Rewrite def rule.lhs pat.term of
+                    -- match term with rule's left-hand side
+                    ruleSubstitution <- withContext CtxMatch $ case matchTerms Rewrite def rule.lhs pat.term of
                         MatchFailed (SubsortingError sortError) -> do
                             withContext CtxError $ logPretty' @mods sortError
                             failRewrite $ RewriteSortError rule pat.term sortError
@@ -303,23 +304,38 @@ applyRule pat@Pattern{ceilConditions} rule =
                                                                 NE.toList remainder
                                                     )
                             failRewrite $ RuleApplicationUnclear rule pat.term remainder
-                        MatchSuccess substitution -> do
+                        MatchSuccess matchingSubstitution -> do
+                            -- existential variables may be present in rule.rhs and rule.ensures,
+                            -- need to strip prefixes and freshen their names with respect to variables already
+                            -- present in the input pattern and in the matching substitution
+                            varsFromInput <- lift . RewriteT $ asks (.varsToAvoid)
+                            let varsFromPattern = freeVariables pat.term <> (Set.unions $ Set.map (freeVariables . coerce) pat.constraints)
+                                varsFromSubst = Set.unions . map freeVariables . Map.elems $ matchingSubstitution
+                                forbiddenVars = varsFromInput <> varsFromPattern <> varsFromSubst
+                                existentialSubst =
+                                    Map.fromSet
+                                        (\v -> Var $ freshenVar v{variableName = stripMarker v.variableName} forbiddenVars)
+                                        rule.existentials
+                                ruleSubstitution = matchingSubstitution <> existentialSubst
+
                             withContext CtxSuccess $ do
                                 logMessage rule
                                 withContext CtxSubstitution
                                     $ logMessage
                                     $ WithJsonMessage
                                         ( object
-                                            ["substitution" .= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList substitution)]
+                                            [ "substitution"
+                                                .= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList ruleSubstitution)
+                                            ]
                                         )
                                     $ renderOneLineText
                                     $ "Substitution:"
                                         <+> ( hsep $
                                                 intersperse "," $
                                                     map (\(k, v) -> pretty' @mods k <+> "->" <+> pretty' @mods v) $
-                                                        Map.toList substitution
+                                                        Map.toList ruleSubstitution
                                             )
-                            pure substitution
+                            pure ruleSubstitution
 
                     -- Also fail the whole rewrite if a rule applies but may introduce
                     -- an undefined term.
@@ -336,40 +352,35 @@ applyRule pat@Pattern{ceilConditions} rule =
                                 rule.computedAttributes.notPreservesDefinednessReasons
 
                     -- check required constraints from lhs: Stop if any is false, abort rewrite if indeterminate.
-                    checkRequires subst
+                    checkRequires ruleSubstitution
 
                     -- check ensures constraints (new) from rhs: stop and return `Trivial` if
                     -- any are false, remove all that are trivially true, return the rest
-                    newConstraints <- checkEnsures subst
+                    ensuredConditions <- checkEnsures ruleSubstitution
 
                     -- if a new constraint is going to be added, the equation cache is invalid
-                    unless (null newConstraints) $ do
+                    unless (null ensuredConditions) $ do
                         withContextFor Equations . logMessage $
                             ("New path condition ensured, invalidating cache" :: Text)
                         lift . RewriteT . lift . modify $ \s -> s{equations = mempty}
 
-                    -- existential variables may be present in rule.rhs and rule.ensures,
-                    -- need to strip prefixes and freshen their names with respect to variables already
-                    -- present in the input pattern and in the unification substitution
-                    varsFromInput <- lift . RewriteT $ asks (.varsToAvoid)
-                    let varsFromPattern = freeVariables pat.term <> (Set.unions $ Set.map (freeVariables . coerce) pat.constraints)
-                        varsFromSubst = Set.unions . map freeVariables . Map.elems $ subst
-                        forbiddenVars = varsFromInput <> varsFromPattern <> varsFromSubst
-                        existentialSubst =
-                            Map.fromSet
-                                (\v -> Var $ freshenVar v{variableName = stripMarker v.variableName} forbiddenVars)
-                                rule.existentials
-
-                    -- modify the substitution to include the existentials
-                    let substWithExistentials = subst `Map.union` existentialSubst
+                    -- partition ensured constrains into substitution and predicates
+                    let (newSubsitution, newConstraints) = extractSubstitution ensuredConditions
+
+                    -- compose the existing substitution pattern and the newly acquired one
+                    let (modifiedPatternSubst, leftoverConstraints) = extractSubstitution . asEquations $ newSubsitution `compose` pat.substitution
 
+                    let rewrittenTerm = substituteInTerm (modifiedPatternSubst `compose` ruleSubstitution) rule.rhs
+                        substitutedNewConstraints =
+                            Set.map
+                                (coerce . substituteInTerm (modifiedPatternSubst `compose` ruleSubstitution) . coerce)
+                                newConstraints
                     let rewritten =
                             Pattern
-                                (substituteInTerm substWithExistentials rule.rhs)
+                                rewrittenTerm
                                 -- adding new constraints that have not been trivially `Top`, substituting the Ex# variables
-                                ( pat.constraints
-                                    <> (Set.fromList $ map (coerce . substituteInTerm existentialSubst . coerce) newConstraints)
-                                )
+                                (pat.constraints <> substitutedNewConstraints <> leftoverConstraints)
+                                modifiedPatternSubst -- ruleSubstitution is not needed, do not attach it to the result
                                 ceilConditions
                     withContext CtxSuccess $
                         withPatternContext rewritten $
@@ -424,21 +435,37 @@ applyRule pat@Pattern{ceilConditions} rule =
         -- apply substitution to rule requires
         let ruleRequires =
                 concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) rule.requires
+            knownConstraints = pat.constraints <> (Set.fromList . asEquations $ pat.substitution)
 
         -- filter out any predicates known to be _syntactically_ present in the known prior
-        toCheck <- lift $ filterOutKnownConstraints pat.constraints ruleRequires
+        toCheck <-
+            lift $
+                filterOutKnownConstraints
+                    knownConstraints
+                    ruleRequires
 
         -- simplify the constraints (one by one in isolation). Stop if false, abort rewrite if indeterminate.
         unclearRequires <-
-            catMaybes <$> mapM (checkConstraint id notAppliedIfBottom pat.constraints) toCheck
+            catMaybes
+                <$> mapM
+                    ( checkConstraint
+                        id
+                        notAppliedIfBottom
+                        knownConstraints
+                    )
+                    toCheck
 
         -- unclear conditions may have been simplified and
         -- could now be syntactically present in the path constraints, filter again
-        stillUnclear <- lift $ filterOutKnownConstraints pat.constraints unclearRequires
+        stillUnclear <-
+            lift $
+                filterOutKnownConstraints
+                    knownConstraints
+                    unclearRequires
 
         -- check unclear requires-clauses in the context of known constraints (priorKnowledge)
         solver <- lift $ RewriteT $ (.smtSolver) <$> ask
-        SMT.checkPredicates solver pat.constraints mempty (Set.fromList stillUnclear) >>= \case
+        SMT.checkPredicates solver pat.constraints pat.substitution (Set.fromList stillUnclear) >>= \case
             SMT.IsUnknown reason -> do
                 -- abort rewrite if a solver result was Unknown
                 withContext CtxAbort $ logMessage reason
@@ -452,17 +479,25 @@ applyRule pat@Pattern{ceilConditions} rule =
     checkEnsures ::
         Substitution -> RewriteRuleAppT (RewriteT io) [Predicate]
     checkEnsures matchingSubst = do
-        -- apply substitution to rule requires
+        -- apply substitution to rule ensures
         let ruleEnsures =
                 concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) rule.ensures
+            knownConstraints = pat.constraints <> (Set.fromList . asEquations $ pat.substitution)
         newConstraints <-
-            catMaybes <$> mapM (checkConstraint id trivialIfBottom pat.constraints) ruleEnsures
+            catMaybes
+                <$> mapM
+                    ( checkConstraint
+                        id
+                        trivialIfBottom
+                        knownConstraints
+                    )
+                    ruleEnsures
 
         -- check all new constraints together with the known side constraints
         solver <- lift $ RewriteT $ (.smtSolver) <$> ask
         -- TODO it is probably enough to establish satisfiablity (rather than validity) of the ensured conditions.
         -- For now, we check validity to be safe and admit indeterminate result (i.e. (P, not P) is (Sat, Sat)).
-        (lift $ SMT.checkPredicates solver pat.constraints mempty (Set.fromList newConstraints)) >>= \case
+        (lift $ SMT.checkPredicates solver pat.constraints pat.substitution (Set.fromList newConstraints)) >>= \case
             SMT.IsInvalid -> do
                 withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text)
                 RewriteRuleAppT $ pure Trivial
@@ -480,12 +515,6 @@ applyRule pat@Pattern{ceilConditions} rule =
             _other ->
                 pure ()
 
-        -- if a new constraint is going to be added, the equation cache is invalid
-        unless (null newConstraints) $ do
-            withContextFor Equations . logMessage $
-                ("New path condition ensured, invalidating cache" :: Text)
-
-            lift . RewriteT . lift . modify $ \s -> s{equations = mempty}
         pure newConstraints
 
     smtUnclear :: [Predicate] -> RewriteRuleAppT (RewriteT io) ()
@@ -669,7 +698,7 @@ mkDiffTerms = \case
   * RewriteStuck: config could not be re-written by any rule, return current
   * RewriteFailed: rewriter cannot handle the case, return current
 
-  The actions are logged at the custom log level '"Rewrite"'.
+  The result also includes a @'Substitution'@ accumulated from the rules ensures clauses.
 
 
     This flow chart should represent the actions of this function:
diff --git a/booster/library/Booster/Pattern/Substitution.hs b/booster/library/Booster/Pattern/Substitution.hs
new file mode 100644
index 0000000000..f2299ccf37
--- /dev/null
+++ b/booster/library/Booster/Pattern/Substitution.hs
@@ -0,0 +1,68 @@
+{- |
+Copyright   : (c) Runtime Verification, 2024
+License     : BSD-3-Clause
+
+Function to manipulate @'Substitution'@s and convert to/from @'Predicate'@s
+
+This module is intended to be imported qualified.
+-}
+module Booster.Pattern.Substitution (
+    mkEq,
+    asEquations,
+    compose,
+    substituteInPredicate,
+    substituteInTerm,
+) where
+
+import Data.Bifunctor (bimap)
+import Data.Coerce (coerce)
+import Data.Map.Strict (Map)
+import Data.Map.Strict qualified as Map
+import Data.Maybe (fromMaybe)
+import Data.Set qualified as Set
+
+import Booster.Pattern.Base
+import Booster.Pattern.Bool
+import Booster.Pattern.Util (sortOfTerm)
+
+{- | Compose substitutions:
+     - apply the left one to the assignments in the right one
+     - merge left with the result of above, left takes priority
+-}
+compose :: Substitution -> Substitution -> Substitution
+compose newSubst oldSubst =
+    let substitutedOldSubst = Map.map (substituteInTerm newSubst) oldSubst
+     in (newSubst `Map.union` substitutedOldSubst) -- new bindings take priority
+
+-- | Build an equality predicate form a variable assignment
+mkEq :: Variable -> Term -> Predicate
+mkEq x t = Predicate $ case sortOfTerm t of
+    SortInt -> EqualsInt (Var x) t
+    SortBool -> EqualsBool (Var x) t
+    otherSort -> EqualsK (KSeq otherSort (Var x)) (KSeq otherSort t)
+
+-- | turns a substitution into a list of equations
+asEquations :: Map Variable Term -> [Predicate]
+asEquations = map (uncurry mkEq) . Map.assocs
+
+substituteInTerm :: Substitution -> Term -> Term
+substituteInTerm substitution = goSubst
+  where
+    targetSet = Map.keysSet substitution
+    goSubst t
+        | Set.null (targetSet `Set.intersection` (getAttributes t).variables) = t
+        | otherwise = case t of
+            Var v -> fromMaybe t (Map.lookup v substitution)
+            DomainValue{} -> t
+            SymbolApplication sym sorts args ->
+                SymbolApplication sym sorts $ map goSubst args
+            AndTerm t1 t2 -> AndTerm (goSubst t1) (goSubst t2)
+            Injection ss s sub -> Injection ss s (goSubst sub)
+            KMap attrs keyVals rest -> KMap attrs (bimap goSubst goSubst <$> keyVals) (goSubst <$> rest)
+            KList def heads rest ->
+                KList def (map goSubst heads) (bimap goSubst (map goSubst) <$> rest)
+            KSet def elements rest ->
+                KSet def (map goSubst elements) (goSubst <$> rest)
+
+substituteInPredicate :: Substitution -> Predicate -> Predicate
+substituteInPredicate substitution = coerce . substituteInTerm substitution . coerce
diff --git a/booster/library/Booster/Pattern/Util.hs b/booster/library/Booster/Pattern/Util.hs
index c819db8758..7f249d58ed 100644
--- a/booster/library/Booster/Pattern/Util.hs
+++ b/booster/library/Booster/Pattern/Util.hs
@@ -6,9 +6,6 @@ module Booster.Pattern.Util (
     substituteInSort,
     sortOfTerm,
     sortOfPattern,
-    substituteInTerm,
-    substituteInPredicate,
-    modifyVariables,
     modifyVariablesInT,
     modifyVariablesInP,
     modifyVarName,
@@ -82,36 +79,6 @@ substituteInSort subst (SortApp n args) =
 sortOfPattern :: Pattern -> Sort
 sortOfPattern pat = sortOfTerm pat.term
 
-substituteInTerm :: Map Variable Term -> Term -> Term
-substituteInTerm substitution = goSubst
-  where
-    targetSet = Map.keysSet substitution
-    goSubst t
-        | Set.null (targetSet `Set.intersection` (getAttributes t).variables) = t
-        | otherwise = case t of
-            Var v -> fromMaybe t (Map.lookup v substitution)
-            DomainValue{} -> t
-            SymbolApplication sym sorts args ->
-                SymbolApplication sym sorts $ map goSubst args
-            AndTerm t1 t2 -> AndTerm (goSubst t1) (goSubst t2)
-            Injection ss s sub -> Injection ss s (goSubst sub)
-            KMap attrs keyVals rest -> KMap attrs (bimap goSubst goSubst <$> keyVals) (goSubst <$> rest)
-            KList def heads rest ->
-                KList def (map goSubst heads) (bimap goSubst (map goSubst) <$> rest)
-            KSet def elements rest ->
-                KSet def (map goSubst elements) (goSubst <$> rest)
-
-substituteInPredicate :: Map Variable Term -> Predicate -> Predicate
-substituteInPredicate substitution = coerce . substituteInTerm substitution . coerce
-
-modifyVariables :: (Variable -> Variable) -> Pattern -> Pattern
-modifyVariables f p =
-    Pattern
-        { term = modifyVariablesInT f p.term
-        , constraints = Set.map (modifyVariablesInP f) p.constraints
-        , ceilConditions = map (coerce $ modifyVariablesInT f) p.ceilConditions
-        }
-
 modifyVariablesInT :: (Variable -> Variable) -> Term -> Term
 modifyVariablesInT f = cata $ \case
     VarF v -> Var (f v)
diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs
index 731562f2d4..962f3e5a1f 100644
--- a/booster/library/Booster/SMT/Interface.hs
+++ b/booster/library/Booster/SMT/Interface.hs
@@ -280,8 +280,9 @@ isSat ::
     Log.LoggerMIO io =>
     SMT.SMTContext ->
     [Predicate] ->
+    Map Variable Term -> -- supplied substitution
     io (IsSatResult ())
-isSat ctxt ps = fmap void <$> (isSatReturnTransState ctxt ps mempty)
+isSat ctxt ps subst = fmap void <$> (isSatReturnTransState ctxt ps subst)
 
 {- |
 Implementation of get-model request
diff --git a/booster/library/Booster/Syntax/Json/Externalise.hs b/booster/library/Booster/Syntax/Json/Externalise.hs
index 4c0ba5e8eb..2b7bf2494e 100644
--- a/booster/library/Booster/Syntax/Json/Externalise.hs
+++ b/booster/library/Booster/Syntax/Json/Externalise.hs
@@ -20,7 +20,6 @@ import Booster.Pattern.Base (externaliseKmapUnsafe)
 import Booster.Pattern.Base qualified as Internal
 import Booster.Pattern.Bool qualified as Internal
 import Booster.Pattern.Util (sortOfTerm)
-import Data.Map (Map)
 import Data.Map qualified as Map
 import Kore.Syntax.Json.Types qualified as Syntax
 
@@ -30,16 +29,16 @@ import Kore.Syntax.Json.Types qualified as Syntax
 -}
 externalisePattern ::
     Internal.Pattern ->
-    Map Internal.Variable Internal.Term ->
     (Syntax.KorePattern, Maybe Syntax.KorePattern, Maybe Syntax.KorePattern)
-externalisePattern Internal.Pattern{term = term, constraints, ceilConditions} substitutions =
+externalisePattern Internal.Pattern{term = term, constraints, ceilConditions, substitution} =
     -- need a sort for the predicates in external format
     let sort = externaliseSort $ sortOfTerm term
-        substitution =
-            if null substitutions
+        -- inputSubstitution is probably not needed here at all
+        externalisedSubstitution =
+            if null substitution
                 then Nothing
-                else Just . multiAnd sort . map (uncurry $ externaliseSubstitution sort) . Map.toList $ substitutions
-        predicate =
+                else Just . multiAnd sort . map (uncurry $ externaliseSubstitution sort) . Map.toList $ substitution
+        externalisedPredicate =
             if null constraints && null ceilConditions
                 then Nothing
                 else
@@ -47,7 +46,7 @@ externalisePattern Internal.Pattern{term = term, constraints, ceilConditions} su
                         multiAnd sort $
                             map (externalisePredicate sort) (Set.toList constraints)
                                 ++ map (externaliseCeil sort) ceilConditions
-     in (externaliseTerm term, predicate, substitution)
+     in (externaliseTerm term, externalisedPredicate, externalisedSubstitution)
   where
     multiAnd :: Syntax.Sort -> [Syntax.KorePattern] -> Syntax.KorePattern
     multiAnd _ [] = error "multiAnd: empty"
diff --git a/booster/library/Booster/Syntax/Json/Internalise.hs b/booster/library/Booster/Syntax/Json/Internalise.hs
index dbca5fb972..591895b18d 100644
--- a/booster/library/Booster/Syntax/Json/Internalise.hs
+++ b/booster/library/Booster/Syntax/Json/Internalise.hs
@@ -24,7 +24,6 @@ module Booster.Syntax.Json.Internalise (
     textToBS,
     trm,
     handleBS,
-    asEquations,
     TermOrPredicates (..),
     InternalisedPredicates (..),
     PatternOrTopOrBottom (..),
@@ -36,6 +35,8 @@ module Booster.Syntax.Json.Internalise (
     pattern CheckSubsorts,
     pattern IgnoreSubsorts,
     logPatternError,
+    -- substitution mining
+    extractSubstitution,
     -- for test only
     InternalisedPredicate (..),
 ) where
@@ -50,6 +51,7 @@ import Data.ByteString.Char8 (ByteString, isPrefixOf)
 import Data.ByteString.Char8 qualified as BS
 import Data.Char (isLower)
 import Data.Coerce (coerce)
+import Data.Either (partitionEithers)
 import Data.Foldable ()
 import Data.Generics (extQ)
 import Data.Graph (SCC (..), stronglyConnComp)
@@ -72,6 +74,7 @@ import Booster.Log (LoggerMIO, logMessage, withKorePatternContext)
 import Booster.Pattern.Base qualified as Internal
 import Booster.Pattern.Bool qualified as Internal
 import Booster.Pattern.Pretty
+import Booster.Pattern.Substitution qualified as Internal
 import Booster.Pattern.Util (freeVariables, sortOfTerm, substituteInSort)
 import Booster.Prettyprinter (renderDefault)
 import Booster.Syntax.Json (addHeader)
@@ -131,15 +134,20 @@ data TermOrPredicates -- = Either Predicate Pattern
     = Predicates InternalisedPredicates
     | TermAndPredicates
         Internal.Pattern
-        (Map Internal.Variable Internal.Term)
         [Syntax.KorePattern]
     deriving stock (Eq, Show)
 
 retractPattern :: TermOrPredicates -> Maybe Internal.Pattern
-retractPattern (TermAndPredicates patt _ _) = Just patt
+retractPattern (TermAndPredicates patt _) = Just patt
 retractPattern _ = Nothing
 
--- main interface functions
+{- | Internalise a @'Syntax.KorePattern'@ into the components constituting a @'Internal.Pattern'@
+
+     Note: This function will NOT apply the internalised @'Internal.Substitution'@ to the other components.
+           The callers of this function must decide if it is necessary to substitute.
+           Use @'internalisePatternOrTopOrBottom'@ or @'internaliseTermOrPredicate'@ that return an already
+           substituted @'Internal.Pattern'@.
+-}
 internalisePattern ::
     Flag "alias" ->
     Flag "subsorts" ->
@@ -151,7 +159,7 @@ internalisePattern ::
         ( Internal.Term
         , [Internal.Predicate]
         , [Internal.Ceil]
-        , Map Internal.Variable Internal.Term
+        , Internal.Substitution
         , [Syntax.KorePattern]
         )
 internalisePattern allowAlias checkSubsorts sortVars definition p = do
@@ -191,7 +199,11 @@ data PatternOrTopOrBottom a
     | IsPattern a
     deriving (Functor)
 
--- main interface functions
+{- | Internalise a @'Syntax.KorePattern'@ into @'Internal.Pattern'@, detecting and reporting trivial cases.
+
+     Note: This function will apply the internalised @'Internal.Substitution'@ part of the pattern's constraints
+           to the term and constraints (but not the ceils).
+-}
 internalisePatternOrTopOrBottom ::
     Flag "alias" ->
     Flag "subsorts" ->
@@ -202,7 +214,7 @@ internalisePatternOrTopOrBottom ::
     Except
         PatternError
         ( PatternOrTopOrBottom
-            ([Internal.Variable], Internal.Pattern, Map Internal.Variable Internal.Term, [Syntax.KorePattern])
+            ([Internal.Variable], Internal.Pattern, [Syntax.KorePattern])
         )
 internalisePatternOrTopOrBottom allowAlias checkSubsorts sortVars definition existentials p = do
     let exploded = explodeAnd p
@@ -221,8 +233,12 @@ internalisePatternOrTopOrBottom allowAlias checkSubsorts sortVars definition exi
                 pure $
                     IsPattern
                         ( existentialVars
-                        , Internal.Pattern{term, constraints = Set.fromList preds, ceilConditions}
-                        , subst
+                        , Internal.Pattern
+                            { term = Internal.substituteInTerm subst term
+                            , constraints = Set.map (Internal.substituteInPredicate subst) . Set.fromList $ preds
+                            , ceilConditions
+                            , substitution = subst
+                            }
                         , unknown
                         )
   where
@@ -236,6 +252,15 @@ internalisePatternOrTopOrBottom allowAlias checkSubsorts sortVars definition exi
         Syntax.KJBottom{sort} : _ -> Just $ IsBottom sort
         _ : xs -> isBottom xs
 
+{- | Internalise a @'Syntax.KorePattern'@ into either @'Internal.Pattern'@
+     or @'[InternalisedPredicates]'@ if only terms of sort bool are present.
+
+     Note: If this function successfully internalises a @'Internal.Pattern'@, it will apply the
+           @'Internal.Substitution'@ part to the term and constraints (but not the ceils).
+
+           Otherwise, when we get predicates only, the substitution part
+           is not applied to the rest of the predicates.
+-}
 internaliseTermOrPredicate ::
     Flag "alias" ->
     Flag "subsorts" ->
@@ -252,8 +277,12 @@ internaliseTermOrPredicate allowAlias checkSubsorts sortVars definition syntaxPa
                     internalisePattern allowAlias checkSubsorts sortVars definition syntaxPatt
                 pure $
                     TermAndPredicates
-                        Internal.Pattern{term, constraints = Set.fromList constrs, ceilConditions}
-                        substitution
+                        Internal.Pattern
+                            { term = Internal.substituteInTerm substitution term
+                            , constraints = Set.map (Internal.substituteInPredicate substitution) . Set.fromList $ constrs
+                            , ceilConditions
+                            , substitution
+                            }
                         unsupported
             )
 
@@ -458,7 +487,7 @@ mkSubstitution initialSubst =
             Map.partition ((== 1) . length) $
                 Map.fromListWith (<>) [(v, [t]) | SubstitutionPred v t <- initialSubst]
         equations =
-            [mkEq v t | (v, ts) <- Map.assocs duplicates, t <- ts]
+            [Internal.mkEq v t | (v, ts) <- Map.assocs duplicates, t <- ts]
      in execState breakCycles (Map.map head substMap, equations)
   where
     breakCycles :: State (Map Internal.Variable Internal.Term, [Internal.Predicate]) ()
@@ -472,19 +501,53 @@ mkSubstitution initialSubst =
             else do
                 modify $ \(m, eqs) ->
                     ( m `Map.withoutKeys` cycleNodes
-                    , eqs <> (map (uncurry mkEq) $ Map.assocs $ m `Map.restrictKeys` cycleNodes)
+                    , eqs <> (map (uncurry Internal.mkEq) $ Map.assocs $ m `Map.restrictKeys` cycleNodes)
                     )
                 breakCycles
 
-mkEq :: Internal.Variable -> Internal.Term -> Internal.Predicate
-mkEq x t = Internal.Predicate $ case sortOfTerm t of
-    Internal.SortInt -> Internal.EqualsInt (Internal.Var x) t
-    Internal.SortBool -> Internal.EqualsBool (Internal.Var x) t
-    otherSort -> Internal.EqualsK (Internal.KSeq otherSort (Internal.Var x)) (Internal.KSeq otherSort t)
+-- | Given a equality @'Term'@, decide if it can be interpreted as substitution.
+mbSubstitution ::
+    Internal.Term -> InternalisedPredicate
+mbSubstitution = \case
+    eq@(Internal.EqualsInt (Internal.Var x) e)
+        | x `Set.member` freeVariables e -> boolPred eq
+        | otherwise -> SubstitutionPred x e
+    eq@(Internal.EqualsInt e (Internal.Var x))
+        | x `Set.member` freeVariables e -> boolPred eq
+        | otherwise -> SubstitutionPred x e
+    eq@(Internal.EqualsK (Internal.KSeq _sortL (Internal.Var x)) (Internal.KSeq _sortR e)) ->
+        do
+            -- NB sorts do not have to agree! (could be subsorts)
+            if (x `Set.member` freeVariables e)
+                then boolPred eq
+                else SubstitutionPred x e
+    eq@(Internal.EqualsK (Internal.KSeq _sortL e) (Internal.KSeq _sortR (Internal.Var x))) ->
+        do
+            -- NB sorts do not have to agree! (could be subsorts)
+            if (x `Set.member` freeVariables e)
+                then boolPred eq
+                else SubstitutionPred x e
+    other ->
+        boolPred other
+  where
+    boolPred = BoolPred . Internal.Predicate
 
--- | turns a substitution into a list of equations
-asEquations :: Map Internal.Variable Internal.Term -> [Internal.Predicate]
-asEquations = map (uncurry mkEq) . Map.assocs
+extractSubstitution ::
+    [Internal.Predicate] -> (Map Internal.Variable Internal.Term, Set Internal.Predicate)
+extractSubstitution ps =
+    let (potentialSubstitution, otherPreds) = partitionSubstitutionPreds . map mbSubstitution . coerce $ ps
+        (newSubstitution, leftoverPreds) = mkSubstitution potentialSubstitution
+     in (newSubstitution, Set.fromList $ leftoverPreds <> otherPreds)
+  where
+    partitionSubstitutionPreds = partitionEithers . map unpackBoolPred
+      where
+        unpackBoolPred :: InternalisedPredicate -> Either InternalisedPredicate Internal.Predicate
+        unpackBoolPred = \case
+            pSubst@SubstitutionPred{} -> Left pSubst
+            BoolPred p -> Right p
+            other ->
+                -- this case is impossible the input is a valid Internal.Predicate
+                error $ "extractSubstitution: unsupported predicate " <> show other
 
 internalisePred ::
     Flag "alias" ->
@@ -547,9 +610,9 @@ internalisePred allowAlias checkSubsorts sortVars definition@KoreDefinition{sort
                 case (argS, a, b) of
                     -- for "true" #Equals P, check whether P is in fact a substitution
                     (Internal.SortBool, Internal.TrueBool, x) ->
-                        mapM mbSubstitution [x]
+                        pure [mbSubstitution x]
                     (Internal.SortBool, x, Internal.TrueBool) ->
-                        mapM mbSubstitution [x]
+                        pure [mbSubstitution x]
                     -- we could also detect NotBool (NEquals _) in "false" #Equals P
                     (Internal.SortBool, Internal.FalseBool, x) ->
                         pure [BoolPred $ Internal.Predicate $ Internal.NotBool x]
@@ -557,12 +620,12 @@ internalisePred allowAlias checkSubsorts sortVars definition@KoreDefinition{sort
                         pure [BoolPred $ Internal.Predicate $ Internal.NotBool x]
                     (_, Internal.Var x, t)
                         | x `Set.member` freeVariables t ->
-                            pure [BoolPred $ mkEq x t]
+                            pure [BoolPred $ Internal.mkEq x t]
                         | otherwise ->
                             pure [SubstitutionPred x t]
                     (_, t, Internal.Var x)
                         | x `Set.member` freeVariables t ->
-                            pure [BoolPred $ mkEq x t]
+                            pure [BoolPred $ Internal.mkEq x t]
                         | otherwise ->
                             pure [SubstitutionPred x t]
                     (Internal.SortInt, _, _) ->
@@ -607,33 +670,6 @@ internalisePred allowAlias checkSubsorts sortVars definition@KoreDefinition{sort
                         throwE (IncompatibleSorts (map externaliseSort [s1, s2]))
                     zipWithM_ go args1 args2
 
-    mbSubstitution :: Internal.Term -> Except PatternError InternalisedPredicate
-    mbSubstitution = \case
-        eq@(Internal.EqualsInt (Internal.Var x) e)
-            | x `Set.member` freeVariables e -> pure $ boolPred eq
-            | otherwise -> pure $ SubstitutionPred x e
-        eq@(Internal.EqualsInt e (Internal.Var x))
-            | x `Set.member` freeVariables e -> pure $ boolPred eq
-            | otherwise -> pure $ SubstitutionPred x e
-        eq@(Internal.EqualsK (Internal.KSeq _sortL (Internal.Var x)) (Internal.KSeq _sortR e)) ->
-            do
-                -- NB sorts do not have to agree! (could be subsorts)
-                pure $
-                    if (x `Set.member` freeVariables e)
-                        then boolPred eq
-                        else SubstitutionPred x e
-        eq@(Internal.EqualsK (Internal.KSeq _sortL e) (Internal.KSeq _sortR (Internal.Var x))) ->
-            do
-                -- NB sorts do not have to agree! (could be subsorts)
-                pure $
-                    if (x `Set.member` freeVariables e)
-                        then boolPred eq
-                        else SubstitutionPred x e
-        other ->
-            pure $ boolPred other
-
-    boolPred = BoolPred . Internal.Predicate
-
 ----------------------------------------
 
 -- for use with withAssoc
diff --git a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs
index 5c258cba73..4031315d62 100644
--- a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs
+++ b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs
@@ -57,6 +57,7 @@ import Booster.Pattern.Base qualified as Def.Symbol (Symbol (..))
 import Booster.Pattern.Bool (foldAndBool, pattern TrueBool)
 import Booster.Pattern.Index as Idx
 import Booster.Pattern.Pretty
+import Booster.Pattern.Substitution qualified as Substitution
 import Booster.Pattern.Util qualified as Util
 import Booster.Prettyprinter hiding (attributes)
 import Booster.Syntax.Json.Internalise
@@ -765,18 +766,20 @@ internaliseAxiom (Partial partialDefinition) parsedAxiom =
                     sortVars
                     attribs
 
-{- | internalises a pattern and turns its contained substitution into
-   equations (predicates). Errors if any ceil conditions or
-   unsupported predicates are found.
+{- | Internalises a pattern to be used as a rule left/right-hand side.
+
+     Turns its contained substitution into predicates.
+
+     Errors if any ceil conditions or unsupported predicates are found.
 -}
-internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported ::
+internaliseRulePattern ::
     KoreDefinition ->
     SourceRef ->
     Maybe [Id] ->
     (Variable -> Variable) ->
     Syntax.KorePattern ->
     Except DefinitionError (Def.Term, [Predicate])
-internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported partialDefinition ref maybeVars f t = do
+internaliseRulePattern partialDefinition ref maybeVars f t = do
     (term, preds, ceilConditions, substitution, unsupported) <-
         withExcept (DefinitionPatternError ref) $
             internalisePattern AllowAlias IgnoreSubsorts maybeVars partialDefinition t
@@ -788,7 +791,7 @@ internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported partialDefinition ref
             DefinitionPatternError ref (NotSupported (head unsupported))
     pure
         ( Util.modifyVariablesInT f term
-        , map (Util.modifyVariablesInP f) (preds <> asEquations substitution)
+        , map (Util.modifyVariablesInP f) (preds <> Substitution.asEquations substitution)
         )
 
 internaliseRewriteRuleNoAlias ::
@@ -805,7 +808,7 @@ internaliseRewriteRuleNoAlias partialDefinition exs left right axAttributes = do
     -- to avoid name clashes with patterns from the user;
     -- filter out literal `Top` constraints
     (lhs, requires) <-
-        internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported
+        internaliseRulePattern
             partialDefinition
             ref
             Nothing
@@ -816,7 +819,7 @@ internaliseRewriteRuleNoAlias partialDefinition exs left right axAttributes = do
             | v `Set.member` existentials' = Util.modifyVarName Util.markAsExVar v
             | otherwise = Util.modifyVarName Util.markAsRuleVar v
     (rhs, ensures) <-
-        internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported
+        internaliseRulePattern
             partialDefinition
             ref
             Nothing
@@ -872,14 +875,14 @@ internaliseSimpleEquation partialDef precond left right sortVars attrs
     | Syntax.KJApp{} <- left = do
         -- this ensures that `left` is a _term_ (invariant guarded by classifyAxiom)
         (lhs, requires) <-
-            internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported
+            internaliseRulePattern
                 partialDef
                 (sourceRef attrs)
                 (Just sortVars)
                 (Util.modifyVarName ("Eq#" <>))
                 $ Syntax.KJAnd left.sort [left, precond]
         (rhs, ensures) <-
-            internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported
+            internaliseRulePattern
                 partialDef
                 (sourceRef attrs)
                 (Just sortVars)
@@ -931,7 +934,7 @@ internaliseCeil ::
 internaliseCeil partialDef left right sortVars attrs = do
     -- this ensures that `left` is a _term_ (invariant guarded by classifyAxiom)
     (lhs, _) <-
-        internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported
+        internaliseRulePattern
             partialDef
             (sourceRef attrs)
             (Just sortVars)
@@ -970,7 +973,7 @@ internaliseCeil partialDef left right sortVars attrs = do
                 internalisePredicates AllowAlias IgnoreSubsorts (Just sortVars) partialDef [p]
         let
             -- turn substitution-like predicates back into equations
-            constraints = internalPs.boolPredicates <> asEquations internalPs.substitution
+            constraints = internalPs.boolPredicates <> Substitution.asEquations internalPs.substitution
             unsupported = internalPs.unsupported
         unless (null unsupported) $
             throwE $
@@ -1017,9 +1020,9 @@ internaliseFunctionEquation partialDef requires args leftTerm right sortVars att
     argPairs <- mapM internaliseArg args
     let lhs =
             Util.modifyVariablesInT (Util.modifyVarName ("Eq#" <>)) $
-                Util.substituteInTerm (Map.fromList argPairs) left
+                Substitution.substituteInTerm (Map.fromList argPairs) left
     (rhs, ensures) <-
-        internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported
+        internaliseRulePattern
             partialDef
             (sourceRef attrs)
             (Just sortVars)
@@ -1049,7 +1052,9 @@ internaliseFunctionEquation partialDef requires args leftTerm right sortVars att
                 { lhs
                 , rhs
                 , requires =
-                    map (Util.modifyVariablesInP $ Util.modifyVarName ("Eq#" <>)) (preds <> asEquations substitution)
+                    map
+                        (Util.modifyVariablesInP $ Util.modifyVarName ("Eq#" <>))
+                        (preds <> Substitution.asEquations substitution)
                 , ensures
                 , attributes
                 , computedAttributes
diff --git a/booster/test/rpc-integration/test-a-to-f/response-branching.kore-rpc-dev b/booster/test/rpc-integration/test-a-to-f/response-branching.kore-rpc-dev
deleted file mode 100644
index 0d2f7baef6..0000000000
--- a/booster/test/rpc-integration/test-a-to-f/response-branching.kore-rpc-dev
+++ /dev/null
@@ -1,400 +0,0 @@
-{
-    "jsonrpc": "2.0",
-    "id": 1,
-    "result": {
-        "reason": "branching",
-        "depth": 0,
-        "state": {
-            "term": {
-                "format": "KORE",
-                "version": 1,
-                "term": {
-                    "tag": "App",
-                    "name": "Lbl'-LT-'generatedTop'-GT-'",
-                    "sorts": [],
-                    "args": [
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'k'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "App",
-                                    "name": "kseq",
-                                    "sorts": [],
-                                    "args": [
-                                        {
-                                            "tag": "App",
-                                            "name": "inj",
-                                            "sorts": [
-                                                {
-                                                    "tag": "SortApp",
-                                                    "name": "SortState",
-                                                    "args": []
-                                                },
-                                                {
-                                                    "tag": "SortApp",
-                                                    "name": "SortKItem",
-                                                    "args": []
-                                                }
-                                            ],
-                                            "args": [
-                                                {
-                                                    "tag": "DV",
-                                                    "sort": {
-                                                        "tag": "SortApp",
-                                                        "name": "SortState",
-                                                        "args": []
-                                                    },
-                                                    "value": "a"
-                                                }
-                                            ]
-                                        },
-                                        {
-                                            "tag": "App",
-                                            "name": "dotk",
-                                            "sorts": [],
-                                            "args": []
-                                        }
-                                    ]
-                                }
-                            ]
-                        },
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'generatedCounter'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "DV",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortInt",
-                                        "args": []
-                                    },
-                                    "value": "0"
-                                }
-                            ]
-                        }
-                    ]
-                }
-            }
-        },
-        "next-states": [
-            {
-                "term": {
-                    "format": "KORE",
-                    "version": 1,
-                    "term": {
-                        "tag": "App",
-                        "name": "Lbl'-LT-'generatedTop'-GT-'",
-                        "sorts": [],
-                        "args": [
-                            {
-                                "tag": "App",
-                                "name": "Lbl'-LT-'k'-GT-'",
-                                "sorts": [],
-                                "args": [
-                                    {
-                                        "tag": "App",
-                                        "name": "kseq",
-                                        "sorts": [],
-                                        "args": [
-                                            {
-                                                "tag": "App",
-                                                "name": "inj",
-                                                "sorts": [
-                                                    {
-                                                        "tag": "SortApp",
-                                                        "name": "SortState",
-                                                        "args": []
-                                                    },
-                                                    {
-                                                        "tag": "SortApp",
-                                                        "name": "SortKItem",
-                                                        "args": []
-                                                    }
-                                                ],
-                                                "args": [
-                                                    {
-                                                        "tag": "DV",
-                                                        "sort": {
-                                                            "tag": "SortApp",
-                                                            "name": "SortState",
-                                                            "args": []
-                                                        },
-                                                        "value": "c"
-                                                    }
-                                                ]
-                                            },
-                                            {
-                                                "tag": "App",
-                                                "name": "dotk",
-                                                "sorts": [],
-                                                "args": []
-                                            }
-                                        ]
-                                    }
-                                ]
-                            },
-                            {
-                                "tag": "App",
-                                "name": "Lbl'-LT-'generatedCounter'-GT-'",
-                                "sorts": [],
-                                "args": [
-                                    {
-                                        "tag": "DV",
-                                        "sort": {
-                                            "tag": "SortApp",
-                                            "name": "SortInt",
-                                            "args": []
-                                        },
-                                        "value": "0"
-                                    }
-                                ]
-                            }
-                        ]
-                    }
-                },
-                "rule-id": "3cfae148c63f879628626da1753b07d517f6ac9b414543f7dd8f7b3e8e19329e",
-                "rule-substitution": {
-                    "format": "KORE",
-                    "version": 1,
-                    "term": {
-                        "tag": "And",
-                        "sort": {
-                            "tag": "SortApp",
-                            "name": "SortGeneratedTopCell",
-                            "args": []
-                        },
-                        "patterns": [
-                            {
-                                "tag": "Equals",
-                                "argSort": {
-                                    "tag": "SortApp",
-                                    "name": "SortGeneratedCounterCell",
-                                    "args": []
-                                },
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortGeneratedTopCell",
-                                    "args": []
-                                },
-                                "first": {
-                                    "tag": "EVar",
-                                    "name": "RuleVar'Unds'DotVar0",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortGeneratedCounterCell",
-                                        "args": []
-                                    }
-                                },
-                                "second": {
-                                    "tag": "App",
-                                    "name": "Lbl'-LT-'generatedCounter'-GT-'",
-                                    "sorts": [],
-                                    "args": [
-                                        {
-                                            "tag": "DV",
-                                            "sort": {
-                                                "tag": "SortApp",
-                                                "name": "SortInt",
-                                                "args": []
-                                            },
-                                            "value": "0"
-                                        }
-                                    ]
-                                }
-                            },
-                            {
-                                "tag": "Equals",
-                                "argSort": {
-                                    "tag": "SortApp",
-                                    "name": "SortK",
-                                    "args": []
-                                },
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortGeneratedTopCell",
-                                    "args": []
-                                },
-                                "first": {
-                                    "tag": "EVar",
-                                    "name": "RuleVar'Unds'DotVar1",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortK",
-                                        "args": []
-                                    }
-                                },
-                                "second": {
-                                    "tag": "App",
-                                    "name": "dotk",
-                                    "sorts": [],
-                                    "args": []
-                                }
-                            }
-                        ]
-                    }
-                }
-            },
-            {
-                "term": {
-                    "format": "KORE",
-                    "version": 1,
-                    "term": {
-                        "tag": "App",
-                        "name": "Lbl'-LT-'generatedTop'-GT-'",
-                        "sorts": [],
-                        "args": [
-                            {
-                                "tag": "App",
-                                "name": "Lbl'-LT-'k'-GT-'",
-                                "sorts": [],
-                                "args": [
-                                    {
-                                        "tag": "App",
-                                        "name": "kseq",
-                                        "sorts": [],
-                                        "args": [
-                                            {
-                                                "tag": "App",
-                                                "name": "inj",
-                                                "sorts": [
-                                                    {
-                                                        "tag": "SortApp",
-                                                        "name": "SortState",
-                                                        "args": []
-                                                    },
-                                                    {
-                                                        "tag": "SortApp",
-                                                        "name": "SortKItem",
-                                                        "args": []
-                                                    }
-                                                ],
-                                                "args": [
-                                                    {
-                                                        "tag": "DV",
-                                                        "sort": {
-                                                            "tag": "SortApp",
-                                                            "name": "SortState",
-                                                            "args": []
-                                                        },
-                                                        "value": "b"
-                                                    }
-                                                ]
-                                            },
-                                            {
-                                                "tag": "App",
-                                                "name": "dotk",
-                                                "sorts": [],
-                                                "args": []
-                                            }
-                                        ]
-                                    }
-                                ]
-                            },
-                            {
-                                "tag": "App",
-                                "name": "Lbl'-LT-'generatedCounter'-GT-'",
-                                "sorts": [],
-                                "args": [
-                                    {
-                                        "tag": "DV",
-                                        "sort": {
-                                            "tag": "SortApp",
-                                            "name": "SortInt",
-                                            "args": []
-                                        },
-                                        "value": "0"
-                                    }
-                                ]
-                            }
-                        ]
-                    }
-                },
-                "rule-id": "aba8479fef763c749fa1a1837f2591f85d8541ca8837c738cf586de790c6f8b8",
-                "rule-substitution": {
-                    "format": "KORE",
-                    "version": 1,
-                    "term": {
-                        "tag": "And",
-                        "sort": {
-                            "tag": "SortApp",
-                            "name": "SortGeneratedTopCell",
-                            "args": []
-                        },
-                        "patterns": [
-                            {
-                                "tag": "Equals",
-                                "argSort": {
-                                    "tag": "SortApp",
-                                    "name": "SortGeneratedCounterCell",
-                                    "args": []
-                                },
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortGeneratedTopCell",
-                                    "args": []
-                                },
-                                "first": {
-                                    "tag": "EVar",
-                                    "name": "RuleVar'Unds'DotVar0",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortGeneratedCounterCell",
-                                        "args": []
-                                    }
-                                },
-                                "second": {
-                                    "tag": "App",
-                                    "name": "Lbl'-LT-'generatedCounter'-GT-'",
-                                    "sorts": [],
-                                    "args": [
-                                        {
-                                            "tag": "DV",
-                                            "sort": {
-                                                "tag": "SortApp",
-                                                "name": "SortInt",
-                                                "args": []
-                                            },
-                                            "value": "0"
-                                        }
-                                    ]
-                                }
-                            },
-                            {
-                                "tag": "Equals",
-                                "argSort": {
-                                    "tag": "SortApp",
-                                    "name": "SortK",
-                                    "args": []
-                                },
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortGeneratedTopCell",
-                                    "args": []
-                                },
-                                "first": {
-                                    "tag": "EVar",
-                                    "name": "RuleVar'Unds'DotVar1",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortK",
-                                        "args": []
-                                    }
-                                },
-                                "second": {
-                                    "tag": "App",
-                                    "name": "dotk",
-                                    "sorts": [],
-                                    "args": []
-                                }
-                            }
-                        ]
-                    }
-                }
-            }
-        ]
-    }
-}
\ No newline at end of file
diff --git a/booster/test/rpc-integration/test-diamond/response-infeasible-branching.booster-dev b/booster/test/rpc-integration/test-diamond/response-infeasible-branching.booster-dev
index ce99ad8ff6..c96f33b892 100644
--- a/booster/test/rpc-integration/test-diamond/response-infeasible-branching.booster-dev
+++ b/booster/test/rpc-integration/test-diamond/response-infeasible-branching.booster-dev
@@ -67,13 +67,13 @@
                             "sorts": [],
                             "args": [
                                 {
-                                    "tag": "EVar",
-                                    "name": "X",
+                                    "tag": "DV",
                                     "sort": {
                                         "tag": "SortApp",
                                         "name": "SortInt",
                                         "args": []
-                                    }
+                                    },
+                                    "value": "42"
                                 }
                             ]
                         },
@@ -96,14 +96,14 @@
                     ]
                 }
             },
-            "predicate": {
+            "substitution": {
                 "format": "KORE",
                 "version": 1,
                 "term": {
                     "tag": "Equals",
                     "argSort": {
                         "tag": "SortApp",
-                        "name": "SortBool",
+                        "name": "SortInt",
                         "args": []
                     },
                     "sort": {
@@ -112,38 +112,22 @@
                         "args": []
                     },
                     "first": {
-                        "tag": "DV",
+                        "tag": "EVar",
+                        "name": "X",
                         "sort": {
                             "tag": "SortApp",
-                            "name": "SortBool",
+                            "name": "SortInt",
                             "args": []
-                        },
-                        "value": "true"
+                        }
                     },
                     "second": {
-                        "tag": "App",
-                        "name": "Lbl'UndsEqlsEqls'Int'Unds'",
-                        "sorts": [],
-                        "args": [
-                            {
-                                "tag": "EVar",
-                                "name": "X",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortInt",
-                                    "args": []
-                                }
-                            },
-                            {
-                                "tag": "DV",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortInt",
-                                    "args": []
-                                },
-                                "value": "42"
-                            }
-                        ]
+                        "tag": "DV",
+                        "sort": {
+                            "tag": "SortApp",
+                            "name": "SortInt",
+                            "args": []
+                        },
+                        "value": "42"
                     }
                 }
             }
diff --git a/booster/test/rpc-integration/test-diamond/response-mutual-constraints-stuck.booster-dev b/booster/test/rpc-integration/test-diamond/response-mutual-constraints-stuck.booster-dev
deleted file mode 100644
index 12b421e0d0..0000000000
--- a/booster/test/rpc-integration/test-diamond/response-mutual-constraints-stuck.booster-dev
+++ /dev/null
@@ -1,134 +0,0 @@
-{
-    "jsonrpc": "2.0",
-    "id": 1,
-    "result": {
-        "reason": "stuck",
-        "depth": 2,
-        "state": {
-            "term": {
-                "format": "KORE",
-                "version": 1,
-                "term": {
-                    "tag": "App",
-                    "name": "Lbl'-LT-'generatedTop'-GT-'",
-                    "sorts": [],
-                    "args": [
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'k'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "App",
-                                    "name": "kseq",
-                                    "sorts": [],
-                                    "args": [
-                                        {
-                                            "tag": "App",
-                                            "name": "inj",
-                                            "sorts": [
-                                                {
-                                                    "tag": "SortApp",
-                                                    "name": "SortState",
-                                                    "args": []
-                                                },
-                                                {
-                                                    "tag": "SortApp",
-                                                    "name": "SortKItem",
-                                                    "args": []
-                                                }
-                                            ],
-                                            "args": [
-                                                {
-                                                    "tag": "DV",
-                                                    "sort": {
-                                                        "tag": "SortApp",
-                                                        "name": "SortState",
-                                                        "args": []
-                                                    },
-                                                    "value": "g"
-                                                }
-                                            ]
-                                        },
-                                        {
-                                            "tag": "App",
-                                            "name": "dotk",
-                                            "sorts": [],
-                                            "args": []
-                                        }
-                                    ]
-                                }
-                            ]
-                        },
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'int'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "EVar",
-                                    "name": "X",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortInt",
-                                        "args": []
-                                    }
-                                }
-                            ]
-                        },
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'generatedCounter'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "DV",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortInt",
-                                        "args": []
-                                    },
-                                    "value": "0"
-                                }
-                            ]
-                        }
-                    ]
-                }
-            }
-        },
-        "logs": [
-            {
-                "tag": "rewrite",
-                "origin": "booster",
-                "result": {
-                    "tag": "success",
-                    "rule-id": "928fbc2c9e62487c0fdc40fb4eeff63c14c06f9cd3e4bdde5c62be73b318d352"
-                }
-            },
-            {
-                "tag": "rewrite",
-                "origin": "booster",
-                "result": {
-                    "tag": "success",
-                    "rule-id": "51a4003346d710ea028036ee9bdeaf964113e46e843a8c8f15a8f0f886be1fcf"
-                }
-            },
-            {
-                "tag": "rewrite",
-                "origin": "booster",
-                "result": {
-                    "tag": "failure",
-                    "reason": "No applicable rules found"
-                }
-            },
-            {
-                "tag": "rewrite",
-                "origin": "booster",
-                "result": {
-                    "tag": "failure",
-                    "reason": "No applicable rules found"
-                }
-            }
-        ]
-    }
-}
\ No newline at end of file
diff --git a/booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal.booster-dev b/booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal.booster-dev
deleted file mode 100644
index 92827d7008..0000000000
--- a/booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal.booster-dev
+++ /dev/null
@@ -1,119 +0,0 @@
-{
-    "jsonrpc": "2.0",
-    "id": 1,
-    "result": {
-        "reason": "terminal-rule",
-        "depth": 2,
-        "rule": "TEST.FG",
-        "state": {
-            "term": {
-                "format": "KORE",
-                "version": 1,
-                "term": {
-                    "tag": "App",
-                    "name": "Lbl'-LT-'generatedTop'-GT-'",
-                    "sorts": [],
-                    "args": [
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'k'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "App",
-                                    "name": "kseq",
-                                    "sorts": [],
-                                    "args": [
-                                        {
-                                            "tag": "App",
-                                            "name": "inj",
-                                            "sorts": [
-                                                {
-                                                    "tag": "SortApp",
-                                                    "name": "SortState",
-                                                    "args": []
-                                                },
-                                                {
-                                                    "tag": "SortApp",
-                                                    "name": "SortKItem",
-                                                    "args": []
-                                                }
-                                            ],
-                                            "args": [
-                                                {
-                                                    "tag": "DV",
-                                                    "sort": {
-                                                        "tag": "SortApp",
-                                                        "name": "SortState",
-                                                        "args": []
-                                                    },
-                                                    "value": "g"
-                                                }
-                                            ]
-                                        },
-                                        {
-                                            "tag": "App",
-                                            "name": "dotk",
-                                            "sorts": [],
-                                            "args": []
-                                        }
-                                    ]
-                                }
-                            ]
-                        },
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'int'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "EVar",
-                                    "name": "X",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortInt",
-                                        "args": []
-                                    }
-                                }
-                            ]
-                        },
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'generatedCounter'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "DV",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortInt",
-                                        "args": []
-                                    },
-                                    "value": "0"
-                                }
-                            ]
-                        }
-                    ]
-                }
-            }
-        },
-        "logs": [
-            {
-                "tag": "rewrite",
-                "origin": "booster",
-                "result": {
-                    "tag": "success",
-                    "rule-id": "928fbc2c9e62487c0fdc40fb4eeff63c14c06f9cd3e4bdde5c62be73b318d352"
-                }
-            },
-            {
-                "tag": "rewrite",
-                "origin": "booster",
-                "result": {
-                    "tag": "success",
-                    "rule-id": "51a4003346d710ea028036ee9bdeaf964113e46e843a8c8f15a8f0f886be1fcf"
-                }
-            }
-        ]
-    }
-}
\ No newline at end of file
diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.json b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.json
index 44aefb1934..812dbd3a09 100644
--- a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.json
+++ b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.json
@@ -86,73 +86,63 @@
                     },
                     "patterns": [
                         {
-                            "tag": "And",
+                            "tag": "Equals",
+                            "argSort": {
+                                "tag": "SortApp",
+                                "name": "SortState",
+                                "args": []
+                            },
                             "sort": {
                                 "tag": "SortApp",
                                 "name": "SortGeneratedTopCell",
                                 "args": []
                             },
-                            "patterns": [
-                                {
-                                    "tag": "Equals",
-                                    "argSort": {
-                                        "tag": "SortApp",
-                                        "name": "SortState",
-                                        "args": []
-                                    },
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortGeneratedTopCell",
-                                        "args": []
-                                    },
-                                    "first": {
-                                        "tag": "EVar",
-                                        "name": "Var'Ques'X",
-                                        "sort": {
-                                            "tag": "SortApp",
-                                            "name": "SortState",
-                                            "args": []
-                                        }
-                                    },
-                                    "second": {
-                                        "tag": "App",
-                                        "name": "Lblb'Unds'QUESTIONMARK-VARS'Unds'State",
-                                        "sorts": [],
-                                        "args": []
-                                    }
-                                },
-                                {
-                                    "tag": "Equals",
-                                    "argSort": {
-                                        "tag": "SortApp",
-                                        "name": "SortState",
-                                        "args": []
-                                    },
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortGeneratedTopCell",
-                                        "args": []
-                                    },
-                                    "first": {
-                                        "tag": "EVar",
-                                        "name": "Var'Ques'X0",
-                                        "sort": {
-                                            "tag": "SortApp",
-                                            "name": "SortState",
-                                            "args": []
-                                        }
-                                    },
-                                    "second": {
-                                        "tag": "EVar",
-                                        "name": "Var'Ques'X1",
-                                        "sort": {
-                                            "tag": "SortApp",
-                                            "name": "SortState",
-                                            "args": []
-                                        }
-                                    }
+                            "first": {
+                                "tag": "EVar",
+                                "name": "Var'Ques'X",
+                                "sort": {
+                                    "tag": "SortApp",
+                                    "name": "SortState",
+                                    "args": []
                                 }
-                            ]
+                            },
+                            "second": {
+                                "tag": "App",
+                                "name": "Lblb'Unds'QUESTIONMARK-VARS'Unds'State",
+                                "sorts": [],
+                                "args": []
+                            }
+                        },
+                        {
+                            "tag": "Equals",
+                            "argSort": {
+                                "tag": "SortApp",
+                                "name": "SortState",
+                                "args": []
+                            },
+                            "sort": {
+                                "tag": "SortApp",
+                                "name": "SortGeneratedTopCell",
+                                "args": []
+                            },
+                            "first": {
+                                "tag": "EVar",
+                                "name": "Var'Ques'X0",
+                                "sort": {
+                                    "tag": "SortApp",
+                                    "name": "SortState",
+                                    "args": []
+                                }
+                            },
+                            "second": {
+                                "tag": "EVar",
+                                "name": "Var'Ques'X1",
+                                "sort": {
+                                    "tag": "SortApp",
+                                    "name": "SortState",
+                                    "args": []
+                                }
+                            }
                         },
                         {
                             "tag": "Equals",
diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.booster-dev b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.kore-rpc-dev
similarity index 67%
rename from booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.booster-dev
rename to booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.kore-rpc-dev
index 812dbd3a09..44aefb1934 100644
--- a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.booster-dev
+++ b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.kore-rpc-dev
@@ -86,63 +86,73 @@
                     },
                     "patterns": [
                         {
-                            "tag": "Equals",
-                            "argSort": {
-                                "tag": "SortApp",
-                                "name": "SortState",
-                                "args": []
-                            },
+                            "tag": "And",
                             "sort": {
                                 "tag": "SortApp",
                                 "name": "SortGeneratedTopCell",
                                 "args": []
                             },
-                            "first": {
-                                "tag": "EVar",
-                                "name": "Var'Ques'X",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortState",
-                                    "args": []
-                                }
-                            },
-                            "second": {
-                                "tag": "App",
-                                "name": "Lblb'Unds'QUESTIONMARK-VARS'Unds'State",
-                                "sorts": [],
-                                "args": []
-                            }
-                        },
-                        {
-                            "tag": "Equals",
-                            "argSort": {
-                                "tag": "SortApp",
-                                "name": "SortState",
-                                "args": []
-                            },
-                            "sort": {
-                                "tag": "SortApp",
-                                "name": "SortGeneratedTopCell",
-                                "args": []
-                            },
-                            "first": {
-                                "tag": "EVar",
-                                "name": "Var'Ques'X0",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortState",
-                                    "args": []
-                                }
-                            },
-                            "second": {
-                                "tag": "EVar",
-                                "name": "Var'Ques'X1",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortState",
-                                    "args": []
+                            "patterns": [
+                                {
+                                    "tag": "Equals",
+                                    "argSort": {
+                                        "tag": "SortApp",
+                                        "name": "SortState",
+                                        "args": []
+                                    },
+                                    "sort": {
+                                        "tag": "SortApp",
+                                        "name": "SortGeneratedTopCell",
+                                        "args": []
+                                    },
+                                    "first": {
+                                        "tag": "EVar",
+                                        "name": "Var'Ques'X",
+                                        "sort": {
+                                            "tag": "SortApp",
+                                            "name": "SortState",
+                                            "args": []
+                                        }
+                                    },
+                                    "second": {
+                                        "tag": "App",
+                                        "name": "Lblb'Unds'QUESTIONMARK-VARS'Unds'State",
+                                        "sorts": [],
+                                        "args": []
+                                    }
+                                },
+                                {
+                                    "tag": "Equals",
+                                    "argSort": {
+                                        "tag": "SortApp",
+                                        "name": "SortState",
+                                        "args": []
+                                    },
+                                    "sort": {
+                                        "tag": "SortApp",
+                                        "name": "SortGeneratedTopCell",
+                                        "args": []
+                                    },
+                                    "first": {
+                                        "tag": "EVar",
+                                        "name": "Var'Ques'X0",
+                                        "sort": {
+                                            "tag": "SortApp",
+                                            "name": "SortState",
+                                            "args": []
+                                        }
+                                    },
+                                    "second": {
+                                        "tag": "EVar",
+                                        "name": "Var'Ques'X1",
+                                        "sort": {
+                                            "tag": "SortApp",
+                                            "name": "SortState",
+                                            "args": []
+                                        }
+                                    }
                                 }
-                            }
+                            ]
                         },
                         {
                             "tag": "Equals",
diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques.booster-dev b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques.json
similarity index 100%
rename from booster/test/rpc-integration/test-questionmark-vars/response-one-ques.booster-dev
rename to booster/test/rpc-integration/test-questionmark-vars/response-one-ques.json
diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques.kore-rpc-dev b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques.kore-rpc-dev
deleted file mode 100644
index 8852423b90..0000000000
--- a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques.kore-rpc-dev
+++ /dev/null
@@ -1,121 +0,0 @@
-{
-    "jsonrpc": "2.0",
-    "id": 1,
-    "result": {
-        "reason": "stuck",
-        "depth": 1,
-        "state": {
-            "term": {
-                "format": "KORE",
-                "version": 1,
-                "term": {
-                    "tag": "App",
-                    "name": "Lbl'-LT-'generatedTop'-GT-'",
-                    "sorts": [],
-                    "args": [
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'k'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "App",
-                                    "name": "dotk",
-                                    "sorts": [],
-                                    "args": []
-                                }
-                            ]
-                        },
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'a-state'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "EVar",
-                                    "name": "Var'Ques'X",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortState",
-                                        "args": []
-                                    }
-                                }
-                            ]
-                        },
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'b-state'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "App",
-                                    "name": "Lbl'Stop'State'Unds'QUESTIONMARK-VARS'Unds'State",
-                                    "sorts": [],
-                                    "args": []
-                                }
-                            ]
-                        },
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'generatedCounter'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "DV",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortInt",
-                                        "args": []
-                                    },
-                                    "value": "0"
-                                }
-                            ]
-                        }
-                    ]
-                }
-            },
-            "predicate": {
-                "format": "KORE",
-                "version": 1,
-                "term": {
-                    "tag": "Equals",
-                    "argSort": {
-                        "tag": "SortApp",
-                        "name": "SortBool",
-                        "args": []
-                    },
-                    "sort": {
-                        "tag": "SortApp",
-                        "name": "SortGeneratedTopCell",
-                        "args": []
-                    },
-                    "first": {
-                        "tag": "DV",
-                        "sort": {
-                            "tag": "SortApp",
-                            "name": "SortBool",
-                            "args": []
-                        },
-                        "value": "true"
-                    },
-                    "second": {
-                        "tag": "App",
-                        "name": "Lblcondition'LParUndsRParUnds'QUESTIONMARK-VARS'Unds'Bool'Unds'State",
-                        "sorts": [],
-                        "args": [
-                            {
-                                "tag": "EVar",
-                                "name": "Var'Ques'X",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortState",
-                                    "args": []
-                                }
-                            }
-                        ]
-                    }
-                }
-            }
-        }
-    }
-}
\ No newline at end of file
diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.booster-dev b/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.json
similarity index 100%
rename from booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.booster-dev
rename to booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.json
diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.kore-rpc-dev b/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.kore-rpc-dev
deleted file mode 100644
index eb9ba3ab36..0000000000
--- a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.kore-rpc-dev
+++ /dev/null
@@ -1,124 +0,0 @@
-{
-    "jsonrpc": "2.0",
-    "id": 1,
-    "result": {
-        "reason": "stuck",
-        "depth": 1,
-        "state": {
-            "term": {
-                "format": "KORE",
-                "version": 1,
-                "term": {
-                    "tag": "App",
-                    "name": "Lbl'-LT-'generatedTop'-GT-'",
-                    "sorts": [],
-                    "args": [
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'k'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "App",
-                                    "name": "dotk",
-                                    "sorts": [],
-                                    "args": []
-                                }
-                            ]
-                        },
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'a-state'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "EVar",
-                                    "name": "Var'Ques'X",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortState",
-                                        "args": []
-                                    }
-                                }
-                            ]
-                        },
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'b-state'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "EVar",
-                                    "name": "Var'Ques'X0",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortState",
-                                        "args": []
-                                    }
-                                }
-                            ]
-                        },
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'generatedCounter'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "DV",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortInt",
-                                        "args": []
-                                    },
-                                    "value": "0"
-                                }
-                            ]
-                        }
-                    ]
-                }
-            },
-            "predicate": {
-                "format": "KORE",
-                "version": 1,
-                "term": {
-                    "tag": "Equals",
-                    "argSort": {
-                        "tag": "SortApp",
-                        "name": "SortBool",
-                        "args": []
-                    },
-                    "sort": {
-                        "tag": "SortApp",
-                        "name": "SortGeneratedTopCell",
-                        "args": []
-                    },
-                    "first": {
-                        "tag": "DV",
-                        "sort": {
-                            "tag": "SortApp",
-                            "name": "SortBool",
-                            "args": []
-                        },
-                        "value": "true"
-                    },
-                    "second": {
-                        "tag": "App",
-                        "name": "Lblcondition'LParUndsRParUnds'QUESTIONMARK-VARS'Unds'Bool'Unds'State",
-                        "sorts": [],
-                        "args": [
-                            {
-                                "tag": "EVar",
-                                "name": "Var'Ques'X0",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortState",
-                                    "args": []
-                                }
-                            }
-                        ]
-                    }
-                }
-            }
-        }
-    }
-}
\ No newline at end of file
diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal-with-counter.booster-dev b/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal-with-counter.json
similarity index 100%
rename from booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal-with-counter.booster-dev
rename to booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal-with-counter.json
diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.booster-dev b/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.json
similarity index 100%
rename from booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.booster-dev
rename to booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.json
diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.kore-rpc-dev b/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.kore-rpc-dev
deleted file mode 100644
index a450b120fc..0000000000
--- a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.kore-rpc-dev
+++ /dev/null
@@ -1,172 +0,0 @@
-{
-    "jsonrpc": "2.0",
-    "id": 1,
-    "result": {
-        "reason": "stuck",
-        "depth": 2,
-        "state": {
-            "term": {
-                "format": "KORE",
-                "version": 1,
-                "term": {
-                    "tag": "App",
-                    "name": "Lbl'-LT-'generatedTop'-GT-'",
-                    "sorts": [],
-                    "args": [
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'k'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "App",
-                                    "name": "dotk",
-                                    "sorts": [],
-                                    "args": []
-                                }
-                            ]
-                        },
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'a-state'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "EVar",
-                                    "name": "Var'Ques'X",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortState",
-                                        "args": []
-                                    }
-                                }
-                            ]
-                        },
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'b-state'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "EVar",
-                                    "name": "Var'Ques'X0",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortState",
-                                        "args": []
-                                    }
-                                }
-                            ]
-                        },
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'generatedCounter'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "DV",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortInt",
-                                        "args": []
-                                    },
-                                    "value": "0"
-                                }
-                            ]
-                        }
-                    ]
-                }
-            },
-            "predicate": {
-                "format": "KORE",
-                "version": 1,
-                "term": {
-                    "tag": "And",
-                    "sort": {
-                        "tag": "SortApp",
-                        "name": "SortGeneratedTopCell",
-                        "args": []
-                    },
-                    "patterns": [
-                        {
-                            "tag": "Equals",
-                            "argSort": {
-                                "tag": "SortApp",
-                                "name": "SortBool",
-                                "args": []
-                            },
-                            "sort": {
-                                "tag": "SortApp",
-                                "name": "SortGeneratedTopCell",
-                                "args": []
-                            },
-                            "first": {
-                                "tag": "DV",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortBool",
-                                    "args": []
-                                },
-                                "value": "true"
-                            },
-                            "second": {
-                                "tag": "App",
-                                "name": "Lblcondition'LParUndsRParUnds'QUESTIONMARK-VARS'Unds'Bool'Unds'State",
-                                "sorts": [],
-                                "args": [
-                                    {
-                                        "tag": "EVar",
-                                        "name": "Var'Ques'X",
-                                        "sort": {
-                                            "tag": "SortApp",
-                                            "name": "SortState",
-                                            "args": []
-                                        }
-                                    }
-                                ]
-                            }
-                        },
-                        {
-                            "tag": "Equals",
-                            "argSort": {
-                                "tag": "SortApp",
-                                "name": "SortBool",
-                                "args": []
-                            },
-                            "sort": {
-                                "tag": "SortApp",
-                                "name": "SortGeneratedTopCell",
-                                "args": []
-                            },
-                            "first": {
-                                "tag": "DV",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortBool",
-                                    "args": []
-                                },
-                                "value": "true"
-                            },
-                            "second": {
-                                "tag": "App",
-                                "name": "Lblcondition'LParUndsRParUnds'QUESTIONMARK-VARS'Unds'Bool'Unds'State",
-                                "sorts": [],
-                                "args": [
-                                    {
-                                        "tag": "EVar",
-                                        "name": "Var'Ques'X0",
-                                        "sort": {
-                                            "tag": "SortApp",
-                                            "name": "SortState",
-                                            "args": []
-                                        }
-                                    }
-                                ]
-                            }
-                        }
-                    ]
-                }
-            }
-        }
-    }
-}
\ No newline at end of file
diff --git a/booster/test/rpc-integration/test-substitutions/README.md b/booster/test/rpc-integration/test-substitutions/README.md
index f6bf9f83bb..6180c4c7af 100644
--- a/booster/test/rpc-integration/test-substitutions/README.md
+++ b/booster/test/rpc-integration/test-substitutions/README.md
@@ -39,6 +39,7 @@ NB: Booster applies the given substitution before performing any action.
   - starts from `concrete-subst`
   - with two equations that have circular dependencies: `Y = 1 +Int X`, `X = Y -Int 1`
   - leading to end state with `X == 42` from the `ensures`-clause
+  - `booster-dev` return a trivial circular constraint `X ==Int X`
 * `state-symbolic-bottom-predicate.execute`
   - starts from `symbolic-subst`
   - with an equation that is instantly false: `X = 1 +Int X`
diff --git a/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev b/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev
index 259a441aeb..337751c9c3 100644
--- a/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev
+++ b/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev
@@ -66,13 +66,13 @@
                             "sorts": [],
                             "args": [
                                 {
-                                    "tag": "EVar",
-                                    "name": "X",
+                                    "tag": "DV",
                                     "sort": {
                                         "tag": "SortApp",
                                         "name": "SortInt",
                                         "args": []
-                                    }
+                                    },
+                                    "value": "42"
                                 }
                             ]
                         },
@@ -82,29 +82,13 @@
                             "sorts": [],
                             "args": [
                                 {
-                                    "tag": "App",
-                                    "name": "Lbl'UndsPlus'Int'Unds'",
-                                    "sorts": [],
-                                    "args": [
-                                        {
-                                            "tag": "EVar",
-                                            "name": "X",
-                                            "sort": {
-                                                "tag": "SortApp",
-                                                "name": "SortInt",
-                                                "args": []
-                                            }
-                                        },
-                                        {
-                                            "tag": "DV",
-                                            "sort": {
-                                                "tag": "SortApp",
-                                                "name": "SortInt",
-                                                "args": []
-                                            },
-                                            "value": "1"
-                                        }
-                                    ]
+                                    "tag": "DV",
+                                    "sort": {
+                                        "tag": "SortApp",
+                                        "name": "SortInt",
+                                        "args": []
+                                    },
+                                    "value": "43"
                                 }
                             ]
                         },
@@ -128,57 +112,6 @@
                 }
             },
             "substitution": {
-                "format": "KORE",
-                "version": 1,
-                "term": {
-                    "tag": "Equals",
-                    "argSort": {
-                        "tag": "SortApp",
-                        "name": "SortInt",
-                        "args": []
-                    },
-                    "sort": {
-                        "tag": "SortApp",
-                        "name": "SortGeneratedTopCell",
-                        "args": []
-                    },
-                    "first": {
-                        "tag": "EVar",
-                        "name": "Y",
-                        "sort": {
-                            "tag": "SortApp",
-                            "name": "SortInt",
-                            "args": []
-                        }
-                    },
-                    "second": {
-                        "tag": "App",
-                        "name": "Lbl'UndsPlus'Int'Unds'",
-                        "sorts": [],
-                        "args": [
-                            {
-                                "tag": "DV",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortInt",
-                                    "args": []
-                                },
-                                "value": "1"
-                            },
-                            {
-                                "tag": "EVar",
-                                "name": "X",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortInt",
-                                    "args": []
-                                }
-                            }
-                        ]
-                    }
-                }
-            },
-            "predicate": {
                 "format": "KORE",
                 "version": 1,
                 "term": {
@@ -193,7 +126,7 @@
                             "tag": "Equals",
                             "argSort": {
                                 "tag": "SortApp",
-                                "name": "SortBool",
+                                "name": "SortInt",
                                 "args": []
                             },
                             "sort": {
@@ -202,45 +135,29 @@
                                 "args": []
                             },
                             "first": {
-                                "tag": "DV",
+                                "tag": "EVar",
+                                "name": "X",
                                 "sort": {
                                     "tag": "SortApp",
-                                    "name": "SortBool",
+                                    "name": "SortInt",
                                     "args": []
-                                },
-                                "value": "true"
+                                }
                             },
                             "second": {
-                                "tag": "App",
-                                "name": "Lbl'UndsEqlsEqls'Int'Unds'",
-                                "sorts": [],
-                                "args": [
-                                    {
-                                        "tag": "EVar",
-                                        "name": "X",
-                                        "sort": {
-                                            "tag": "SortApp",
-                                            "name": "SortInt",
-                                            "args": []
-                                        }
-                                    },
-                                    {
-                                        "tag": "EVar",
-                                        "name": "X",
-                                        "sort": {
-                                            "tag": "SortApp",
-                                            "name": "SortInt",
-                                            "args": []
-                                        }
-                                    }
-                                ]
+                                "tag": "DV",
+                                "sort": {
+                                    "tag": "SortApp",
+                                    "name": "SortInt",
+                                    "args": []
+                                },
+                                "value": "42"
                             }
                         },
                         {
                             "tag": "Equals",
                             "argSort": {
                                 "tag": "SortApp",
-                                "name": "SortBool",
+                                "name": "SortInt",
                                 "args": []
                             },
                             "sort": {
@@ -249,42 +166,77 @@
                                 "args": []
                             },
                             "first": {
-                                "tag": "DV",
+                                "tag": "EVar",
+                                "name": "Y",
                                 "sort": {
                                     "tag": "SortApp",
-                                    "name": "SortBool",
+                                    "name": "SortInt",
                                     "args": []
-                                },
-                                "value": "true"
+                                }
                             },
                             "second": {
-                                "tag": "App",
-                                "name": "Lbl'UndsEqlsEqls'Int'Unds'",
-                                "sorts": [],
-                                "args": [
-                                    {
-                                        "tag": "EVar",
-                                        "name": "X",
-                                        "sort": {
-                                            "tag": "SortApp",
-                                            "name": "SortInt",
-                                            "args": []
-                                        }
-                                    },
-                                    {
-                                        "tag": "DV",
-                                        "sort": {
-                                            "tag": "SortApp",
-                                            "name": "SortInt",
-                                            "args": []
-                                        },
-                                        "value": "42"
-                                    }
-                                ]
+                                "tag": "DV",
+                                "sort": {
+                                    "tag": "SortApp",
+                                    "name": "SortInt",
+                                    "args": []
+                                },
+                                "value": "43"
                             }
                         }
                     ]
                 }
+            },
+            "predicate": {
+                "format": "KORE",
+                "version": 1,
+                "term": {
+                    "tag": "Equals",
+                    "argSort": {
+                        "tag": "SortApp",
+                        "name": "SortBool",
+                        "args": []
+                    },
+                    "sort": {
+                        "tag": "SortApp",
+                        "name": "SortGeneratedTopCell",
+                        "args": []
+                    },
+                    "first": {
+                        "tag": "DV",
+                        "sort": {
+                            "tag": "SortApp",
+                            "name": "SortBool",
+                            "args": []
+                        },
+                        "value": "true"
+                    },
+                    "second": {
+                        "tag": "App",
+                        "name": "Lbl'UndsEqlsEqls'Int'Unds'",
+                        "sorts": [],
+                        "args": [
+                            {
+                                "tag": "EVar",
+                                "name": "X",
+                                "sort": {
+                                    "tag": "SortApp",
+                                    "name": "SortInt",
+                                    "args": []
+                                }
+                            },
+                            {
+                                "tag": "EVar",
+                                "name": "X",
+                                "sort": {
+                                    "tag": "SortApp",
+                                    "name": "SortInt",
+                                    "args": []
+                                }
+                            }
+                        ]
+                    }
+                }
             }
         }
     }
diff --git a/booster/test/rpc-integration/test-substitutions/response-concrete-substitution.booster-dev b/booster/test/rpc-integration/test-substitutions/response-concrete-substitution.booster-dev
deleted file mode 100644
index 379ed33ccc..0000000000
--- a/booster/test/rpc-integration/test-substitutions/response-concrete-substitution.booster-dev
+++ /dev/null
@@ -1,168 +0,0 @@
-{
-    "jsonrpc": "2.0",
-    "id": 1,
-    "result": {
-        "reason": "terminal-rule",
-        "depth": 1,
-        "rule": "TEST.concrete-subst",
-        "state": {
-            "term": {
-                "format": "KORE",
-                "version": 1,
-                "term": {
-                    "tag": "App",
-                    "name": "Lbl'-LT-'generatedTop'-GT-'",
-                    "sorts": [],
-                    "args": [
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'k'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "App",
-                                    "name": "kseq",
-                                    "sorts": [],
-                                    "args": [
-                                        {
-                                            "tag": "App",
-                                            "name": "inj",
-                                            "sorts": [
-                                                {
-                                                    "tag": "SortApp",
-                                                    "name": "SortState",
-                                                    "args": []
-                                                },
-                                                {
-                                                    "tag": "SortApp",
-                                                    "name": "SortKItem",
-                                                    "args": []
-                                                }
-                                            ],
-                                            "args": [
-                                                {
-                                                    "tag": "DV",
-                                                    "sort": {
-                                                        "tag": "SortApp",
-                                                        "name": "SortState",
-                                                        "args": []
-                                                    },
-                                                    "value": "a"
-                                                }
-                                            ]
-                                        },
-                                        {
-                                            "tag": "App",
-                                            "name": "dotk",
-                                            "sorts": [],
-                                            "args": []
-                                        }
-                                    ]
-                                }
-                            ]
-                        },
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'int'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "EVar",
-                                    "name": "X",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortInt",
-                                        "args": []
-                                    }
-                                }
-                            ]
-                        },
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'jnt'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "EVar",
-                                    "name": "Y",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortInt",
-                                        "args": []
-                                    }
-                                }
-                            ]
-                        },
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'generatedCounter'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "DV",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortInt",
-                                        "args": []
-                                    },
-                                    "value": "0"
-                                }
-                            ]
-                        }
-                    ]
-                }
-            },
-            "predicate": {
-                "format": "KORE",
-                "version": 1,
-                "term": {
-                    "tag": "Equals",
-                    "argSort": {
-                        "tag": "SortApp",
-                        "name": "SortBool",
-                        "args": []
-                    },
-                    "sort": {
-                        "tag": "SortApp",
-                        "name": "SortGeneratedTopCell",
-                        "args": []
-                    },
-                    "first": {
-                        "tag": "DV",
-                        "sort": {
-                            "tag": "SortApp",
-                            "name": "SortBool",
-                            "args": []
-                        },
-                        "value": "true"
-                    },
-                    "second": {
-                        "tag": "App",
-                        "name": "Lbl'UndsEqlsEqls'Int'Unds'",
-                        "sorts": [],
-                        "args": [
-                            {
-                                "tag": "EVar",
-                                "name": "X",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortInt",
-                                    "args": []
-                                }
-                            },
-                            {
-                                "tag": "DV",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortInt",
-                                    "args": []
-                                },
-                                "value": "42"
-                            }
-                        ]
-                    }
-                }
-            }
-        }
-    }
-}
\ No newline at end of file
diff --git a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev
deleted file mode 100644
index 8196839aaa..0000000000
--- a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev
+++ /dev/null
@@ -1,183 +0,0 @@
-{
-    "jsonrpc": "2.0",
-    "id": 1,
-    "result": {
-        "reason": "vacuous",
-        "depth": 0,
-        "state": {
-            "term": {
-                "format": "KORE",
-                "version": 1,
-                "term": {
-                    "tag": "App",
-                    "name": "Lbl'-LT-'generatedTop'-GT-'",
-                    "sorts": [],
-                    "args": [
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'k'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "App",
-                                    "name": "kseq",
-                                    "sorts": [],
-                                    "args": [
-                                        {
-                                            "tag": "App",
-                                            "name": "inj",
-                                            "sorts": [
-                                                {
-                                                    "tag": "SortApp",
-                                                    "name": "SortState",
-                                                    "args": []
-                                                },
-                                                {
-                                                    "tag": "SortApp",
-                                                    "name": "SortKItem",
-                                                    "args": []
-                                                }
-                                            ],
-                                            "args": [
-                                                {
-                                                    "tag": "DV",
-                                                    "sort": {
-                                                        "tag": "SortApp",
-                                                        "name": "SortState",
-                                                        "args": []
-                                                    },
-                                                    "value": "symbolic-subst"
-                                                }
-                                            ]
-                                        },
-                                        {
-                                            "tag": "App",
-                                            "name": "dotk",
-                                            "sorts": [],
-                                            "args": []
-                                        }
-                                    ]
-                                }
-                            ]
-                        },
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'int'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "EVar",
-                                    "name": "X",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortInt",
-                                        "args": []
-                                    }
-                                }
-                            ]
-                        },
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'jnt'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "EVar",
-                                    "name": "Y",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortInt",
-                                        "args": []
-                                    }
-                                }
-                            ]
-                        },
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'generatedCounter'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "DV",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortInt",
-                                        "args": []
-                                    },
-                                    "value": "0"
-                                }
-                            ]
-                        }
-                    ]
-                }
-            },
-            "predicate": {
-                "format": "KORE",
-                "version": 1,
-                "term": {
-                    "tag": "Equals",
-                    "argSort": {
-                        "tag": "SortApp",
-                        "name": "SortBool",
-                        "args": []
-                    },
-                    "sort": {
-                        "tag": "SortApp",
-                        "name": "SortGeneratedTopCell",
-                        "args": []
-                    },
-                    "first": {
-                        "tag": "DV",
-                        "sort": {
-                            "tag": "SortApp",
-                            "name": "SortBool",
-                            "args": []
-                        },
-                        "value": "true"
-                    },
-                    "second": {
-                        "tag": "App",
-                        "name": "Lbl'UndsEqlsEqls'Int'Unds'",
-                        "sorts": [],
-                        "args": [
-                            {
-                                "tag": "EVar",
-                                "name": "X",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortInt",
-                                    "args": []
-                                }
-                            },
-                            {
-                                "tag": "App",
-                                "name": "Lbl'UndsPlus'Int'Unds'",
-                                "sorts": [],
-                                "args": [
-                                    {
-                                        "tag": "DV",
-                                        "sort": {
-                                            "tag": "SortApp",
-                                            "name": "SortInt",
-                                            "args": []
-                                        },
-                                        "value": "1"
-                                    },
-                                    {
-                                        "tag": "EVar",
-                                        "name": "X",
-                                        "sort": {
-                                            "tag": "SortApp",
-                                            "name": "SortInt",
-                                            "args": []
-                                        }
-                                    }
-                                ]
-                            }
-                        ]
-                    }
-                }
-            }
-        }
-    }
-}
\ No newline at end of file
diff --git a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json
index 8196839aaa..8dd09608d8 100644
--- a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json
+++ b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json
@@ -180,4 +180,4 @@
             }
         }
     }
-}
\ No newline at end of file
+}
diff --git a/booster/test/rpc-integration/test-substitutions/response-symbolic-substitution.booster-dev b/booster/test/rpc-integration/test-substitutions/response-symbolic-substitution.booster-dev
deleted file mode 100644
index 5cf51a99bb..0000000000
--- a/booster/test/rpc-integration/test-substitutions/response-symbolic-substitution.booster-dev
+++ /dev/null
@@ -1,168 +0,0 @@
-{
-    "jsonrpc": "2.0",
-    "id": 1,
-    "result": {
-        "reason": "terminal-rule",
-        "depth": 1,
-        "rule": "TEST.symbolic-subst",
-        "state": {
-            "term": {
-                "format": "KORE",
-                "version": 1,
-                "term": {
-                    "tag": "App",
-                    "name": "Lbl'-LT-'generatedTop'-GT-'",
-                    "sorts": [],
-                    "args": [
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'k'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "App",
-                                    "name": "kseq",
-                                    "sorts": [],
-                                    "args": [
-                                        {
-                                            "tag": "App",
-                                            "name": "inj",
-                                            "sorts": [
-                                                {
-                                                    "tag": "SortApp",
-                                                    "name": "SortState",
-                                                    "args": []
-                                                },
-                                                {
-                                                    "tag": "SortApp",
-                                                    "name": "SortKItem",
-                                                    "args": []
-                                                }
-                                            ],
-                                            "args": [
-                                                {
-                                                    "tag": "DV",
-                                                    "sort": {
-                                                        "tag": "SortApp",
-                                                        "name": "SortState",
-                                                        "args": []
-                                                    },
-                                                    "value": "a"
-                                                }
-                                            ]
-                                        },
-                                        {
-                                            "tag": "App",
-                                            "name": "dotk",
-                                            "sorts": [],
-                                            "args": []
-                                        }
-                                    ]
-                                }
-                            ]
-                        },
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'int'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "EVar",
-                                    "name": "X",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortInt",
-                                        "args": []
-                                    }
-                                }
-                            ]
-                        },
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'jnt'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "EVar",
-                                    "name": "Y",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortInt",
-                                        "args": []
-                                    }
-                                }
-                            ]
-                        },
-                        {
-                            "tag": "App",
-                            "name": "Lbl'-LT-'generatedCounter'-GT-'",
-                            "sorts": [],
-                            "args": [
-                                {
-                                    "tag": "DV",
-                                    "sort": {
-                                        "tag": "SortApp",
-                                        "name": "SortInt",
-                                        "args": []
-                                    },
-                                    "value": "0"
-                                }
-                            ]
-                        }
-                    ]
-                }
-            },
-            "predicate": {
-                "format": "KORE",
-                "version": 1,
-                "term": {
-                    "tag": "Equals",
-                    "argSort": {
-                        "tag": "SortApp",
-                        "name": "SortBool",
-                        "args": []
-                    },
-                    "sort": {
-                        "tag": "SortApp",
-                        "name": "SortGeneratedTopCell",
-                        "args": []
-                    },
-                    "first": {
-                        "tag": "DV",
-                        "sort": {
-                            "tag": "SortApp",
-                            "name": "SortBool",
-                            "args": []
-                        },
-                        "value": "true"
-                    },
-                    "second": {
-                        "tag": "App",
-                        "name": "Lbl'UndsEqlsEqls'Int'Unds'",
-                        "sorts": [],
-                        "args": [
-                            {
-                                "tag": "EVar",
-                                "name": "X",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortInt",
-                                    "args": []
-                                }
-                            },
-                            {
-                                "tag": "EVar",
-                                "name": "Y",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortInt",
-                                    "args": []
-                                }
-                            }
-                        ]
-                    }
-                }
-            }
-        }
-    }
-}
\ No newline at end of file
diff --git a/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test1.json b/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test1.json
index caf1cf3ac9..f0938023a3 100644
--- a/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test1.json
+++ b/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test1.json
@@ -63,13 +63,13 @@
                             "sorts": [],
                             "args": [
                                 {
-                                    "tag": "EVar",
-                                    "name": "Var'Ques'X",
+                                    "tag": "DV",
                                     "sort": {
                                         "tag": "SortApp",
                                         "name": "SortInt",
                                         "args": []
-                                    }
+                                    },
+                                    "value": "42"
                                 }
                             ]
                         },
@@ -92,14 +92,14 @@
                     ]
                 }
             },
-            "predicate": {
+            "substitution": {
                 "format": "KORE",
                 "version": 1,
                 "term": {
                     "tag": "Equals",
                     "argSort": {
                         "tag": "SortApp",
-                        "name": "SortBool",
+                        "name": "SortInt",
                         "args": []
                     },
                     "sort": {
@@ -108,38 +108,22 @@
                         "args": []
                     },
                     "first": {
-                        "tag": "DV",
+                        "tag": "EVar",
+                        "name": "Var'Ques'X",
                         "sort": {
                             "tag": "SortApp",
-                            "name": "SortBool",
+                            "name": "SortInt",
                             "args": []
-                        },
-                        "value": "true"
+                        }
                     },
                     "second": {
-                        "tag": "App",
-                        "name": "Lbl'UndsEqlsEqls'Int'Unds'",
-                        "sorts": [],
-                        "args": [
-                            {
-                                "tag": "EVar",
-                                "name": "Var'Ques'X",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortInt",
-                                    "args": []
-                                }
-                            },
-                            {
-                                "tag": "DV",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortInt",
-                                    "args": []
-                                },
-                                "value": "42"
-                            }
-                        ]
+                        "tag": "DV",
+                        "sort": {
+                            "tag": "SortApp",
+                            "name": "SortInt",
+                            "args": []
+                        },
+                        "value": "42"
                     }
                 }
             }
diff --git a/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test2.json b/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test2.json
index 9d24d95c64..8b9792046d 100644
--- a/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test2.json
+++ b/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test2.json
@@ -63,13 +63,13 @@
                             "sorts": [],
                             "args": [
                                 {
-                                    "tag": "EVar",
-                                    "name": "Var'Ques'X",
+                                    "tag": "DV",
                                     "sort": {
                                         "tag": "SortApp",
                                         "name": "SortInt",
                                         "args": []
-                                    }
+                                    },
+                                    "value": "42"
                                 }
                             ]
                         },
@@ -92,14 +92,14 @@
                     ]
                 }
             },
-            "predicate": {
+            "substitution": {
                 "format": "KORE",
                 "version": 1,
                 "term": {
                     "tag": "Equals",
                     "argSort": {
                         "tag": "SortApp",
-                        "name": "SortBool",
+                        "name": "SortInt",
                         "args": []
                     },
                     "sort": {
@@ -108,41 +108,25 @@
                         "args": []
                     },
                     "first": {
-                        "tag": "DV",
+                        "tag": "EVar",
+                        "name": "Var'Ques'X",
                         "sort": {
                             "tag": "SortApp",
-                            "name": "SortBool",
+                            "name": "SortInt",
                             "args": []
-                        },
-                        "value": "true"
+                        }
                     },
                     "second": {
-                        "tag": "App",
-                        "name": "Lbl'UndsEqlsEqls'Int'Unds'",
-                        "sorts": [],
-                        "args": [
-                            {
-                                "tag": "EVar",
-                                "name": "Var'Ques'X",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortInt",
-                                    "args": []
-                                }
-                            },
-                            {
-                                "tag": "DV",
-                                "sort": {
-                                    "tag": "SortApp",
-                                    "name": "SortInt",
-                                    "args": []
-                                },
-                                "value": "42"
-                            }
-                        ]
+                        "tag": "DV",
+                        "sort": {
+                            "tag": "SortApp",
+                            "name": "SortInt",
+                            "args": []
+                        },
+                        "value": "42"
                     }
                 }
             }
         }
     }
-}
+}
\ No newline at end of file
diff --git a/booster/tools/booster/Proxy.hs b/booster/tools/booster/Proxy.hs
index edadbd7e0f..251728085b 100644
--- a/booster/tools/booster/Proxy.hs
+++ b/booster/tools/booster/Proxy.hs
@@ -523,8 +523,7 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of
                                 pure $
                                     Right
                                         ( ( Booster.toExecState
-                                                Pattern{term, ceilConditions, constraints = Set.fromList preds}
-                                                sub
+                                                Pattern{term, ceilConditions, constraints = Set.fromList preds, substitution = sub}
                                                 unsup
                                                 Nothing
                                           )
diff --git a/booster/unit-tests/Test/Booster/Pattern/Binary.hs b/booster/unit-tests/Test/Booster/Pattern/Binary.hs
index 931d803707..e5588fda77 100644
--- a/booster/unit-tests/Test/Booster/Pattern/Binary.hs
+++ b/booster/unit-tests/Test/Booster/Pattern/Binary.hs
@@ -67,7 +67,7 @@ genPredicate =
         <$> Gen.choice [pure TrueBool, pure FalseBool, genTerm]
 
 genPattern :: Gen Pattern
-genPattern = (\t cs -> Pattern t cs mempty) <$> genTerm <*> (Set.fromList <$> upTo 10 genPredicate)
+genPattern = (\t cs -> Pattern t cs mempty mempty) <$> genTerm <*> (Set.fromList <$> upTo 10 genPredicate)
 
 test_BinaryRoundTrips :: [TestTree]
 test_BinaryRoundTrips =
diff --git a/booster/unit-tests/Test/Booster/Pattern/Substitution.hs b/booster/unit-tests/Test/Booster/Pattern/Substitution.hs
new file mode 100644
index 0000000000..663bdd2a54
--- /dev/null
+++ b/booster/unit-tests/Test/Booster/Pattern/Substitution.hs
@@ -0,0 +1,84 @@
+{-# LANGUAGE QuasiQuotes #-}
+
+module Test.Booster.Pattern.Substitution (
+    test_subst,
+) where
+
+import Data.Map qualified as Map
+import Test.Tasty
+import Test.Tasty.HUnit
+
+import Booster.Definition.Attributes.Base
+import Booster.Pattern.Base
+import Booster.Pattern.Substitution
+import Booster.Syntax.Json.Internalise (trm)
+
+test_subst :: TestTree
+test_subst =
+    testGroup
+        "Substitution"
+        [ testGroup
+            "Application"
+            [ test
+                "con1(X)[con1(Y)/X]"
+                ("X" |-> [trm| con1{}(Y:SomeSort{}) |])
+                ([trm| con1{}(X:SomeSort{}) |])
+                ([trm| con1{}(con1{}(Y:SomeSort{})) |])
+            , test
+                "con1(X)/\\con1(X)[con1(Y)/X]"
+                ("X" |-> [trm| con1{}(Y:SomeSort{}) |])
+                (AndTerm ([trm| con1{}(X:SomeSort{}) |]) ([trm| con1{}(X:SomeSort{}) |]))
+                (AndTerm ([trm| con1{}(con1{}(Y:SomeSort{})) |]) ([trm| con1{}(con1{}(Y:SomeSort{})) |]))
+            , test
+                "con1(X)/\\con1(Y)[con1(Y)/X]"
+                ("X" |-> [trm| con1{}(Y:SomeSort{}) |])
+                (AndTerm ([trm| con1{}(X:SomeSort{}) |]) ([trm| con1{}(Y:SomeSort{}) |]))
+                (AndTerm ([trm| con1{}(con1{}(Y:SomeSort{})) |]) ([trm| con1{}(Y:SomeSort{}) |]))
+            ]
+        , testGroup
+            "Composition"
+            [ testCase
+                "compose is idempotent"
+                $ (("X" |-> [trm| con1{}(Y:SomeSort{}) |]) `compose` ("X" |-> [trm| con1{}(Y:SomeSort{}) |]))
+                    @?= ("X" |-> [trm| con1{}(Y:SomeSort{}) |])
+            , testCase
+                "compose is transitive and saturating"
+                $ (("X" |-> [trm| Z:SomeSort{} |]) `compose` ("Y" |-> [trm| X:SomeSort{} |]))
+                    @?= ("X" |-> [trm| Z:SomeSort{} |])
+                        <> ("Y" |-> [trm| Z:SomeSort{} |])
+            ]
+        ]
+
+----------------------------------------
+-- Test fixture
+test :: String -> Map.Map Variable Term -> Term -> Term -> TestTree
+test name substitutions term expected =
+    testCase name $ substituteInTerm substitutions term @?= expected
+
+someSort :: Sort
+someSort = SortApp "SomeSort" []
+
+(|->) :: VarName -> Term -> Substitution
+(|->) v t = Map.fromList [(Variable someSort v, t)]
+
+asConstructor :: SymbolAttributes
+asConstructor =
+    SymbolAttributes
+        Constructor
+        IsNotIdem
+        IsNotAssoc
+        IsNotMacroOrAlias
+        CanBeEvaluated
+        Nothing
+        Nothing
+        Nothing
+
+con1 :: Symbol
+con1 =
+    Symbol
+        { name = "con1"
+        , sortVars = []
+        , resultSort = someSort
+        , argSorts = [someSort]
+        , attributes = asConstructor
+        }
diff --git a/booster/unit-tests/Test/Booster/Pattern/Util.hs b/booster/unit-tests/Test/Booster/Pattern/Util.hs
index 110c542898..11f021c5dd 100644
--- a/booster/unit-tests/Test/Booster/Pattern/Util.hs
+++ b/booster/unit-tests/Test/Booster/Pattern/Util.hs
@@ -1,38 +1,14 @@
 module Test.Booster.Pattern.Util (
-    test_subst,
     test_freshen,
 ) where
 
-import Data.Map qualified as Map
 import Data.Set qualified as Set
 import Test.Tasty
 import Test.Tasty.HUnit
 
-import Booster.Definition.Attributes.Base
 import Booster.Pattern.Base
 import Booster.Pattern.Util
 
-test_subst :: TestTree
-test_subst =
-    testGroup
-        "Substitution"
-        [ test
-            "con1(X)[con1(Y)/X]"
-            (Map.fromList [(Variable someSort "X", app con1 [var "Y" someSort])])
-            (app con1 [var "X" someSort])
-            (app con1 [app con1 [var "Y" someSort]])
-        , test
-            "con1(X)/\\con1(X)[con1(Y)/X]"
-            (Map.fromList [(Variable someSort "X", app con1 [var "Y" someSort])])
-            (AndTerm (app con1 [var "X" someSort]) (app con1 [var "X" someSort]))
-            (AndTerm (app con1 [app con1 [var "Y" someSort]]) (app con1 [app con1 [var "Y" someSort]]))
-        , test
-            "con1(X)/\\con1(Y)[con1(Y)/X]"
-            (Map.fromList [(Variable someSort "X", app con1 [var "Y" someSort])])
-            (AndTerm (app con1 [var "X" someSort]) (app con1 [var "Y" someSort]))
-            (AndTerm (app con1 [app con1 [var "Y" someSort]]) (app con1 [var "Y" someSort]))
-        ]
-
 test_freshen :: TestTree
 test_freshen =
     testGroup
@@ -53,38 +29,6 @@ test_freshen =
         ]
 
 ----------------------------------------
--- Test fixture
-test :: String -> Map.Map Variable Term -> Term -> Term -> TestTree
-test name substitutions term expected =
-    testCase name $ substituteInTerm substitutions term @?= expected
 
 someSort :: Sort
 someSort = SortApp "SomeSort" []
-
-var :: VarName -> Sort -> Term
-var variableName variableSort = Var $ Variable{variableSort, variableName}
-
-app :: Symbol -> [Term] -> Term
-app s = SymbolApplication s []
-
-asConstructor :: SymbolAttributes
-asConstructor =
-    SymbolAttributes
-        Constructor
-        IsNotIdem
-        IsNotAssoc
-        IsNotMacroOrAlias
-        CanBeEvaluated
-        Nothing
-        Nothing
-        Nothing
-
-con1 :: Symbol
-con1 =
-    Symbol
-        { name = "con1"
-        , sortVars = []
-        , resultSort = someSort
-        , argSorts = [someSort]
-        , attributes = asConstructor
-        }