Skip to content

Commit fdc0fc8

Browse files
committed
Use mult_overflow_exprt in smt2_convt
1 parent 533a902 commit fdc0fc8

File tree

1 file changed

+5
-4
lines changed

1 file changed

+5
-4
lines changed

src/solvers/smt2/smt2_conv.cpp

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1908,13 +1908,14 @@ void smt2_convt::convert_expr(const exprt &expr)
19081908
"overflow check should not be performed on unsupported type",
19091909
op_type.id_string());
19101910
}
1911-
else if(expr.id()==ID_overflow_mult)
1911+
else if(
1912+
const auto mult_overflow = expr_try_dynamic_cast<mult_overflow_exprt>(expr))
19121913
{
1913-
const auto &op0 = to_binary_expr(expr).op0();
1914-
const auto &op1 = to_binary_expr(expr).op1();
1914+
const auto &op0 = mult_overflow->op0();
1915+
const auto &op1 = mult_overflow->op1();
19151916

19161917
DATA_INVARIANT(
1917-
expr.type().id() == ID_bool,
1918+
mult_overflow->type().id() == ID_bool,
19181919
"overflow mult expression shall be of Boolean type");
19191920

19201921
// No better idea than to multiply with double the bits and then compare

0 commit comments

Comments
 (0)