diff --git a/Pystan/config/sign_analysis.py b/Pystan/config/sign_analysis.py
index 043f5b1351cfccb192fcff24f88fcc1200a90214..38b4e9e2b1f6c8d4b1fd3f6f0ee7773c61b02f89 100644
--- a/Pystan/config/sign_analysis.py
+++ b/Pystan/config/sign_analysis.py
@@ -344,11 +344,33 @@ def reduce_strict_lower_bound(s: state, x: str, expr: ArithExpr) -> state:
     if res is None: return None
     return s | { x: res }
 
-def reduce_state(s: state,c: BoolExpr) -> state:
-    if s is None: return s
+def reduce_state(s: state, c: BoolExpr) -> state:
+    if s is None:
+        return s
+
     match c:
-        # To be completed (see course's slides)
-        case _: return s
+        case BEEq(AEVar(x), expr):
+            return reduce_eq_sign(s, x, expr)
+        case BEEq(expr, AEVar(x)):
+            return reduce_eq_sign(s, x, expr)
+
+        case BELeq(AEVar(x), expr):
+            return reduce_upper_bound(s, x, expr)
+        case BELeq(expr, AEVar(x)):
+            return reduce_lower_bound(s, x, expr)
+
+        case BENeg(BEEq(AEVar(x), expr)):
+            return reduce_neq_sign(s, x, expr)
+        case BENeg(BEEq(expr, AEVar(x))):
+            return reduce_neq_sign(s, x, expr)
+
+        case BENeg(BELeq(AEVar(x), expr)):
+            return reduce_strict_lower_bound(s, x, expr)
+        case BENeg(BELeq(expr, AEVar(x))):
+            return reduce_strict_upper_bound(s, x, expr)
+
+        case _:
+            return s
 
 class Sign_interp(Transfer[state]):
     variables: frozenset[str]