Skip to content

Commit ad1b927

Browse files
Replace to_integer with numeric_cast in extractbits_expr
This allows us to be a bit more explicit in the code with `has_value` rather than using an "anonymous" boolean result.
1 parent 550f37c commit ad1b927

File tree

1 file changed

+7
-4
lines changed

1 file changed

+7
-4
lines changed

src/solvers/flattening/boolbv_extractbits.cpp

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -24,16 +24,19 @@ bvt boolbvt::convert_extractbits(const extractbits_exprt &expr)
2424
throw 0;
2525
}
2626

27-
mp_integer upper_as_int, lower_as_int;
2827
auto const &src_bv = convert_bv(expr.src());
2928

29+
auto const maybe_upper_as_int = numeric_cast<mp_integer>(expr.upper());
30+
auto const maybe_lower_as_int = numeric_cast<mp_integer>(expr.lower());
31+
3032
// We only do constants for now.
3133
// Should implement a shift here.
32-
if(
33-
to_integer(expr.op1(), upper_as_int) ||
34-
to_integer(expr.op2(), lower_as_int))
34+
if(!maybe_upper_as_int.has_value() || !maybe_lower_as_int.has_value())
3535
return conversion_failed(expr);
3636

37+
auto upper_as_int = maybe_upper_as_int.value();
38+
auto lower_as_int = maybe_lower_as_int.value();
39+
3740
if(upper_as_int < 0 || upper_as_int >= src_bv.size())
3841
{
3942
error().source_location=expr.find_source_location();

0 commit comments

Comments
 (0)