Dealing with typecast of string expression in string solver

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator.cpp

@@ -111,8 +111,8 @@ string_exprt string_constraint_generatort::add_axioms_for_string_expr(
   else if(unrefined_string.id()==ID_typecast)
   {
     exprt arg=to_typecast_expr(unrefined_string).op();
-    assert(refined_string_typet::is_unrefined_string_type(
-      unrefined_string.type()));
+    //assert(refined_string_typet::is_unrefined_string_type(
+    //  unrefined_string.type())); // its type could be simply Object
     exprt res=add_axioms_for_string_expr(arg);
     assert(res.type()==refined_string_typet(get_char_type()));
     s=to_string_expr(res);

src/solvers/refinement/string_refinement.cpp

@@ -136,6 +136,19 @@ bool string_refinementt::boolbv_set_equality_to_true(const equal_exprt &expr)
     debug() << "string_refinementt " << from_expr(expr.lhs()) << " <- "
             << from_expr(expr.rhs()) << eom;
 
+
+    if(expr.rhs().id()==ID_typecast)
+    {
+      exprt uncast=to_typecast_expr(expr.rhs()).op();
+      if(refined_string_typet::is_unrefined_string_type(uncast.type()))
+      {
+	debug() << "(sr) detected casted string" << eom;
+	symbol_exprt sym=to_symbol_expr(expr.lhs());
+	generator.set_string_symbol_equal_to_expr(sym, uncast);
+	return false;
+      }
+    }
+
     if(refined_string_typet::is_unrefined_string_type(type))
     {
       symbol_exprt sym=to_symbol_expr(expr.lhs());