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();