replace instances of numeric_cast by numeric_cast_v

Author: Daniel Kroening

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1069,12 +1069,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
     {
       PRECONDITION(!i_it->args.empty());
 
-      auto target = numeric_cast<unsigned>(to_constant_expr(i_it->args[0]));
-      DATA_INVARIANT(
-        target.has_value(), "target expected to be unsigned integer");
-      targets.insert(target.value());
+      auto target = numeric_cast_v<unsigned>(to_constant_expr(i_it->args[0]));
+      targets.insert(target);
 
-      a_entry.first->second.successors.push_back(target.value());
+      a_entry.first->second.successors.push_back(target);
 
       if(i_it->statement=="jsr" ||
          i_it->statement=="jsr_w")
@@ -1094,11 +1092,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
       {
         if(is_label)
         {
-          auto target = numeric_cast<unsigned>(to_constant_expr(arg));
-          DATA_INVARIANT(
-            target.has_value(), "target expected to be unsigned integer");
-          targets.insert(target.value());
-          a_entry.first->second.successors.push_back(target.value());
+          auto target = numeric_cast_v<unsigned>(to_constant_expr(arg));
+          targets.insert(target);
+          a_entry.first->second.successors.push_back(target);
         }
         is_label=!is_label;
       }

jbmc/src/java_bytecode/java_local_variable_table.cpp

@@ -193,9 +193,7 @@ static bool is_store_to_slot(
   {
     // Store with an argument:
     const auto &arg=inst.args[0];
-    auto v = numeric_cast<unsigned>(to_constant_expr(arg));
-    CHECK_RETURN(v.has_value());
-    storeslotidx = v.value();
+    storeslotidx = numeric_cast_v<unsigned>(to_constant_expr(arg));
   }
   else
   {

src/solvers/refinement/string_constraint_generator_format.cpp

@@ -488,11 +488,7 @@ utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
   std::wstring out(length, '?');
 
   for(std::size_t i=0; i<arr.operands().size() && i<length; i++)
-  {
-    auto c = numeric_cast<unsigned>(to_constant_expr(arr.operands()[i]));
-    INVARIANT(c.has_value(), "constant should be convertible to unsigned");
-    out[i] = c.value();
-  }
+    out[i] = numeric_cast_v<unsigned>(to_constant_expr(arr.operands()[i]));
 
   return utf16_native_endian_to_java(out);
 }