diff --git a/kore/src/Kore/Step/Simplification/SubstitutionSimplifier.hs b/kore/src/Kore/Step/Simplification/SubstitutionSimplifier.hs
index d7db4b3ada..9426ce20f9 100644
--- a/kore/src/Kore/Step/Simplification/SubstitutionSimplifier.hs
+++ b/kore/src/Kore/Step/Simplification/SubstitutionSimplifier.hs
@@ -75,7 +75,6 @@ import Kore.Internal.SideCondition
     )
 import qualified Kore.Internal.SideCondition as SideCondition
     ( toRepresentation
-    , topTODO
     )
 import Kore.Internal.Substitution
     ( Assignment
@@ -180,9 +179,10 @@ simplifyAnds
         , Monad monad
         )
     => MakeAnd monad
+    -> SideCondition variable
     -> NonEmpty (TermLike variable)
     -> monad (Pattern variable)
-simplifyAnds MakeAnd { makeAnd } (NonEmpty.sort -> patterns) =
+simplifyAnds MakeAnd { makeAnd } sideCondition (NonEmpty.sort -> patterns) =
     foldM simplifyAnds' Pattern.top patterns
   where
     simplifyAnds'
@@ -194,7 +194,6 @@ simplifyAnds MakeAnd { makeAnd } (NonEmpty.sort -> patterns) =
             AndF And { andFirst, andSecond } ->
                 foldM simplifyAnds' intermediate [andFirst, andSecond]
             _ -> do
-                let sideCondition = SideCondition.topTODO
                 simplified <-
                     makeAnd
                         intermediateTerm
@@ -211,12 +210,13 @@ deduplicateSubstitution
         , Monad monad
         )
     =>  MakeAnd monad
+    ->  SideCondition variable
     ->  Substitution variable
     ->  monad
             ( Predicate variable
             , Map (UnifiedVariable variable) (TermLike variable)
             )
-deduplicateSubstitution makeAnd' =
+deduplicateSubstitution sideCondition makeAnd' =
     worker Predicate.makeTruePredicate_ . checkSetVars . Substitution.toMultiMap
   where
     checkSetVars m
@@ -228,7 +228,7 @@ deduplicateSubstitution makeAnd' =
                 (\k v -> Any $ isSetVar k && isNotSingleton v)
             isNotSingleton = isNothing . getSingleton
 
-    simplifyAnds' = simplifyAnds makeAnd'
+    simplifyAnds' = simplifyAnds sideCondition makeAnd'
 
     worker
         ::  Predicate variable
@@ -373,7 +373,7 @@ simplifySubstitutionWorker sideCondition makeAnd' = \substitution -> do
                 (Map (UnifiedVariable variable) (TermLike variable))
     deduplicate substitution = do
         (predicate, substitution') <-
-            deduplicateSubstitution makeAnd' substitution
+            deduplicateSubstitution makeAnd' sideCondition substitution
             & lift . lift
         addPredicate predicate
         return substitution'
diff --git a/kore/test/Test/Kore/Unification/Unifier.hs b/kore/test/Test/Kore/Unification/Unifier.hs
index c502bc8f96..7f292cfe8c 100644
--- a/kore/test/Test/Kore/Unification/Unifier.hs
+++ b/kore/test/Test/Kore/Unification/Unifier.hs
@@ -195,6 +195,7 @@ simplifyAnds
 simplifyAnds =
     SubstitutionSimplifier.simplifyAnds
         (Unification.unificationMakeAnd Not.notSimplifier)
+        SideCondition.top
 
 andSimplifySuccess
     :: HasCallStack