From c25be425785f28ad91c94ca2d389226683898721 Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Fri, 20 Nov 2020 16:15:52 +0100 Subject: [PATCH] fix rare race in solution reporting --- ortools/sat/integer_search.cc | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc index d23d34e7c0..e9e518bc83 100644 --- a/ortools/sat/integer_search.cc +++ b/ortools/sat/integer_search.cc @@ -801,6 +801,12 @@ SatSolver::Status SolveIntegerProblem(Model* model) { // No decision means that we reached a leave of the search tree and that // we have a feasible solution. + // + // Tricky: If the time limit is reached during the final propagation when + // all variables are fixed, there is no guarantee that the propagation + // responsible for testing the validity of the solution was run to + // completion. So we cannot report a feasible solution. + if (time_limit->LimitReached()) return SatSolver::LIMIT_REACHED; if (decision == kNoLiteralIndex) { // Save the current polarity of all Booleans in the solution. It will be // followed for the next SAT decisions. This is known to be a good policy