Merge pull request #6008 from tautschnig/no-width

Remove ID_width expression support from solvers

Author: tautschnig

src/solvers/flattening/boolbv.cpp

@@ -109,25 +109,6 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
     return convert_with(to_with_expr(expr));
   else if(expr.id()==ID_update)
     return convert_update(to_update_expr(expr));
-  else if(expr.id()==ID_width)
-  {
-    std::size_t result_width=boolbv_width(expr.type());
-
-    if(result_width==0)
-      return conversion_failed(expr);
-
-    if(expr.operands().size()!=1)
-      return conversion_failed(expr);
-
-    std::size_t op_width = boolbv_width(to_unary_expr(expr).op().type());
-
-    if(op_width==0)
-      return conversion_failed(expr);
-
-    if(expr.type().id()==ID_unsignedbv ||
-       expr.type().id()==ID_signedbv)
-      return bv_utils.build_constant(op_width/8, result_width);
-  }
   else if(expr.id()==ID_case)
     return convert_case(expr);
   else if(expr.id()==ID_cond)

src/solvers/smt2/smt2_conv.cpp

@@ -1613,17 +1613,6 @@ void smt2_convt::convert_expr(const exprt &expr)
     INVARIANT(
       false, "byte_update ops should be lowered in prepare_for_convert_expr");
   }
-  else if(expr.id()==ID_width)
-  {
-    std::size_t result_width=boolbv_width(expr.type());
-    CHECK_RETURN(result_width != 0);
-
-    std::size_t op_width = boolbv_width(to_unary_expr(expr).op().type());
-    CHECK_RETURN(op_width != 0);
-
-    out << "(_ bv" << op_width/8
-        << " " << result_width << ")";
-  }
   else if(expr.id()==ID_abs)
   {
     const abs_exprt &abs_expr = to_abs_expr(expr);