mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-02-28 17:22:20 +00:00
parent 5455603910
commit 803f0f0c65
1 changed files with 4 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/ast/sls/bv_sls_eval.cpp
View file

@ -504,8 +504,7 @@ namespace bv {
val.set(m_tmp); val.set(m_tmp);
} }
else { else {
for (unsigned i = 0; i < a.nw; ++i) a.set_zero(m_tmp);
m_tmp[i] = 0;
for (unsigned i = 0; i < a.bw; ++i) for (unsigned i = 0; i < a.bw; ++i)
m_tmp.set(i, i + sh < a.bw && a.get_bit(i + sh)); m_tmp.set(i, i + sh < a.bw && a.get_bit(i + sh));
if (sign) if (sign)
@ -516,8 +515,7 @@ namespace bv {
} }
case OP_SIGN_EXT: { case OP_SIGN_EXT: {
auto& a = wval(e->get_arg(0)); auto& a = wval(e->get_arg(0));
for (unsigned i = 0; i < a.bw; ++i) a.get(m_tmp);
m_tmp.set(i, a.get_bit(i));
bool sign = a.sign(); bool sign = a.sign();
val.set_range(m_tmp, a.bw, val.bw, sign); val.set_range(m_tmp, a.bw, val.bw, sign);
val.set(m_tmp); val.set(m_tmp);
@ -525,8 +523,7 @@ namespace bv {
} }
case OP_ZERO_EXT: { case OP_ZERO_EXT: {
auto& a = wval(e->get_arg(0)); auto& a = wval(e->get_arg(0));
for (unsigned i = 0; i < a.bw; ++i) a.get(m_tmp);
m_tmp.set(i, a.get_bit(i));
val.set_range(m_tmp, a.bw, val.bw, false); val.set_range(m_tmp, a.bw, val.bw, false);
val.set(m_tmp); val.set(m_tmp);
break; break;
@ -1367,9 +1364,7 @@ namespace bv {
return a.set_repair(random_bool(), m_tmp); return a.set_repair(random_bool(), m_tmp);
} }
for (unsigned i = 0; i < a.nw; ++i) b.get_variant(m_tmp2, m_rand);
m_tmp2[i] = random_bits();
b.clear_overflow_bits(m_tmp2);
while (b.bits() < m_tmp2) while (b.bits() < m_tmp2)
m_tmp2.set(b.msb(m_tmp2), false); m_tmp2.set(b.msb(m_tmp2), false);
while (a.set_add(m_tmp3, m_tmp, m_tmp2)) while (a.set_add(m_tmp3, m_tmp, m_tmp2))