From f7a7b9e1f4678b16903c8d711acdd66649aeb602 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 26 Apr 2020 20:22:02 -0700
Subject: [PATCH] fix #4108

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/pb2bv_rewriter.cpp | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp
index d1714b794..bf9659e43 100644
--- a/src/ast/rewriter/pb2bv_rewriter.cpp
+++ b/src/ast/rewriter/pb2bv_rewriter.cpp
@@ -819,7 +819,9 @@ struct pb2bv_rewriter::imp {
                     return false;
                 }
             }
-            if (m.is_ite(a, c, th, el) && au.is_numeral(th, r1) && au.is_numeral(el, r2)) {
+            if (m.is_ite(a, c, th, el) && 
+                au.is_numeral(th, r1) && 
+                au.is_numeral(el, r2)) {
                 r1 *= mul;
                 r2 *= mul;
                 if (r1 < r2) {
@@ -832,7 +834,7 @@ struct pb2bv_rewriter::imp {
                     m_coeffs.push_back(r1-r2);
                     m_k -= r2;
                 }
-                return m_k.is_int();
+                return m_k.is_int() && (r1-r2).is_int();
             }
             return false;
         }