diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml index 45d99f410094db6382f78851512fb86b9685003a..2a738c5678a858b272bca174ee0842739c60b430 100644 --- a/src/lib/CoAlgLogics.ml +++ b/src/lib/CoAlgLogics.ml @@ -135,7 +135,13 @@ let mkRule_MultiModalKD sort bs defer sl : stateExpander = let f formula = if lfGetType sort formula = AxF && lfGetDest3 sort formula = r - then ignore (bsetAdd succs (lfGetDest1 sort formula)) + then + let nextf1 = (lfGetDest1 sort formula) in + bsetAdd succs nextf1; + ignore (if (bsetMem defer formula) && + (lfGetDeferral sort formula) = (lfGetDeferral sort nextf1) + then + bsetAdd defer1 nextf1;) else () in bsetIter f bs;