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.

Author: thomasspriggs

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -278,6 +278,15 @@ static smt_termt convert_expr_to_smt(const constant_exprt &constant_literal)
     const auto address = 0;
     return smt_bit_vector_constant_termt{address, bit_width};
   }
+  if(constant_literal.type() == integer_typet{})
+  {
+    // This is converting integer constants into bit vectors for use with
+    // bit vector based smt logics. As bit vector widths are not specified for
+    // non bit vector types, this chooses a width based on the minimum needed
+    // to hold the integer constant value.
+    const auto value = numeric_cast_v<mp_integer>(constant_literal);
+    return smt_bit_vector_constant_termt{value, address_bits(value + 1)};
+  }
   const auto sort = convert_type_to_smt_sort(constant_literal.type());
   sort_based_literal_convertert converter(constant_literal);
   sort.accept(converter);