fix bound sharing

ortools/sat/integer_search.cc

@@ -415,11 +415,14 @@ SatSolver::Status SolveProblemWithPortfolioSearch(
       policy_index = (policy_index + 1) % num_policies;
     }
 
-    LevelZeroCallbackHelper* level_zero_callbacks =
-        model->GetOrCreate<LevelZeroCallbackHelper>();
-    for (const auto& cb : level_zero_callbacks->callbacks) {
-      if (!cb) {
-        return solver->UnsatStatus();
+    if (solver->CurrentDecisionLevel() == 0) {
+      auto* level_zero_callbacks =
+          model->GetOrCreate<LevelZeroCallbackHelper>();
+      for (const auto& cb : level_zero_callbacks->callbacks) {
+        if (!cb()) {
+          solver->NotifyThatModelIsUnsat();
+          return SatSolver::INFEASIBLE;
+        }
       }
     }
 
@@ -456,6 +459,7 @@ SatSolver::Status SolveProblemWithPortfolioSearch(
                 IntegerLiteral::LowerOrEqual(helper->objective_var,
                                              new_objective_upper_bound),
                 {}, {})) {
+          solver->NotifyThatModelIsUnsat();
           return SatSolver::INFEASIBLE;
         }
         if (new_objective_lower_bound > current_objective_lower_bound &&
@@ -463,10 +467,11 @@ SatSolver::Status SolveProblemWithPortfolioSearch(
                 IntegerLiteral::GreaterOrEqual(helper->objective_var,
                                                new_objective_lower_bound),
                 {}, {})) {
+          solver->NotifyThatModelIsUnsat();
           return SatSolver::INFEASIBLE;
         }
         if (!solver->FinishPropagation()) {
-          return solver->UnsatStatus();
+          return SatSolver::INFEASIBLE;
         }
       }
     }

ortools/sat/integer_search.h

@@ -123,6 +123,7 @@ struct ObjectiveSynchronizationHelper {
 };
 
 // Callbacks that be called when the search goes back to level 0.
+// Callbacks should return false if the propagation fails.
 struct LevelZeroCallbackHelper {
   std::vector<std::function<bool()>> callbacks;
 };

ortools/sat/synchronization.cc

@@ -233,6 +233,9 @@ void RegisterVariableBoundsLevelZeroWatcher(
         return false;
       }
     }
+    if (!model->GetOrCreate<SatSolver>()->FinishPropagation()) {
+      return false;
+    }
     return true;
   };
   model->GetOrCreate<LevelZeroCallbackHelper>()->callbacks.push_back(