Replace throw and assert in boolbv_extractbit

The throw was on checking if a constant expression with extractbit was a valid
integer expression.

The assert was signaling that we didn't support a type of expression so has been
replaced with a throw of the appropriate exception type

Author: hannes-steffenhagen-diffblue

src/solvers/flattening/boolbv_extractbit.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
+#include <util/exception_utils.h>
 
 literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
 {
@@ -22,10 +23,7 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
   // constant?
   if(expr.index().is_constant())
   {
-    mp_integer index_as_integer;
-
-    if(to_integer(expr.index(), index_as_integer))
-      throw "extractbit failed to convert constant index";
+    mp_integer index_as_integer = numeric_cast_v<mp_integer>(expr.index());
 
     if(index_as_integer < 0 || index_as_integer >= src_bv.size())
       return prop.new_variable(); // out of range!
@@ -37,8 +35,7 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
     expr.src().type().id() == ID_verilog_signedbv ||
     expr.src().type().id() == ID_verilog_unsignedbv)
   {
-    // TODO
-    assert(false);
+    throw unsupported_operation_exceptiont("extractbit expression not implemented for verilog integers in flattening solver");
   }
   else
   {