Skip to content

Commit 0794f5b

Browse files
committed
Incremental SMT2: support cast from pointer to integer of different width
Do a zero extension, just like the propositional back-end does.
1 parent 9d1be21 commit 0794f5b

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -165,6 +165,8 @@ extension_for_type(const typet &type)
165165
return smt_bit_vector_theoryt::zero_extend;
166166
if(can_cast_type<bv_typet>(type))
167167
return smt_bit_vector_theoryt::zero_extend;
168+
if(can_cast_type<pointer_typet>(type))
169+
return smt_bit_vector_theoryt::zero_extend;
168170
UNREACHABLE;
169171
}
170172

0 commit comments

Comments
 (0)