Setting bound in if_exprt for constant arrays

Characters arrays used for strings are either infinite length or
constant array with fixed length (ID_array).
In this latter case we need to set up the bound of axioms accordingly.

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -294,12 +294,21 @@ void string_constraint_generatort::add_axioms_for_if_array(
   // a1 : forall qvar2<max_length, !cond => lhs[qvar] = f[qvar]
   symbol_exprt qvar=fresh_univ_index("QA_array_if_true", index_type);
   equal_exprt qequal(index_exprt(lhs, qvar), index_exprt(t, qvar));
-  string_constraintt a1(qvar, max_length, expr.cond(), qequal);
+
+  // In case t is a constant array of fixed length is does not make sense
+  // to talk about indexes exceeding this length
+  exprt upper_bound_t=
+    (t.id()==ID_array)?from_integer(t.operands().size(), index_type):max_length;
+  string_constraintt a1(qvar, upper_bound_t, expr.cond(), qequal);
   axioms.push_back(a1);
 
   symbol_exprt qvar2=fresh_univ_index("QA_array_if_false", index_type);
   equal_exprt qequal2(index_exprt(lhs, qvar2), index_exprt(f, qvar2));
-  string_constraintt a2(qvar2, max_length, not_exprt(expr.cond()), qequal2);
+  // In case f is a constant array of fixed length is does not make sense
+  // to talk about indexes exceeding this length
+  exprt upper_bound_f=
+    (f.id()==ID_array)?from_integer(f.operands().size(), index_type):max_length;
+  string_constraintt a2(qvar2, upper_bound_f, not_exprt(expr.cond()), qequal2);
   axioms.push_back(a2);
 }