Skip to content

Commit a0f253e

Browse files
committed
Add support for converting integer constants into bit vectors
This is required for the following refactor because it requires all sub-expressions to be convertible to smt terms whereas the current implementation only requires sub expressions which are recursed into to be convertible. These integer constants which need converting can be found as sub expressions of extract bits expressions.
1 parent 3a353a6 commit a0f253e

File tree

1 file changed

+9
-0
lines changed

1 file changed

+9
-0
lines changed

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -278,6 +278,15 @@ static smt_termt convert_expr_to_smt(const constant_exprt &constant_literal)
278278
const auto address = 0;
279279
return smt_bit_vector_constant_termt{address, bit_width};
280280
}
281+
if(constant_literal.type() == integer_typet{})
282+
{
283+
// This is converting integer constants into bit vectors for use with
284+
// bit vector based smt logics. As bit vector widths are not specified for
285+
// non bit vector types, this chooses a width based on the minimum needed
286+
// to hold the integer constant value.
287+
const auto value = numeric_cast_v<mp_integer>(constant_literal);
288+
return smt_bit_vector_constant_termt{value, address_bits(value + 1)};
289+
}
281290
const auto sort = convert_type_to_smt_sort(constant_literal.type());
282291
sort_based_literal_convertert converter(constant_literal);
283292
sort.accept(converter);

0 commit comments

Comments
 (0)