Keep Substitution when converting from Predicate to Condition

kore/src/Kore/Internal/Conditional.hs

@@ -183,7 +183,10 @@ instance
     From (Predicate variable) (Conditional variable ())
     where
     from predicate =
-        Conditional{term = (), predicate, substitution = mempty}
+        Substitution.retractAssignment predicate
+            & maybe fallback (from @(Assignment _))
+      where
+        fallback = Conditional{term = (), predicate, substitution = mempty}
 
 instance
     InternalVariable variable =>

kore/src/Kore/Internal/MultiAnd.hs

@@ -118,6 +118,13 @@ instance
     from = fromPredicate . from @_ @(Predicate _)
     {-# INLINE from #-}
 
+instance
+    InternalVariable variable =>
+    From (MultiAnd (Predicate variable)) (Condition variable)
+    where
+    from = foldMap (from @_ @(Condition _))
+    {-# INLINE from #-}
+
 instance
     InternalVariable variable =>
     From (TermLike variable) (MultiAnd (TermLike variable))

kore/src/Kore/Internal/Substitution.hs

@@ -13,6 +13,7 @@ module Kore.Internal.Substitution (
     assignedVariable,
     assignedTerm,
     mapAssignedTerm,
+    retractAssignment,
     singleSubstitutionToPredicate,
     UnwrappedSubstitution,
     mkUnwrappedSubstitution,
@@ -68,6 +69,7 @@ import qualified Kore.Attribute.Pattern.Simplified as Attribute (
 import Kore.Debug
 import Kore.Internal.Predicate (
     Predicate,
+    pattern PredicateEquals,
  )
 import qualified Kore.Internal.Predicate as Predicate
 import qualified Kore.Internal.SideCondition.SideCondition as SideCondition (
@@ -155,6 +157,20 @@ mkUnwrappedSubstitution ::
     [Assignment variable]
 mkUnwrappedSubstitution = fmap (uncurry assign)
 
+{- | Extract an 'Assignment' from a 'Predicate' of the proper form.
+
+Returns 'Nothing' if the 'Predicate' is not in the correct form.
+-}
+retractAssignment ::
+    InternalVariable variable =>
+    Predicate variable ->
+    Maybe (Assignment variable)
+retractAssignment (PredicateEquals (Var_ var) term) =
+    Just (assign var term)
+retractAssignment (PredicateEquals term (Var_ var)) =
+    Just (assign var term)
+retractAssignment _ = Nothing
+
 {- | @Substitution@ represents a collection @[xᵢ=φᵢ]@ of substitutions.
 
 Individual substitutions are a pair of type