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 c1122878a..8485b10d0 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"););