From 74d8497ed9ff1cab60e15f2509d1abc7f6ac398f Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Tue, 27 Sep 2022 17:53:45 +0200
Subject: [PATCH] Fix subsumption for unilinear case

---
 src/math/polysat/simplify_clause.cpp | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/math/polysat/simplify_clause.cpp b/src/math/polysat/simplify_clause.cpp
index 010f1ae18..8fe76514d 100644
--- a/src/math/polysat/simplify_clause.cpp
+++ b/src/math/polysat/simplify_clause.cpp
@@ -67,11 +67,17 @@ namespace polysat {
      * \param[out] v Body
      */
     pdd simplify_clause::abstract(pdd const& p, pdd& v) {
-        if (p.is_val())
+        if (p.is_val()) {
+            SASSERT(v.is_zero());
             return p;
+        }
         if (p.is_unilinear()) {
-            v = p.manager().mk_var(p.var());
-            return p;
+            // we need an interval with coeff == 1 to be able to compare intervals easily
+            auto const& coeff = p.hi().val();
+            if (coeff.is_one() || coeff == p.manager().max_value()) {
+                v = p.manager().mk_var(p.var());
+                return p;
+            }
         }
         unsigned max_var = p.var();
         auto& m = p.manager();