diff --git a/kore/src/Kore/Strategies/Goal.hs b/kore/src/Kore/Strategies/Goal.hs
index 2f816718a0..8132f11b37 100644
--- a/kore/src/Kore/Strategies/Goal.hs
+++ b/kore/src/Kore/Strategies/Goal.hs
@@ -846,16 +846,33 @@ simplify'
     => Lens' goal ClaimPattern
     -> goal
     -> Strategy.TransitionT (AppliedRule goal) m goal
-simplify' lensClaimPattern =
-    Lens.traverseOf (lensClaimPattern . field @"left") $ \config -> do
-        let definedConfig =
-                Pattern.andCondition (mkDefined <$> config)
-                $ from $ makeCeilPredicate_ (Conditional.term config)
-        configs <-
-            simplifyTopConfiguration definedConfig
-            >>= SMT.Evaluator.filterMultiOr
-            & lift
-        Foldable.asum (pure <$> configs)
+simplify' lensClaimPattern goal = do
+    goal' <- simplifyLeftHandSide goal
+    let sideCondition = extractSideCondition goal'
+    simplifyRightHandSide sideCondition goal'
+  where
+    extractSideCondition =
+        SideCondition.assumeTrueCondition
+        . Pattern.withoutTerm
+        . Lens.view (lensClaimPattern . field @"left")
+
+    simplifyLeftHandSide =
+        Lens.traverseOf (lensClaimPattern . field @"left") $ \config -> do
+            let definedConfig =
+                    Pattern.andCondition (mkDefined <$> config)
+                    $ from $ makeCeilPredicate_ (Conditional.term config)
+            configs <-
+                simplifyTopConfiguration definedConfig
+                >>= SMT.Evaluator.filterMultiOr
+                & lift
+            Foldable.asum (pure <$> configs)
+
+    simplifyRightHandSide sideCondition =
+        Lens.traverseOf (lensClaimPattern . field @"right") $ \dest ->
+            OrPattern.observeAllT
+            $ Logic.scatter dest
+            >>= Pattern.simplify sideCondition
+            >>= Logic.scatter
 
 isTriviallyValid' :: Lens' goal ClaimPattern -> goal -> Bool
 isTriviallyValid' lensClaimPattern =
diff --git a/test/all-path/00-basic/01-one-rule/all-path-b-or-c-spec.k b/test/all-path/00-basic/01-one-rule/all-path-b-or-c-spec.k
index 62eb99aa26..613f848be3 100644
--- a/test/all-path/00-basic/01-one-rule/all-path-b-or-c-spec.k
+++ b/test/all-path/00-basic/01-one-rule/all-path-b-or-c-spec.k
@@ -7,7 +7,6 @@ module ALL-PATH-B-OR-C-SPEC
   import PATH
 
   // This should be provable as transiting to b suffices
-  // TODO (#1278): ... => ?X ensures ?X ==K b orBool ?X ==K c
   rule <k> a => b #Or c </k> [all-path]
 
 endmodule
diff --git a/test/all-path/03-unification/set-select/all-path-b-or-c-spec.k b/test/all-path/03-unification/set-select/all-path-b-or-c-spec.k
index 6c3bfb03a5..34f7aadf35 100644
--- a/test/all-path/03-unification/set-select/all-path-b-or-c-spec.k
+++ b/test/all-path/03-unification/set-select/all-path-b-or-c-spec.k
@@ -7,7 +7,6 @@ module ALL-PATH-B-OR-C-SPEC
   imports VERIFICATION
   imports PATH
 
-  // TODO (#1278): ... => ?X ensures ?X ==K b orBool ?X ==K c
   rule <k> select => b #Or c </k>
        <state> SetItem(b) SetItem(c) </state>
     [all-path]
diff --git a/test/all-path/03-unification/set-select/one-path-b-or-c-spec.k b/test/all-path/03-unification/set-select/one-path-b-or-c-spec.k
index c07de6847a..337b4aa4a5 100644
--- a/test/all-path/03-unification/set-select/one-path-b-or-c-spec.k
+++ b/test/all-path/03-unification/set-select/one-path-b-or-c-spec.k
@@ -7,7 +7,6 @@ module ONE-PATH-B-OR-C-SPEC
   imports VERIFICATION
   imports PATH
 
-  // TODO (#1278): ... => ?X ensures ?X ==K b orBool ?X ==K c
   rule <k> select => b #Or c </k>
        <state> SetItem(b) SetItem(c) </state>
     [one-path]
diff --git a/test/simplify-rhs/Makefile b/test/simplify-rhs/Makefile
new file mode 100644
index 0000000000..382792481e
--- /dev/null
+++ b/test/simplify-rhs/Makefile
@@ -0,0 +1,2 @@
+DEF = test
+include $(CURDIR)/../include.mk
diff --git a/test/simplify-rhs/test-1-repl-script-spec.k b/test/simplify-rhs/test-1-repl-script-spec.k
new file mode 100644
index 0000000000..adc43ba8bb
--- /dev/null
+++ b/test/simplify-rhs/test-1-repl-script-spec.k
@@ -0,0 +1,11 @@
+module VERIFICATION
+    imports TEST
+
+endmodule
+
+module TEST-1-REPL-SCRIPT-SPEC
+    imports VERIFICATION
+
+    rule a => f(c)
+
+endmodule
diff --git a/test/simplify-rhs/test-1-repl-script-spec.k.out.golden b/test/simplify-rhs/test-1-repl-script-spec.k.out.golden
new file mode 100644
index 0000000000..ea80a9b1c1
--- /dev/null
+++ b/test/simplify-rhs/test-1-repl-script-spec.k.out.golden
@@ -0,0 +1,10 @@
+Kore (0)> ProveSteps 1
+    #Top
+  #And
+    <k>
+      evaluated ~> _DotVar1 ~> .
+    </k>
+#Implies
+  #wAF ( <k>
+    evaluated ~> _DotVar1 ~> .
+  </k> )
diff --git a/test/simplify-rhs/test-1-repl-script-spec.k.repl b/test/simplify-rhs/test-1-repl-script-spec.k.repl
new file mode 100644
index 0000000000..7b1fece8d1
--- /dev/null
+++ b/test/simplify-rhs/test-1-repl-script-spec.k.repl
@@ -0,0 +1 @@
+step
diff --git a/test/simplify-rhs/test.k b/test/simplify-rhs/test.k
new file mode 100644
index 0000000000..e37713eb91
--- /dev/null
+++ b/test/simplify-rhs/test.k
@@ -0,0 +1,10 @@
+module TEST
+    
+    syntax S ::= "a" | "b" | "c" | "evaluated"
+               | f(S) [function]
+
+    rule f(_:S) => evaluated
+
+    rule a => f(b)
+
+endmodule