From 5f27b328ad646b6589736a8c404dbeaf91816bd0 Mon Sep 17 00:00:00 2001
From: Mate Soos <soos.mate@gmail.com>
Date: Sat, 13 Jul 2024 21:47:13 +0200
Subject: [PATCH] Fixing bug

---
 src/main.cpp   |  2 +-
 src/solver.cpp | 36 ++++++++++++------------------------
 2 files changed, 13 insertions(+), 25 deletions(-)

diff --git a/src/main.cpp b/src/main.cpp
index 8559874cd..d8f78ab53 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -1242,9 +1242,9 @@ int Main::solve()
     if (program.is_used("maxtime")) solver->set_max_time(program.get<double>("maxtime"));
     if (program.is_used("maxconfl")) solver->set_max_confl(program.get<uint64_t>("maxconfl"));
 
+    parse_sampling_vars();
     check_num_threads_sanity(num_threads);
     solver->set_num_threads(num_threads);
-    parse_sampling_vars();
     if (sql != 0) solver->set_sqlite(sqlite_filename);
 
     //Print command line used to execute the solver: for options and inputs
diff --git a/src/solver.cpp b/src/solver.cpp
index 481f4b0bb..1b81d8742 100644
--- a/src/solver.cpp
+++ b/src/solver.cpp
@@ -3661,28 +3661,17 @@ void Solver::detach_clauses_in_xors() {
     // Go through watchlist
     uint32_t deleted = 0;
     vector<ClOffset> delayed_clause_free;
-    for(uint32_t x = 0; x < nVars()*2; x++) {
-        Lit l = Lit::toLit(x);
-        for(const auto& w : watches[l]) {
-            if (w.isBin() || w.isBNN() || w.isIdx()) continue;
-            assert(w.isClause());
-            ClOffset offs = w.get_offset();
-            Clause* cl = cl_alloc.ptr(offs);
-            assert(!cl->freed());
-
-            //We have already went through this clause, and set it to be removed/detached
-            if (cl->red()) goto next;
-            if (cl->get_removed()) continue;
-            if (cl->size() <= maxsize_xor &&
-                    xor_hashes.count(hash_xcl(*cl)) &&
-                    check_clause_represented_by_xor(*cl)) {
-                cl->set_removed();
-                delayed_clause_free.push_back(offs);
-                deleted++;
-                continue;
-            }
-            next:
-            ;
+    for(auto offs: longIrredCls) {
+        Clause* cl = cl_alloc.ptr(offs);
+        cl->stats.marked_clause = false;
+        assert(!cl->freed());
+        assert(!cl->get_removed());
+        if (cl->size() <= maxsize_xor &&
+                xor_hashes.count(hash_xcl(*cl)) &&
+                check_clause_represented_by_xor(*cl)) {
+            detachClause(*cl);
+            cl->stats.marked_clause = true;
+            deleted++;
         }
     }
 
@@ -3691,8 +3680,7 @@ void Solver::detach_clauses_in_xors() {
         for(uint32_t i = 0; i < longIrredCls.size(); i++) {
             ClOffset offs = longIrredCls[i];
             Clause* cl = cl_alloc.ptr(offs);
-            if (cl->get_removed()) detachClause(*cl);
-            else longIrredCls[j++] = offs;
+            if (!cl->stats.marked_clause) longIrredCls[j++] = offs;
         }
         longIrredCls.resize(j);