Add symmetrical cases

runtimeverification · Oct 17, 2024 · 7091e0f · 7091e0f
1 parent 571dbda
commit 7091e0f
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/booster/library/Booster/Pattern/Substitution.hs b/booster/library/Booster/Pattern/Substitution.hs
@@ -46,9 +46,13 @@ mkEq x t = Predicate $ case sortOfTerm t of
 destructEq :: Predicate -> Maybe (Variable, Term)
 destructEq = \case
     Predicate (EqualsInt (Var x) t) -> Just (x, t)
+    Predicate (EqualsInt t (Var x)) -> Just (x, t)
     Predicate (EqualsBool (Var x) t) -> Just (x, t)
+    Predicate (EqualsBool t (Var x)) -> Just (x, t)
     Predicate
         (EqualsK (KSeq _lhsSort (Var x)) (KSeq _rhsSort t)) -> Just (x, t)
+    Predicate
+        (EqualsK (KSeq _lhsSort t) (KSeq _rhsSort (Var x))) -> Just (x, t)
     _ -> Nothing
 
 -- | turns a substitution into a list of equations