From a049235caa3277edbd2cee28f6534e7c89f9bebf Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 18 Jun 2021 17:26:11 -0700
Subject: [PATCH] simplify output to use signed constants

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/dd/dd_pdd.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 24b93817a..9b27cf1b4 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -1460,7 +1460,10 @@ namespace dd {
             rational c = abs(m.first);
             m.second.reverse();
             if (!c.is_one() || m.second.empty()) {
-                out << c;
+                if (m_semantics == mod2N_e && mod(-c, m_mod2N) < c)
+                    out << -mod(-c, m_mod2N);
+                else 
+                    out << c;
                 if (!m.second.empty()) out << "*";
             }
             unsigned v_prev = UINT_MAX;