boolbvt::convert_constant is now independent of bitvector representation

Author: Daniel Kroening

src/solvers/flattening/boolbv_constant.cpp

@@ -78,19 +78,12 @@ bvt boolbvt::convert_constant(const constant_exprt &expr)
           expr_type.id()==ID_c_bit_field ||
           expr_type.id()==ID_incomplete_c_enum)
   {
-    const std::string &binary=id2string(expr.get_value());
-
-    if(binary.size()!=width)
-    {
-      error().source_location=expr.find_source_location();
-      error() << "wrong value length in constant: "
-              << expr.pretty() << eom;
-      throw 0;
-    }
+    auto value = bv2integer(id2string(expr.get_value()), width, false);
 
     for(std::size_t i=0; i<width; i++)
     {
-      bool bit=(binary[binary.size()-i-1]=='1');
+      const bool bit=value.is_odd();
+      value/=2;
       bv[i]=const_literal(bit);
     }