Merge pull request #4798 from allredj/replace-array-if-exprts-before-solve

Replace array if-exprts before giving to solver

Author: Joel Allred

src/solvers/strings/array_pool.cpp

@@ -93,7 +93,9 @@ array_string_exprt array_poolt::make_char_array_for_char_pointer(
         to_array_type(t.type()).size(),
         to_array_type(f.type()).size()));
     // BEWARE: this expression is possibly type-inconsistent and must not be
-    // used for any purposes other than passing it to concretisation
+    // used for any purposes other than passing it to concretization.
+    // Array if-exprts must be replaced (using substitute_array_access) before
+    // passing the lemmas to the solver.
     return to_array_string_expr(if_exprt(if_expr.cond(), t, f, array_type));
   }
   const bool is_constant_array =

src/solvers/strings/string_refinement.cpp

@@ -738,7 +738,9 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   }
 
   for(const exprt &lemma : generator.constraints.existential)
-    add_lemma(lemma);
+  {
+    add_lemma(substitute_array_access(lemma, generator.fresh_symbol, true));
+  }
 
   // All generated strings should have non-negative length
   for(const auto &pair : generator.array_pool.created_strings())
@@ -785,7 +787,9 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   const auto initial_instances =
     generate_instantiations(index_sets, axioms, not_contain_witnesses);
   for(const auto &instance : initial_instances)
-    add_lemma(instance);
+  {
+    add_lemma(substitute_array_access(instance, generator.fresh_symbol, true));
+  }
 
   while((loop_bound_--) > 0)
   {