Skip to content

Commit 6a4731b

Browse files
committed
bv_pointerst::offset_arithmetic: de-duplicate code
Fall back to existing variant of bv_pointerst::offset_arithmetic rather than duplicating a particular branch of that implementation.
1 parent 66d9d17 commit 6a4731b

File tree

1 file changed

+2
-7
lines changed

1 file changed

+2
-7
lines changed

src/solvers/flattening/bv_pointers.cpp

Lines changed: 2 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -830,13 +830,8 @@ bvt bv_pointerst::offset_arithmetic(
830830
{
831831
const std::size_t offset_bits = bv_pointers_width.get_offset_width(type);
832832

833-
bvt bv1 = offset_literals(bv, type);
834-
835-
bvt bv2=bv_utils.build_constant(x, offset_bits);
836-
837-
bvt tmp=bv_utils.add(bv1, bv2);
838-
839-
return object_offset_encoding(object_literals(bv, type), tmp);
833+
return offset_arithmetic(
834+
type, bv, 1, bv_utils.build_constant(x, offset_bits));
840835
}
841836

842837
bvt bv_pointerst::offset_arithmetic(

0 commit comments

Comments
 (0)