diff --git a/src/external.cpp b/src/external.cpp
index 4716fd17..fa97708a 100644
--- a/src/external.cpp
+++ b/src/external.cpp
@@ -392,6 +392,12 @@ void External::reset_observed_vars () {
   // Shouldn't be called if there is no connected propagator
   assert (propagator);
   reset_extended ();
+  
+  internal->notified = 0;
+  LOG ("reset notified counter to 0");
+
+  if (!is_observed.size ()) return;
+  
   assert (!max_var || (size_t) max_var + 1 == is_observed.size ());
 
   for (auto elit : vars) {
@@ -405,8 +411,8 @@ void External::reset_observed_vars () {
       melt (elit);
     }
   }
-  internal->notified = 0;
-  LOG ("reset notified counter to 0");
+  
+  
 }
 
 bool External::observed (int elit) {
diff --git a/src/internal.cpp b/src/internal.cpp
index 2b26dfcd..54fc4c36 100644
--- a/src/internal.cpp
+++ b/src/internal.cpp
@@ -602,11 +602,13 @@ void Internal::produce_failed_assumptions () {
   assert (!assumptions.empty ());
   while (!unsat) {
     assert (!satisfied ());
+    notify_assignments ();
     if (decide ())
       break;
     while (!unsat && !propagate ())
       analyze ();
   }
+  notify_assignments ();
   if (unsat)
     LOG ("formula is actually unsatisfiable unconditionally");
   else
diff --git a/src/mobical.cpp b/src/mobical.cpp
index 90c16db3..0822a87b 100644
--- a/src/mobical.cpp
+++ b/src/mobical.cpp
@@ -692,8 +692,8 @@ class MockPropagator : public ExternalPropagator {
   }
 
   void notify_new_decision_level () {
-    MLOG ("notify new decision level " << observed_trail.size () << " -> "
-                                       << observed_trail.size () + 1
+    MLOG ("notify new decision level " << observed_trail.size () -1 << " -> "
+                                       << observed_trail.size ()
                                        << std::endl);
     observed_trail.push_back (std::vector<int> ());
   }