Setting the default of integer_of_expr to 0

This function is only used for getting some strings from the current
valuation given by the string solver, so if the value is not a valid
constant, we can replace it by 0 to get one possible valuation.

Author: romainbrenguier

src/solvers/refinement/string_refinement.cpp

@@ -282,29 +282,29 @@ void string_refinementt::add_lemma(const exprt &lemma, bool add_to_index_set)
     cur.push_back(lemma);
 }
 
-int integer_of_expr(const constant_exprt & expr)
+unsigned integer_of_expr(const constant_exprt & expr)
 {
   mp_integer i;
-  assert(!to_integer(expr,i));
+  if(to_integer(expr,i))
+    return 0;
   if(i<0)
-    return -integer2unsigned(-i);
+    return 0;
   else
     return integer2unsigned(i);
 }
 
 std::string string_refinementt::string_of_array(const exprt &arr, const exprt &size)
 {
   if(size.id() != ID_constant) return "string of unknown size";
-  int n = integer_of_expr(to_constant_expr(size));
-  if(n<0) return "string of wrong size";
+  unsigned n=integer_of_expr(to_constant_expr(size));
   if(n>500) return "very long string";
   if(n==0) return "\"\"";
   unsigned str[n];
   exprt val = get(arr);
   if(val.id() == "array-list") {
     for (size_t i = 0; i < val.operands().size()/2; i++) {
       exprt index = val.operands()[i*2];
-      int idx = integer_of_expr(to_constant_expr(index));
+      unsigned idx = integer_of_expr(to_constant_expr(index));
       if(idx<n)
       {
 	exprt value = val.operands()[i*2+1];