fix propagator notification when ILB keeps unsat state that was found…

… by preprocessing

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) {

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

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> ());
   }