Remove ID_width expression support from solvers

We do not seem to generate such an expression in the code base, and the
current implementation is rather dubious for it returns the multiple of
8 bits in the propositional encoding.

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);