From 437e83f6debdf01365a189e8e753abed46e36072 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 23 Aug 2022 08:20:32 -0700
Subject: [PATCH] fixmul negative case

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/simplify_clause.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/math/polysat/simplify_clause.cpp b/src/math/polysat/simplify_clause.cpp
index bba5d7433..4b8231479 100644
--- a/src/math/polysat/simplify_clause.cpp
+++ b/src/math/polysat/simplify_clause.cpp
@@ -40,7 +40,8 @@ namespace polysat {
         pdd r(m);
         v = p - p.offset();
         r = p - v;
-        if (p.leading_coefficient() < 0) {
+        auto const& lc = p.leading_coefficient();
+        if (mod(-lc, m.two_to_N()) < lc) {
             v = -v;
             r -= m.mk_var(max_var);
         }