Fast path: don't check the dependency between null observers: it's dependent

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index fb1bb57..10881de 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -367,6 +367,9 @@ bool ModelChecker::requests_are_dependent(RemotePtr<kernel::actor::SimcallObserv
   m.type = MessageType::SIMCALLS_DEPENDENT;
   m.obs1 = obs1.local();
   m.obs2 = obs2.local();
+
+  if (m.obs1 == nullptr || m.obs2 == nullptr)
+    return true;
   checker_side_.get_channel().send(m);
 
   s_mc_message_simcalls_dependent_answer_t answer;

diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp
index 259155a..40fc447 100644 (file)
--- a/src/mc/remote/AppSide.cpp
+++ b/src/mc/remote/AppSide.cpp
@@ -212,11 +212,12 @@ void AppSide::handle_messages() const
         auto* obs2        = msg_simcalls->obs2;
         bool res          = true;
 
-        if (obs1 != nullptr && obs2 != nullptr)
+        if (obs1 != nullptr && obs2 != nullptr) {
           res = obs1->depends(obs2);
 
-        XBT_DEBUG("return SIMCALLS_DEPENDENT(%s, %s) = %s", obs1->to_string(0).c_str(), obs2->to_string(0).c_str(),
-                  (res ? "true" : "false"));
+          XBT_DEBUG("return SIMCALLS_DEPENDENT(%s, %s) = %s", obs1->to_string(0).c_str(), obs2->to_string(0).c_str(),
+                    (res ? "true" : "false"));
+        }
 
         // Send result:
         s_mc_message_simcalls_dependent_answer_t answer{MessageType::SIMCALLS_DEPENDENT_ANSWER, 0};