Correct bounds in instantiate method

This was not checking that the instantiate variable does not exceed the
upper bound.

Author: romainbrenguier

src/solvers/refinement/string_refinement.cpp

@@ -2128,19 +2128,19 @@ static exprt instantiate(
   const exprt &str,
   const exprt &val)
 {
-  exprt idx=find_index(axiom.body(), str, axiom.univ_var());
+  const exprt idx = find_index(axiom.body(), str, axiom.univ_var());
   if(idx.is_nil())
     return true_exprt();
 
-  exprt r=compute_inverse_function(stream, axiom.univ_var(), val, idx);
-  implies_exprt instance(axiom.premise(), axiom.body());
+  const exprt r = compute_inverse_function(stream, axiom.univ_var(), val, idx);
+  implies_exprt instance(
+    and_exprt(
+      binary_relation_exprt(axiom.univ_var(), ID_ge, axiom.lower_bound()),
+      binary_relation_exprt(axiom.univ_var(), ID_lt, axiom.upper_bound()),
+      axiom.premise()),
+    axiom.body());
   replace_expr(axiom.univ_var(), r, instance);
-  // We are not sure the index set contains only positive numbers
-  and_exprt bounds(
-    axiom.univ_within_bounds(),
-    binary_relation_exprt(from_integer(0, val.type()), ID_le, val));
-  replace_expr(axiom.univ_var(), r, bounds);
-  return implies_exprt(bounds, instance);
+  return instance;
 }
 
 /// Instantiates a quantified formula representing `not_contains` by