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

fixing conca

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-09-01 16:34:35 -07:00
parent 39eaf62040
commit 27e3d28cfc
2 changed files with 9 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/sls/sls_bv_eval.cpp
View file

@ -362,9 +362,9 @@ namespace sls {
}
case OP_CONCAT: {
unsigned bw = 0;
for (unsigned i = e->get_num_args(); i-- > 0; ) {
for (unsigned i = e->get_num_args(); i-- > 0;) {
auto const& a = wval(e->get_arg(i));
for (unsigned j = 0; false && j < a.bw; ++j)
for (unsigned j = 0; j < a.bw; ++j)
val.eval.set(j + bw, a.get_bit(j));
bw += a.bw;
}
@ -656,7 +656,7 @@ namespace sls {
}
}
bool bv_eval::repair_down(app* e, unsigned i) {
bool bv_eval::repair_down(app* e, unsigned i) {
expr* arg = e->get_arg(i);
if (m.is_value(arg))
return false;
@ -1838,6 +1838,7 @@ namespace sls {
auto& ve = assign_value(e);
for (unsigned j = e->get_num_args() - 1; j > idx; --j)
bw += bv.get_bv_size(e->get_arg(j));
//verbose_stream() << m_bounded_pp(e, m) << " " << idx << " " << bw << "\n";
auto& a = wval(e, idx);
for (unsigned i = 0; i < a.bw; ++i)
m_tmp.set(i, ve.get(i + bw));

10
src/ast/sls/sls_bv_fixed.h
View file

@ -28,11 +28,11 @@ namespace sls {
class bv_eval;
class bv_fixed {
bv_eval& ev;
bv_terms& terms;
ast_manager& m;
bv_util& bv;
sls::context& ctx;
bv_eval& ev;
bv_terms& terms;
ast_manager& m;
bv_util& bv;
sls::context& ctx;
bool init_range(app* e, bool sign);
void propagate_range_up(expr* e);