Note type inconsistencies in solver axioms and avoid simplifying

Author: tautschnig

src/solvers/strings/string_constraint_generator_main.cpp

@@ -120,6 +120,8 @@ array_string_exprt array_poolt::make_char_array_for_char_pointer(
         if_expr.cond(),
         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
     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

@@ -917,7 +917,18 @@ static optionalt<exprt> get_array(
 {
   const auto eom = messaget::eom;
   const exprt &size = arr.length();
-  exprt arr_val = simplify_expr(super_get(arr), ns);
+  exprt s = super_get(arr);
+  while(s.id() == ID_if)
+  {
+    const exprt simp_cond = simplify_expr(to_if_expr(s).cond(), ns);
+    if(simp_cond.is_true())
+      s = to_if_expr(s).true_case();
+    else if(simp_cond.is_false())
+      s = to_if_expr(s).false_case();
+    else
+      break;
+  }
+  exprt arr_val = simplify_expr(s, ns);
   exprt size_val = super_get(size);
   size_val = simplify_expr(size_val, ns);
   const typet char_type = arr.type().subtype();