Merge pull request #1021 from romainbrenguier/bugfix/object-get-class#272

Fix small bugs in string support related to Object.getClass

Author: Daniel Kroening

src/java_bytecode/java_string_library_preprocess.cpp

@@ -1223,6 +1223,8 @@ codet java_string_library_preprocesst::make_object_get_class_code(
       ID_cprover_string_literal_func,
       {class_identifier},
       symbol_table));
+  exprt string_expr_sym=fresh_string_expr_symbol(loc, symbol_table, code);
+  code.add(code_assignt(string_expr_sym, string_expr));
 
   // string_expr1 = substr(string_expr, 6)
   // We do this to remove the "java::" prefix
@@ -1233,6 +1235,8 @@ codet java_string_library_preprocesst::make_object_get_class_code(
       ID_cprover_string_substring_func,
       {string_expr, from_integer(6, java_int_type())},
       symbol_table));
+  exprt string_expr_sym1=fresh_string_expr_symbol(loc, symbol_table, code);
+  code.add(code_assignt(string_expr_sym1, string_expr1));
 
   // string1 = (String*) string_expr
   pointer_typet string_ptr_type(

src/solvers/refinement/string_constraint_generator_transformation.cpp

@@ -122,7 +122,7 @@ string_exprt string_constraint_generatort::add_axioms_for_substring(
   string_constraintt a4(idx,
                         res.length(),
                         equal_exprt(res[idx],
-                        str[plus_exprt_with_overflow_check(start, idx)]));
+                        str[plus_exprt(start, idx)]));
   axioms.push_back(a4);
   return res;
 }