From 46147c2fc35a304f66f2eb11becba89a0bb75ad5 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 23 Jan 2023 13:59:00 +0100
Subject: [PATCH] Fix unsoundness in ule_constraint lemma

---
 src/math/polysat/ule_constraint.cpp | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp
index 5fe9f42ea..7e8206ffb 100644
--- a/src/math/polysat/ule_constraint.cpp
+++ b/src/math/polysat/ule_constraint.cpp
@@ -240,14 +240,13 @@ namespace polysat {
 
         s.m_viable.intersect(p, q, sc);
 
-        if (first && !is_positive) {
-            if (!p.is_val())
-                // -1 > q
-                s.add_clause(~sc, s.ult(q, -1), false);
-            if (!q.is_val())
-                // p > 0
-                s.add_clause(~sc, s.ult(0, p), false);
+        if (first && !is_positive && !lhs().is_val() && !rhs().is_val()) {
+            // lhs > rhs  ==>  -1 > rhs
+            s.add_clause(~sc, s.ult(rhs(), -1), false);
+            // lhs > rhs  ==>  lhs > 0
+            s.add_clause(~sc, s.ult(0, lhs()), false);
         }
+
 #if 0
         propagate_bits(s, is_positive);
 #endif