mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-08 04:01:22 +00:00
Code Activity

fix #3402

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-19 10:07:28 -07:00
parent 1380a98a17
commit d2886a46b7
1 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/tactic/arith/eq2bv_tactic.cpp
View file

@ -267,6 +267,10 @@ public:
else { else {
++kv.m_value; ++kv.m_value;
} }
if (m_bounds.has_lower(kv.m_key, val, strict)) {
SASSERT(!strict);
if (val.get_unsigned() > kv.m_value) kv.m_value = val.get_unsigned();
}
unsigned p = next_power_of_two(kv.m_value); unsigned p = next_power_of_two(kv.m_value);
if (p <= 1) p = 2; if (p <= 1) p = 2;
if (kv.m_value == p) p *= 2; if (kv.m_value == p) p *= 2;