Replace asserts

asserts are to be replaced by INVARIANT, PRECONDITION, CHECK_RETURN,
etc.

Author: Joel Allred

src/solvers/refinement/string_constraint_generator_concat.cpp

@@ -91,12 +91,12 @@ string_exprt string_constraint_generatort::add_axioms_for_concat(
   const function_application_exprt &f)
 {
   const function_application_exprt::argumentst &args=f.arguments();
-  assert(args.size()>=2);
+  PRECONDITION(args.size()>=2);
   string_exprt s1=get_string_expr(args[0]);
   string_exprt s2=get_string_expr(args[1]);
   if(args.size()!=2)
   {
-    assert(args.size()==4);
+    PRECONDITION(args.size()==4);
     return add_axioms_for_concat_substr(s1, s2, args[2], args[3]);
   }
   return add_axioms_for_concat(s1, s2);
@@ -160,7 +160,7 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_double(
   const function_application_exprt &f)
 {
   string_exprt s1=get_string_expr(args(f, 2)[0]);
-  assert(refined_string_typet::is_refined_string_type(f.type()));
+  PRECONDITION(refined_string_typet::is_refined_string_type(f.type()));
   refined_string_typet ref_type=to_refined_string_type(f.type());
   string_exprt s2=add_axioms_from_float(args(f, 2)[1], ref_type, true);
   return add_axioms_for_concat(s1, s2);
@@ -173,7 +173,7 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_float(
   const function_application_exprt &f)
 {
   string_exprt s1=get_string_expr(args(f, 2)[0]);
-  assert(refined_string_typet::is_refined_string_type(f.type()));
+  PRECONDITION(refined_string_typet::is_refined_string_type(f.type()));
   refined_string_typet ref_type=to_refined_string_type(f.type());
   string_exprt s2=add_axioms_from_float(args(f, 2)[1], ref_type, false);
   return add_axioms_for_concat(s1, s2);