Concretize arrays in axioms when string solver checks axioms

This makes the string solver more likely to come up with a solution to
the formulas that are passed to it.

Author: romainbrenguier

src/solvers/refinement/string_refinement.cpp

@@ -1140,21 +1140,25 @@ bool string_refinementt::check_axioms()
 
     exprt negaxiom=negation_of_constraint(axiom_in_model);
 
-    debug() << "  - axiom:\n"
-            << "     " << from_expr(ns, "", axiom) << eom;
-    debug() << "  - axiom_in_model:\n"
-            << "     " << from_expr(ns, "", axiom_in_model) << eom;
-    debug() << "  - negated_axiom:\n"
-            << "     " << from_expr(ns, "", negaxiom) << eom;
-
-    substitute_array_access(negaxiom, true);
-
-    debug() << "  - negated_axiom_without_array_access:\n"
-            << "     " << from_expr(ns, "", negaxiom) << eom;
-
+    debug() << "  "<< i << ".\n"
+            << "    - axiom:\n"
+            << "       " << from_expr(ns, "", axiom) << eom;
+    debug() << "    - axiom_in_model:\n"
+            << "       " << from_expr(ns, "", axiom_in_model) << eom;
+    debug() << "    - negated_axiom:\n"
+            << "       " << from_expr(ns, "", negaxiom) << eom;
+
+    exprt with_concretized_arrays=concretize_arrays_in_expression(
+      negaxiom, generator.max_string_length);
+    debug() << "    - negated_axiom_with_concretized_array_access:\n"
+            << "       " << from_expr(ns, "", with_concretized_arrays) << eom;
+
+    substitute_array_access(with_concretized_arrays);
+    debug() << "    - negated_axiom_without_array_access:\n"
+            << "       " << from_expr(ns, "", with_concretized_arrays) << eom;
     exprt witness;
 
-    bool is_sat=is_axiom_sat(negaxiom, univ_var, witness);
+    bool is_sat=is_axiom_sat(with_concretized_arrays, univ_var, witness);
 
     if(is_sat)
     {