mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-10 09:15:47 +00:00
Code Activity

fix #2771

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-02 15:41:56 -08:00
parent 37a4dd68d0
commit 28cb13fb96
3 changed files with 14 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_utvpi.cpp
View file

@ -138,14 +138,12 @@ namespace smt {
m_coeff_map.insert_if_not_there2(e, rational(0))->get_data().m_value += mul;
}
}
obj_map<expr, rational>::iterator it = m_coeff_map.begin();
obj_map<expr, rational>::iterator end = m_coeff_map.end();
for (; it != end; ++it) {
rational r = it->m_value;
for (auto const& kv : m_coeff_map) {
rational r = kv.m_value;
if (r.is_zero()) {
continue;
}
m_terms.push_back(std::make_pair(it->m_key, r));
m_terms.push_back(std::make_pair(kv.m_key, r));
if (m_terms.size() > 2) {
return false;
}