From de43e051022235a8125c8e57d244bf6821486f4c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 29 Aug 2019 22:33:25 -0300
Subject: [PATCH] fix overflow bug exposed by #2476

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_pb.cpp | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index c1122878a69..8485b10d09e 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -1597,6 +1597,9 @@ namespace smt {
                 value += coeff;
             }
         }
+        if (value >= 0) {
+            display_resolved_lemma(verbose_stream() << "not validated\n");
+        }
         // std::cout << "bound: " << m_bound << " value " << value << " coeffs: " << m_active_vars.size() << " lemma is " << (value >= 0 ? "sat" : "unsat") << "\n";    
         return value < 0;
     }
@@ -1804,8 +1807,8 @@ namespace smt {
         }
         if (g >= 2) {
             normalize_active_coeffs();
-            for (unsigned i = 0; i < m_active_vars.size(); ++i) {
-                m_coeffs[m_active_vars[i]] /= g;                
+            for (auto v : m_active_vars) {
+                m_coeffs[v] /= static_cast<int>(g);                
             }
             m_bound = (m_bound + g - 1) / g;
             TRACE("pb", display_resolved_lemma(tout << "cut\n"););