Skip to content

Commit c483860

Browse files
author
Daniel Kroening
committed
bv_pointerst::bv_get_rec is now independent of bitvector representation
1 parent a9f2e52 commit c483860

File tree

1 file changed

+4
-1
lines changed

1 file changed

+4
-1
lines changed

src/solvers/flattening/bv_pointers.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -633,7 +633,10 @@ exprt bv_pointerst::bv_get_rec(
633633
// we treat these like bit-vector constants, but with
634634
// some additional annotation
635635

636-
constant_exprt result(value, type);
636+
const irep_idt bvrep =
637+
make_bvrep(bits, [&value](std::size_t i) { return value[value.size()-1-i]=='1'; });
638+
639+
constant_exprt result(bvrep, type);
637640

638641
pointer_logict::pointert pointer;
639642
pointer.object=integer2size_t(binary2integer(value_addr, false));

0 commit comments

Comments
 (0)