From eaf38abf171e7b63d0f14046cd06a62f23c08923 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 7 Nov 2022 15:32:34 +0100
Subject: [PATCH] Normalize to 0 < 0 instead of 1 <= 0

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

diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp
index 2a0326ff0..f2cde7c90 100644
--- a/src/math/polysat/ule_constraint.cpp
+++ b/src/math/polysat/ule_constraint.cpp
@@ -84,7 +84,7 @@ namespace {
             if (lhs.val() <= rhs.val())
                 lhs = 0, rhs = 0;
             else
-                lhs = 1, rhs = 0;
+                lhs = 0, rhs = 0, is_positive = !is_positive;
             return;
         }
         // k <= p   -->   p - k <= - k - 1
@@ -100,9 +100,10 @@ namespace {
             rhs = 0;
             is_positive = !is_positive;
         }
-        // 2p + 1 <= 0   -->   1 <= 0
+        // 2p + 1 <= 0   -->   0 < 0
         if (rhs.is_zero() && lhs.is_never_zero()) {
-            lhs = 1;
+            lhs = 0;
+            is_positive = !is_positive;
             return;
         }
         // a*p + q <= 0   -->   p + a^-1*q <= 0   for a odd