From 8855163ccfcac208034c980aa81aa286ac65987c Mon Sep 17 00:00:00 2001
From: Clemens Eisenhofer <Clemens.Eisenhofer@tuwien.ac.at>
Date: Sat, 10 Dec 2022 22:29:31 +0100
Subject: [PATCH] Fixed justification (justification may not contain
 consequence)

---
 src/sat/smt/xor_gaussian.cpp | 6 +++---
 src/sat/smt/xor_solver.cpp   | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/sat/smt/xor_gaussian.cpp b/src/sat/smt/xor_gaussian.cpp
index 583a5596c..b7632ed00 100644
--- a/src/sat/smt/xor_gaussian.cpp
+++ b/src/sat/smt/xor_gaussian.cpp
@@ -69,8 +69,8 @@ void PackedRow::get_reason(literal_vector& antecedents, const unsigned_vector& c
             SASSERT((*this)[col] == 1);
             unsigned var = column_to_var[col];
             if (var == prop.var()) {
-                antecedents.push_back(prop); 
-                std::swap(antecedents[0], antecedents.back());
+                // In Z3 we should not have the antecedents in the justification
+                //antecedents.push_back(prop); 
             }
             else 
                 antecedents.push_back(literal(var, !tmp_col2[col]));
@@ -373,7 +373,7 @@ std::ostream& EGaussian::display(std::ostream& out) const {
     if (m_mat.num_rows() == 0)
         return out;
     for (auto const& row : m_mat) {
-        bool first = true;
+        bool first = true; 
         for (int i = 0; i < row.get_size() * 64; ++i) {
             if (row[i]) {
                 if (first)
diff --git a/src/sat/smt/xor_solver.cpp b/src/sat/smt/xor_solver.cpp
index 675d66d27..c58c707de 100644
--- a/src/sat/smt/xor_solver.cpp
+++ b/src/sat/smt/xor_solver.cpp
@@ -127,7 +127,7 @@ namespace xr {
         }
     }
 
-    void solver::asserted(sat::literal l) {        
+    void solver::asserted(literal l) {        
         TRACE("xor", tout << "asserted: " << l << "\n";);
         force_push();
         m_prop_queue.push_back(l);
@@ -699,7 +699,7 @@ namespace xr {
             while (!m_interesting.empty()) {
     
                 // Pop and check if it can be XOR-ed together
-                const unsigned v = m_interesting.back();
+                bool_var v = m_interesting.back();
                 m_interesting.pop_back();
                 if (m_occ_cnt[v] != 2)
                     continue;
@@ -707,7 +707,7 @@ namespace xr {
                 unsigned indexes[2];
                 unsigned at = 0;
                 unsigned_vector& ws = occurs[v];
-                for (unsigned i : ws) 
+                for (bool_var i : ws) 
                     if (!xors[i].empty()) 
                         indexes[at++] = i;
                 SASSERT(at == 2);