Handling of if_exprt in checking universal axioms of string solver

Author: romainbrenguier

src/solvers/refinement/string_refinement.cpp

@@ -859,9 +859,15 @@ exprt string_refinementt::substitute_array_with_expr(
 }
 
 /// create an equivalent expression where array accesses and 'with' expressions
-/// are replaced by 'if' expressions. e.g. for an array access arr[x], where:
-/// `arr := {12, 24, 48}` the constructed expression will be: `index==0 ? 12 :
-/// index==1 ? 24 : 48`
+/// are replaced by 'if' expressions, in particular:
+///  * for an array access `arr[x]`, where:
+///    `arr := {12, 24, 48}` the constructed expression will be:
+///    `index==0 ? 12 : index==1 ? 24 : 48`
+///  * for an array access `arr[x]`, where:
+///    `arr := array_of(12) with {0:=24} with {2:=42}` the constructed
+///    expression will be: `index==0 ? 24 : index==2 ? 42 : 12`
+///  * for an array access `(g1?arr1:arr2)[x]` where `arr1 := {12}` and
+///    `arr2 := {34}`, the constructed expression will be: `g1 ? 12 : 34`
 /// \param expr: an expression containing array accesses
 /// \return an expression containing no array access
 void string_refinementt::substitute_array_access(exprt &expr) const
@@ -892,6 +898,18 @@ void string_refinementt::substitute_array_access(exprt &expr) const
       return;
     }
 
+    if(index_expr.array().id()==ID_if)
+    {
+      // Substitute recursively in branches of conditional expressions
+      if_exprt if_expr=to_if_expr(index_expr.array());
+      exprt true_case=index_exprt(if_expr.true_case(), index_expr.index());
+      substitute_array_access(true_case);
+      exprt false_case=index_exprt(if_expr.false_case(), index_expr.index());
+      substitute_array_access(false_case);
+      expr=if_exprt(if_expr.cond(), true_case, false_case);
+      return;
+    }
+
     assert(index_expr.array().id()==ID_array);
     array_exprt &array_expr=to_array_expr(index_expr.array());