diff --git a/mc.cc b/mc.cc
index 95c82c3..9300923 100644
--- a/mc.cc
+++ b/mc.cc
@@ -350,6 +350,10 @@ BDD ModelChecker::getStatesRSCTLK(const FormRSCTLK *form)
     auto proc_id = srs->rs->getProcessID(form->getSingleAgent());
     return statesNK(getStatesRSCTLK(form->getLeftSF()) * *reach, proc_id) * *reach;
   }
+  else if (oper == RSCTLK_UK) {
+    auto proc_id = srs->rs->getProcessID(form->getSingleAgent());
+    return *reach - (statesNK(*reach - getStatesRSCTLK(form->getLeftSF()), proc_id) * *reach);
+  }
 
   assert(0); // Should never happen
   return BDD_FALSE;