A few further fixes to issues found while testing with CaDiCal

marekpiotrow · May 8, 2024 · b4ba41f · b4ba41f
1 parent 79ec525
commit b4ba41f
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 5 deletions.
diff --git a/MsSolver.cc b/MsSolver.cc
@@ -865,6 +865,7 @@ void MsSolver::maxsat_solve(solve_Command cmd)
             convertPbs(false);
         }
       } else { // UNSAT returned
+        if (sat_solver.conflict.size() == 0) break;          // unconditional UNSAT
         sat_solver.conflict.copyTo(sat_conflicts);
         if (global_assumptions.size() > 0 || harden_assump.size() > 0) {
             int j = 0;
@@ -1196,10 +1197,10 @@ void MsSolver::maxsat_solve(solve_Command cmd)
     if (ipamir_used) reset_soft_cls(soft_cls, fixed_soft_cls, modified_soft_cls, goal_gcd);
 #ifdef USE_SCIP
     char test = OPT_NONE;
-    bool MSAT_found_opt = satisfied && !asynch_interrupt && cmd != sc_FirstSolution && best_goalvalue < Int_MAX
+    bool MSAT_found_opt = (!satisfied || satisfied && !asynch_interrupt && cmd != sc_FirstSolution && best_goalvalue < Int_MAX)
                           && opt_finder.compare_exchange_strong(test, OPT_MSAT);
 #else
-    bool MSAT_found_opt = satisfied && !asynch_interrupt && cmd != sc_FirstSolution && best_goalvalue < Int_MAX;
+    bool MSAT_found_opt = !satisfied || satisfied && !asynch_interrupt && cmd != sc_FirstSolution && best_goalvalue < Int_MAX;
 #endif
 			  ;
     if (opt_verbosity >= 1 && opt_output_top < 0){

diff --git a/ScipSolver.cc b/ScipSolver.cc
@@ -129,10 +129,12 @@ lbool scip_solve_async(SCIP *scip, std::vector<SCIP_VAR *> vars, std::vector<lbo
             solver->printStats(true);
             return l_True;
         } else {
+            std::lock_guard<std::mutex> lck(optsol_mtx);
             found_opt = l_False;
-            if (opt_verbosity > 0) reportf("SCIP result: UNSATISFIABLE\n");
-            if (!solver->ipamir_used) { 
-                printf("s UNSATISFIABLE\n");
+            char test = OPT_NONE;
+            if (!solver->ipamir_used && opt_finder.compare_exchange_strong(test, OPT_SCIP) ) { 
+                if (opt_verbosity > 0) reportf("SCIP result: UNSATISFIABLE\n");
+                printf("s UNSATISFIABLE\n"); fflush(stdout);
                 std::_Exit(20);
             }
         }