Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 7 additions & 7 deletions src/solvers/smt2/smt2_parser.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -656,7 +656,7 @@ exprt smt2_parsert::function_application()
if(next_token() != smt2_tokenizert::NUMERAL)
throw error() << "expected numeral after " << id;

auto index = std::stoll(smt2_tokenizer.get_buffer());
auto index = string2integer(smt2_tokenizer.get_buffer());

if(next_token() != smt2_tokenizert::CLOSE)
throw error() << "expected ')' after " << id << " index";
Expand All @@ -681,21 +681,21 @@ exprt smt2_parsert::function_application()
// we first convert to a signed type of the original width,
// then extend to the new width, and then go to unsigned
const auto width = to_unsignedbv_type(op[0].type()).get_width();
const signedbv_typet small_signed_type(width);
const signedbv_typet large_signed_type(width + index);
const unsignedbv_typet unsigned_type(width + index);
const signedbv_typet small_signed_type{width};
const signedbv_typet large_signed_type{width + index};
const unsignedbv_typet unsigned_type{width + index};

return typecast_exprt(
typecast_exprt(
typecast_exprt(op[0], small_signed_type), large_signed_type),
unsigned_type);
}
else if(id=="zero_extend")
else if(id == ID_zero_extend)
{
auto width=to_unsignedbv_type(op[0].type()).get_width();
unsignedbv_typet unsigned_type(width+index);
unsignedbv_typet unsigned_type{width + index};

return typecast_exprt(op[0], unsigned_type);
return zero_extend_exprt{op[0], unsigned_type};
}
else if(id == ID_repeat)
{
Expand Down
15 changes: 15 additions & 0 deletions src/util/bitvector_types.h
Original file line number Diff line number Diff line change
Expand Up @@ -107,6 +107,11 @@ class integer_bitvector_typet : public bitvector_typet
{
}

integer_bitvector_typet(const irep_idt &id, const mp_integer &width)
: bitvector_typet(id, width)
{
}

/// Return the smallest value that can be represented using this type.
mp_integer smallest() const;
/// Return the largest value that can be represented using this type.
Expand Down Expand Up @@ -167,6 +172,11 @@ class unsignedbv_typet : public integer_bitvector_typet
{
}

explicit unsignedbv_typet(const mp_integer &width)
: integer_bitvector_typet(ID_unsignedbv, width)
{
}

static void check(
const typet &type,
const validation_modet vm = validation_modet::INVARIANT)
Expand Down Expand Up @@ -216,6 +226,11 @@ class signedbv_typet : public integer_bitvector_typet
{
}

explicit signedbv_typet(const mp_integer &width)
: integer_bitvector_typet(ID_signedbv, width)
{
}

static void check(
const typet &type,
const validation_modet vm = validation_modet::INVARIANT)
Expand Down
Loading