diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-11-14 00:29:50 +0000 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-11-14 00:29:50 +0000 |
| commit | 8c6c93e0b65e67046ed654886b1294dcc6667687 (patch) | |
| tree | dee2d44cfcad7ce57ca0c530955c372d87cdc53c /src/prop | |
| parent | 0b1bc92ea30fd851e35db6728939cc0b33f03397 (diff) | |
fix a race problem. due to interrupt mechanism minisat returned true instead of undef.
Diffstat (limited to 'src/prop')
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index b5d524c31..ba36ac879 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -1250,6 +1250,9 @@ lbool Solver::solve_() curr_restarts++; } + if(!withinBudget()) + status = l_Undef; + if (verbosity >= 1) printf("===============================================================================\n"); |