diff --git a/src/math/polysat/simplify_clause.cpp b/src/math/polysat/simplify_clause.cpp
index 92464838e..089d91b10 100644
--- a/src/math/polysat/simplify_clause.cpp
+++ b/src/math/polysat/simplify_clause.cpp
@@ -40,6 +40,21 @@ Notes:
         ==> drop 294 because it implies 295
         ==> drop 292 because it implies 295
 
+
+    TODO from bench0:
+	-43 \/ 3 \/ 4 \/ -0 \/ -44 \/ -52
+		-43: v3 + -1 != 0
+		3: v3 == 0
+		4: v3 <= v5
+		-0: v5 + v4*v3 + -1*v2*v1 != 0
+		-44: v4 + -1 != 0
+		-52: v2 != 0
+
+        Drop v3 == 0 because it implies v3 - 1 != 0
+
+    The try_recognize_bailout returns true, but fails to simplify any other literal.
+    Overall, why return true immediately if there are other literals that subsume each-other?
+
 --*/
 #include "math/polysat/solver.h"
 #include "math/polysat/simplify_clause.h"
@@ -110,6 +125,8 @@ namespace polysat {
                 });
             }
         }
+        if (j == cl.size())
+            return false;
         cl.m_literals.shrink(j);
         return true;
     }
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 590d3f08b..2be1df738 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -890,8 +890,10 @@ namespace polysat {
                 UNREACHABLE();
             }
         }
-        for (auto cl : side_lemmas)
+        for (auto cl : side_lemmas) {
+            m_simplify_clause.apply(*cl);
             add_clause(*cl);
+        }
         SASSERT(lemma_invariant_part2(lemma_invariant_todo));
         learn_lemma(lemma);
     }
diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp
index 17e6e7b13..615d154b8 100644
--- a/src/test/polysat.cpp
+++ b/src/test/polysat.cpp
@@ -354,6 +354,27 @@ namespace polysat {
             s.expect_sat();
         }
 
+        //
+	// -43 \/ 3 \/ 4 
+        //   -43: v3 + -1 != 0
+        //   3: v3 == 0
+        //   4: v3 <= v5
+
+        static void test_clause_simplify1() {
+            scoped_solver s(__func__);
+            simplify_clause simp(s);
+            clause_builder cb(s);
+            auto u = s.var(s.add_var(4));
+            auto v = s.var(s.add_var(4));
+            cb.push(s.eq(u));
+            cb.push(~s.eq(u - 1));
+            cb.push(s.ule(u, v));
+            auto cl = cb.build();
+            simp.apply(*cl);
+            std::cout << *cl << "\n";
+            SASSERT(cl->size() == 2);
+        }
+
 
         /**
          * Check unsat of:
@@ -1409,6 +1430,8 @@ namespace polysat {
 void tst_polysat() {
     using namespace polysat;
 
+    test_polysat::test_clause_simplify1();
+
     // test_polysat::test_add_conflicts();  // ok
     // test_polysat::test_wlist();  // ok
     // test_polysat::test_cjust();  // uses viable_fallback; weak lemmas