Merge pull request #2962 from xbauch/cleanup_refinement

Cleanup error handling in solvers/refinement

Author: tautschnig

src/solvers/refinement/refine_arrays.cpp

@@ -95,13 +95,10 @@ void bv_refinementt::arrays_overapproximated()
       lazy_array_constraints.erase(it++);
       break;
     default:
-      error() << "error in array over approximation check" << eom;
       INVARIANT(
         false,
         string_refinement_invariantt("error in array over approximation "
           "check"));
-      // Placeholder to tell the compiler we bail
-      throw 0;
     }
   }
 

src/solvers/refinement/string_constraint_generator_format.cpp

@@ -365,7 +365,6 @@ add_axioms_for_format_specifier(
                     << message.eom;
     INVARIANT(
       false, "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
-    throw 0;
   }
 }
 

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -554,10 +554,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_char_literal(
   }
   else
   {
-    // convert_char_literal unimplemented
     UNIMPLEMENTED;
-    // For the compiler
-    throw 0;
   }
 }