diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 81eb2ffee7fb10a0a0dd2a2528ecb5d85a223958..202a29f2a10c0487b840fe22092fb979e730d179 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -538,14 +538,17 @@ let insertRule state dep (chldrn: (sort * bset) list junction) : bool option =
     in
     junctionEvalBoolOption (junc (List.map child2satState children))
   in
-  let isUnsat = (satStateChildren = Some false) in
   (* find out satisfiability *)
   let idx = stateAddRule state dep (List.rev children) in
   List.iter (fun c -> coreAddParent c state idx) children;
-  if isUnsat then begin
-    propagateUnsat [UState (state, Some idx)];
-    Some false
-  end else None
+  match satStateChildren with
+  | Some false -> (* definitely unsat *)
+        propagateUnsat [UState (state, Some idx)];
+        Some false
+  | Some true ->
+        (* TODO: propagateSat ? *)
+        Some true
+  | None -> None
 
     (* tells whether it is satisfiable:
         Some true -> surely satisfiable