Skip to content

Commit 55d4011

Browse files
Fix getting model for object address (unsigned -> size_t)
Bug exhibited by cbmc-java/iterator2 when run with --object-bits 35
1 parent 28d478d commit 55d4011

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/solvers/flattening/bv_pointers.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -601,7 +601,7 @@ exprt bv_pointerst::bv_get_rec(
601601
result.set_value(value);
602602

603603
pointer_logict::pointert pointer;
604-
pointer.object=integer2unsigned(binary2integer(value_addr, false));
604+
pointer.object=integer2size_t(binary2integer(value_addr, false));
605605
pointer.offset=binary2integer(value_offset, true);
606606

607607
// we add the elaborated expression as operand

0 commit comments

Comments
 (0)