From e7c9112beba48b741c01355316c7f512e89935a0 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Fri, 21 Jul 2023 12:45:46 +0200
Subject: [PATCH] bugfix

---
 src/math/polysat/slicing.cpp | 7 +++++--
 src/test/slicing.cpp         | 2 +-
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp
index 4f06f2844..6c4e011ea 100644
--- a/src/math/polysat/slicing.cpp
+++ b/src/math/polysat/slicing.cpp
@@ -610,8 +610,11 @@ namespace polysat {
             SASSERT(!has_sub(x));
             SASSERT(!has_sub(y));
             if (width(x) == width(y)) {
-                if (!merge_base(x, y, dep))
+                if (!merge_base(x, y, dep)) {
+                    xs.clear();
+                    ys.clear();
                     return false;
+                }
             }
             else if (width(x) > width(y)) {
                 // need to split x according to y
@@ -785,7 +788,7 @@ namespace polysat {
                 continue;
             pdd const body = a.is_one() ? (m.mk_var(x) - p) : (m.mk_var(x) + p);
             // c is either x = body or x != body, depending on polarity
-            LOG("Equation from lit(" << c.blit() << ")  " << c << ":  v" << x << " = " << body);
+            LOG("Equation from lit(" << c.blit() << ")  " << c << ":  v" << x << (c.is_positive() ? " = " : " != ") << body);
             if (!add_equation(x, body, c.blit())) {
                 SASSERT(is_conflict());
                 return;
diff --git a/src/test/slicing.cpp b/src/test/slicing.cpp
index bf7644ba5..e7c624957 100644
--- a/src/test/slicing.cpp
+++ b/src/test/slicing.cpp
@@ -318,7 +318,7 @@ void tst_slicing() {
     using namespace polysat;
     test_slicing::test1();
     test_slicing::test2();
-    // test_slicing::test3();
+    test_slicing::test3();
     test_slicing::test4();
     test_slicing::test5();
     test_slicing::test6();