From d32591550468e6a9e46287c7fbef9a9eebd10950 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 24 Nov 2024 10:50:02 +0000 Subject: [PATCH] SMT2: allow natural-typed shift distance This adds conversion for shifts with natural-typed shift distance (in addition to integer-typed) to the SMT2 backend. --- src/solvers/smt2/smt2_conv.cpp | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 2402bb8ca92..7feb8835f7b 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -1586,7 +1586,8 @@ void smt2_convt::convert_expr(const exprt &expr) // SMT2 requires the shift distance to have the same width as // the value that is shifted -- odd! - if(shift_expr.distance().type().id() == ID_integer) + const auto &distance_type = shift_expr.distance().type(); + if(distance_type.id() == ID_integer || distance_type.id() == ID_natural) { const mp_integer i = numeric_cast_v(to_constant_expr(shift_expr.distance())); @@ -1597,13 +1598,12 @@ void smt2_convt::convert_expr(const exprt &expr) convert_expr(tmp); } else if( - shift_expr.distance().type().id() == ID_signedbv || - shift_expr.distance().type().id() == ID_unsignedbv || - shift_expr.distance().type().id() == ID_c_enum || - shift_expr.distance().type().id() == ID_c_bool) + distance_type.id() == ID_signedbv || + distance_type.id() == ID_unsignedbv || + distance_type.id() == ID_c_enum || distance_type.id() == ID_c_bool) { std::size_t width_op0 = boolbv_width(shift_expr.op().type()); - std::size_t width_op1 = boolbv_width(shift_expr.distance().type()); + std::size_t width_op1 = boolbv_width(distance_type); if(width_op0==width_op1) convert_expr(shift_expr.distance()); @@ -1621,9 +1621,11 @@ void smt2_convt::convert_expr(const exprt &expr) } } else + { UNEXPECTEDCASE( "unsupported distance type for " + shift_expr.id_string() + ": " + - type.id_string()); + distance_type.id_string()); + } out << ")"; // bv*sh }