diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h
index 55aacd7f4d5..e72ead2495d 100644
--- a/src/solvers/refinement/string_constraint.h
+++ b/src/solvers/refinement/string_constraint.h
@@ -93,11 +93,10 @@ class string_constraintt : public exprt
     const symbol_exprt &_univ_var,
     const exprt &bound_inf,
     const exprt &bound_sup,
-    const exprt &prem,
     const exprt &body):
     exprt(ID_string_constraint)
   {
-    copy_to_operands(prem, body);
+    copy_to_operands(true_exprt(), body);
     copy_to_operands(_univ_var, bound_sup, bound_inf);
   }
 
@@ -105,24 +104,14 @@ class string_constraintt : public exprt
   string_constraintt(
     const symbol_exprt &_univ_var,
     const exprt &bound_sup,
-    const exprt &prem,
     const exprt &body):
     string_constraintt(
       _univ_var,
       from_integer(0, _univ_var.type()),
       bound_sup,
-      prem,
       body)
   {}
 
-  // Default premise is true
-  string_constraintt(
-    const symbol_exprt &_univ_var,
-    const exprt &bound_sup,
-    const exprt &body):
-    string_constraintt(_univ_var, bound_sup, true_exprt(), body)
-  {}
-
   exprt univ_within_bounds() const
   {
     return and_exprt(
diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h
index 778ede29cff..68e77136a15 100644
--- a/src/solvers/refinement/string_constraint_generator.h
+++ b/src/solvers/refinement/string_constraint_generator.h
@@ -436,4 +436,7 @@ size_t max_printed_string_length(const typet &type, unsigned long ul_radix);
 std::string
 utf16_constant_array_to_java(const array_exprt &arr, std::size_t length);
 
+/// \return expression representing the minimum of two expressions
+exprt minimum(const exprt &a, const exprt &b);
+
 #endif
diff --git a/src/solvers/refinement/string_constraint_generator_comparison.cpp b/src/solvers/refinement/string_constraint_generator_comparison.cpp
index 7b8590e7836..ca555921144 100644
--- a/src/solvers/refinement/string_constraint_generator_comparison.cpp
+++ b/src/solvers/refinement/string_constraint_generator_comparison.cpp
@@ -43,7 +43,8 @@ exprt string_constraint_generatort::add_axioms_for_equals(
   lemmas.push_back(a1);
 
   symbol_exprt qvar=fresh_univ_index("QA_equal", index_type);
-  string_constraintt a2(qvar, s1.length(), eq, equal_exprt(s1[qvar], s2[qvar]));
+  string_constraintt a2(
+    qvar, s1.length(), implies_exprt(eq, equal_exprt(s1[qvar], s2[qvar])));
   constraints.push_back(a2);
 
   symbol_exprt witness=fresh_exist_index("witness_unequal", index_type);
@@ -130,7 +131,7 @@ exprt string_constraint_generatort::add_axioms_for_equals_ignore_case(
     fresh_univ_index("QA_equal_ignore_case", index_type);
   const exprt constr2 =
     character_equals_ignore_case(s1[qvar], s2[qvar], char_a, char_A, char_Z);
-  const string_constraintt a2(qvar, s1.length(), eq, constr2);
+  const string_constraintt a2(qvar, s1.length(), implies_exprt(eq, constr2));
   constraints.push_back(a2);
 
   const symbol_exprt witness =
@@ -224,7 +225,7 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
 
   const symbol_exprt i = fresh_univ_index("QA_compare_to", index_type);
   const string_constraintt a2(
-    i, s1.length(), res_null, equal_exprt(s1[i], s2[i]));
+    i, s1.length(), implies_exprt(res_null, equal_exprt(s1[i], s2[i])));
   constraints.push_back(a2);
 
   const symbol_exprt x = fresh_exist_index("index_compare_to", index_type);
@@ -255,7 +256,7 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
 
   const symbol_exprt i2 = fresh_univ_index("QA_compare_to", index_type);
   const string_constraintt a4(
-    i2, x, not_exprt(res_null), equal_exprt(s1[i2], s2[i2]));
+    i2, x, implies_exprt(not_exprt(res_null), equal_exprt(s1[i2], s2[i2])));
   constraints.push_back(a4);
 
   return res;
diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp
index 77086d849f3..e2336e598a9 100644
--- a/src/solvers/refinement/string_constraint_generator_indexof.cpp
+++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp
@@ -65,7 +65,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
 
   symbol_exprt n=fresh_univ_index("QA_index_of", index_type);
   string_constraintt a4(
-    n, lower_bound, index, contains, not_exprt(equal_exprt(str[n], c)));
+    n, lower_bound, index, implies_exprt(contains, notequal_exprt(str[n], c)));
   constraints.push_back(a4);
 
   symbol_exprt m=fresh_univ_index("QA_index_of", index_type);
@@ -73,8 +73,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
     m,
     lower_bound,
     str.length(),
-    not_exprt(contains),
-    not_exprt(equal_exprt(str[m], c)));
+    implies_exprt(not_exprt(contains), not_exprt(equal_exprt(str[m], c))));
   constraints.push_back(a5);
 
   return index;
@@ -130,8 +129,8 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
   string_constraintt a3(
     qvar,
     needle.length(),
-    contains,
-    equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar]));
+    implies_exprt(
+      contains, equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar])));
   constraints.push_back(a3);
 
   // string_not contains_constraintt are formulas of the form:
@@ -221,7 +220,8 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
 
   symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type);
   equal_exprt constr3(haystack[plus_exprt(qvar, offset)], needle[qvar]);
-  string_constraintt a3(qvar, needle.length(), contains, constr3);
+  const string_constraintt a3(
+    qvar, needle.length(), implies_exprt(contains, constr3));
   constraints.push_back(a3);
 
   // end_index is min(from_index, |str| - |substring|)
@@ -364,13 +364,14 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
     n,
     plus_exprt(index, index1),
     end_index,
-    contains,
-    notequal_exprt(str[n], c));
+    implies_exprt(contains, notequal_exprt(str[n], c)));
   constraints.push_back(a4);
 
   const symbol_exprt m = fresh_univ_index("QA_last_index_of2", index_type);
   const string_constraintt a5(
-    m, end_index, not_exprt(contains), notequal_exprt(str[m], c));
+    m,
+    end_index,
+    implies_exprt(not_exprt(contains), notequal_exprt(str[m], c)));
   constraints.push_back(a5);
 
   return index;
diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp
index 286ee7fa095..a739aa18efe 100644
--- a/src/solvers/refinement/string_constraint_generator_main.cpp
+++ b/src/solvers/refinement/string_constraint_generator_main.cpp
@@ -369,7 +369,7 @@ void string_constraint_generatort::add_constraint_on_characters(
   const and_exprt char_in_set(
     binary_relation_exprt(chr, ID_ge, from_integer(low_char, chr.type())),
     binary_relation_exprt(chr, ID_le, from_integer(high_char, chr.type())));
-  const string_constraintt sc(qvar, start, end, true_exprt(), char_in_set);
+  const string_constraintt sc(qvar, start, end, char_in_set);
   constraints.push_back(sc);
 }
 
@@ -662,3 +662,8 @@ exprt string_constraint_generatort::add_axioms_for_char_at(
   lemmas.push_back(equal_exprt(char_sym, str[f.arguments()[1]]));
   return char_sym;
 }
+
+exprt minimum(const exprt &a, const exprt &b)
+{
+  return if_exprt(binary_relation_exprt(a, ID_le, b), a, b);
+}
diff --git a/src/solvers/refinement/string_constraint_generator_testing.cpp b/src/solvers/refinement/string_constraint_generator_testing.cpp
index b8dbfaa95ec..09948073b49 100644
--- a/src/solvers/refinement/string_constraint_generator_testing.cpp
+++ b/src/solvers/refinement/string_constraint_generator_testing.cpp
@@ -46,8 +46,8 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix(
   string_constraintt a2(
     qvar,
     prefix.length(),
-    isprefix,
-    equal_exprt(str[plus_exprt(qvar, offset)], prefix[qvar]));
+    implies_exprt(
+      isprefix, equal_exprt(str[plus_exprt(qvar, offset)], prefix[qvar])));
   constraints.push_back(a2);
 
   symbol_exprt witness=fresh_exist_index("witness_not_isprefix", index_type);
@@ -153,7 +153,9 @@ exprt string_constraint_generatort::add_axioms_for_is_suffix(
   symbol_exprt qvar=fresh_univ_index("QA_suffix", index_type);
   const plus_exprt qvar_shifted(qvar, minus_exprt(s1.length(), s0.length()));
   string_constraintt a2(
-    qvar, s0.length(), issuffix, equal_exprt(s0[qvar], s1[qvar_shifted]));
+    qvar,
+    s0.length(),
+    implies_exprt(issuffix, equal_exprt(s0[qvar], s1[qvar_shifted])));
   constraints.push_back(a2);
 
   symbol_exprt witness=fresh_exist_index("witness_not_suffix", index_type);
@@ -221,7 +223,9 @@ exprt string_constraint_generatort::add_axioms_for_contains(
   symbol_exprt qvar=fresh_univ_index("QA_contains", index_type);
   const plus_exprt qvar_shifted(qvar, startpos);
   string_constraintt a4(
-    qvar, s1.length(), contains, equal_exprt(s1[qvar], s0[qvar_shifted]));
+    qvar,
+    s1.length(),
+    implies_exprt(contains, equal_exprt(s1[qvar], s0[qvar_shifted])));
   constraints.push_back(a4);
 
   string_not_contains_constraintt a5(
diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp
index 1271c11184a..e4df62603fd 100644
--- a/src/solvers/refinement/string_constraint_generator_transformation.cpp
+++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp
@@ -45,24 +45,21 @@ exprt string_constraint_generatort::add_axioms_for_set_length(
 
   // We add axioms:
   // a1 : |res|=k
-  // a2 : forall i<|res|. i < |s1|  ==> res[i] = s1[i]
-  // a3 : forall i<|res|. i >= |s1| ==> res[i] = 0
+  // a2 : forall i< min(|s1|, k) .res[i] = s1[i]
+  // a3 : forall |s1| <= i < |res|. res[i] = 0
 
   lemmas.push_back(res.axiom_for_has_length(k));
 
-  symbol_exprt idx = fresh_univ_index("QA_index_set_length", index_type);
-  string_constraintt a2(
-    idx,
-    res.length(),
-    s1.axiom_for_length_gt(idx),
-    equal_exprt(s1[idx], res[idx]));
+  const symbol_exprt idx = fresh_univ_index("QA_index_set_length", index_type);
+  const string_constraintt a2(
+    idx, minimum(s1.length(), k), equal_exprt(s1[idx], res[idx]));
   constraints.push_back(a2);
 
   symbol_exprt idx2 = fresh_univ_index("QA_index_set_length2", index_type);
   string_constraintt a3(
     idx2,
+    s1.length(),
     res.length(),
-    s1.axiom_for_length_le(idx2),
     equal_exprt(res[idx2], constant_char(0, char_type)));
   constraints.push_back(a3);
 
@@ -395,8 +392,8 @@ exprt string_constraint_generatort::add_axioms_for_to_upper_case(
 /// These axioms are:
 ///   1. \f$ |{\tt res}| = |{\tt str}|\f$
 ///   2. \f$ {\tt res}[{\tt pos}]={\tt char}\f$
-///   3. \f$ \forall i<|{\tt res}|.\ i \ne {\tt pos}
-///          \Rightarrow {\tt res}[i] = {\tt str}[i]\f$
+///   3. \f$ \forall i < min(|{\tt res}|, pos). {\tt res}[i] = {\tt str}[i]\f$
+///   4. \f$ \forall pos+1 <= i < |{\tt res}|.\ {\tt res}[i] = {\tt str}[i]\f$
 /// \param f: function application with arguments integer `|res|`, character
 ///           pointer `&res[0]`, refined_string `str`, integer `pos`,
 ///           and character `char`
@@ -413,14 +410,22 @@ exprt string_constraint_generatort::add_axioms_for_char_set(
   const exprt &character = f.arguments()[4];
 
   const binary_relation_exprt out_of_bounds(position, ID_ge, str.length());
-  lemmas.push_back(equal_exprt(res.length(), str.length()));
-  lemmas.push_back(equal_exprt(res[position], character));
+  const equal_exprt a1(res.length(), str.length());
+  lemmas.push_back(a1);
+  const equal_exprt a2(res[position], character);
+  lemmas.push_back(a2);
+
   const symbol_exprt q = fresh_univ_index("QA_char_set", position.type());
-  equal_exprt a3_body(res[q], str[q]);
-  notequal_exprt a3_guard(q, position);
-  constraints.push_back(
-    string_constraintt(
-      q, from_integer(0, q.type()), res.length(), a3_guard, a3_body));
+  const equal_exprt a3_body(res[q], str[q]);
+  const string_constraintt a3(q, minimum(res.length(), position), a3_body);
+  constraints.push_back(a3);
+
+  const symbol_exprt q2 = fresh_univ_index("QA_char_set2", position.type());
+  const plus_exprt lower_bound(position, from_integer(1, position.type()));
+  const equal_exprt a4_body(res[q2], str[q2]);
+  const string_constraintt a4(q2, lower_bound, res.length(), a4_body);
+  constraints.push_back(a4);
+
   return if_exprt(
     out_of_bounds, from_integer(1, f.type()), from_integer(0, f.type()));
 }
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 202c2b4f8b8..53da9d1cbb6 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -772,17 +772,12 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       config_.use_counter_example,
       supert::config_.ui,
       symbol_resolve);
-    if(!satisfied)
-    {
-      for(const auto &counter : counter_examples)
-        add_lemma(counter);
-      debug() << "check_SAT: got SAT but the model is not correct" << eom;
-    }
-    else
+    if(satisfied)
     {
       debug() << "check_SAT: the model is correct" << eom;
       return resultt::D_SATISFIABLE;
     }
+    debug() << "check_SAT: got SAT but the model is not correct" << eom;
   }
   else
   {
@@ -821,19 +816,15 @@ decision_proceduret::resultt string_refinementt::dec_solve()
         config_.use_counter_example,
         supert::config_.ui,
         symbol_resolve);
-      if(!satisfied)
-      {
-        for(const auto &counter : counter_examples)
-          add_lemma(counter);
-        debug() << "check_SAT: got SAT but the model is not correct" << eom;
-      }
-      else
+      if(satisfied)
       {
         debug() << "check_SAT: the model is correct" << eom;
         return resultt::D_SATISFIABLE;
       }
 
-      debug() <<  "refining..." << eom;
+      debug() << "check_SAT: got SAT but the model is not correct, refining..."
+              << eom;
+
       // Since the model is not correct although we got SAT, we need to refine
       // the property we are checking by adding more indices to the index set,
       // and instantiating universal formulas with this indices.
@@ -852,7 +843,12 @@ decision_proceduret::resultt string_refinementt::dec_solve()
           return resultt::D_ERROR;
         }
         else
-          debug() << "dec_solve: current index set is empty" << eom;
+        {
+          debug() << "dec_solve: current index set is empty, "
+                  << "adding counter examples" << eom;
+          for(const auto &counter : counter_examples)
+            add_lemma(counter);
+        }
       }
       current_constraints.clear();
       for(const auto &instance :
@@ -1553,10 +1549,12 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
     const exprt &bound_inf=axiom.lower_bound();
     const exprt &bound_sup=axiom.upper_bound();
     const exprt &prem=axiom.premise();
+    INVARIANT(
+      prem == true_exprt(), "string constraint premises are not supported");
     const exprt &body=axiom.body();
 
     const string_constraintt axiom_in_model(
-      univ_var, get(bound_inf), get(bound_sup), get(prem), get(body));
+      univ_var, get(bound_inf), get(bound_sup), get(body));
 
     exprt negaxiom=negation_of_constraint(axiom_in_model);
     negaxiom = simplify_expr(negaxiom, ns);
@@ -1643,8 +1641,6 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
 
     if(use_counter_example)
     {
-      stream << "Adding counter-examples: " << eom;
-
       std::vector<exprt> lemmas;
 
       for(const auto &v : violated)
@@ -1660,8 +1656,6 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
           binary_relation_exprt(from_integer(0, val.type()), ID_le, val));
         replace_expr(axiom.univ_var(), val, bounds);
         const implies_exprt counter(bounds, instance);
-
-        stream << "  -  " << format(counter) << eom;
         lemmas.push_back(counter);
       }
 
@@ -1678,8 +1672,6 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
         indices.insert(std::pair<exprt, exprt>(comp_val, func_val));
         const exprt counter=::instantiate_not_contains(
           axiom, indices, generator)[0];
-
-        stream << "    -  " << format(counter) << eom;
         lemmas.push_back(counter);
       }
       return { false, lemmas };
@@ -1973,53 +1965,68 @@ static void add_to_index_set(
   }
 }
 
+/// Given an array access of the form \a s[i] assumed to be part of a formula
+/// \f$ \forall q < u. charconstraint \f$, initialize the index set of \a s
+/// so that:
+///   - \f$ i[q -> u - 1] \f$ appears in the index set of \a s if \a s is a
+///     symbol
+///   - if \a s is an array expression, all index from \a 0 to
+///     \f$ s.length - 1 \f$ are in the index set
+///   - if \a s is an if expression we apply this procedure to the true and
+///     false cases
+/// \param index_set: the index_set to initialize
+/// \param ns: namespace, used for simplifying indexes
+/// \param qvar: the quantified variable \a q
+/// \param upper_bound: bound \a u on the quantified variable
+/// \param s: expression representing a string
+/// \param i: expression representing the index at which \a s is accessed
+static void initial_index_set(
+  index_set_pairt &index_set,
+  const namespacet &ns,
+  const exprt &qvar,
+  const exprt &upper_bound,
+  const exprt &s,
+  const exprt &i)
+{
+  PRECONDITION(s.id() == ID_symbol || s.id() == ID_array || s.id() == ID_if);
+  if(s.id() == ID_array)
+  {
+    for(std::size_t j = 0; j < s.operands().size(); ++j)
+      add_to_index_set(index_set, ns, s, from_integer(j, i.type()));
+    return;
+  }
+  if(auto ite = expr_try_dynamic_cast<if_exprt>(s))
+  {
+    initial_index_set(index_set, ns, qvar, upper_bound, ite->true_case(), i);
+    initial_index_set(index_set, ns, qvar, upper_bound, ite->false_case(), i);
+    return;
+  }
+  const minus_exprt u_minus_1(upper_bound, from_integer(1, upper_bound.type()));
+  exprt i_copy = i;
+  replace_expr(qvar, u_minus_1, i_copy);
+  add_to_index_set(index_set, ns, s, i_copy);
+}
+
 static void initial_index_set(
   index_set_pairt &index_set,
   const namespacet &ns,
   const string_constraintt &axiom)
 {
   const symbol_exprt &qvar=axiom.univ_var();
-  std::list<exprt> to_process;
-  to_process.push_back(axiom.body());
-
-  while(!to_process.empty())
+  const auto &bound = axiom.upper_bound();
+  auto it = axiom.body().depth_begin();
+  const auto end = axiom.body().depth_end();
+  while(it != end)
   {
-    const exprt cur = to_process.back();
-    to_process.pop_back();
-    if(cur.id() == ID_index && is_char_type(cur.type()))
+    if(it->id() == ID_index && is_char_type(it->type()))
     {
-      const index_exprt &index_expr = to_index_expr(cur);
-      const exprt &s = index_expr.array();
-      const exprt &i = index_expr.index();
-
-      if(s.id() == ID_array)
-      {
-        for(std::size_t j = 0; j < s.operands().size(); ++j)
-          add_to_index_set(index_set, ns, s, from_integer(j, i.type()));
-      }
-      else
-      {
-        const bool has_quant_var = find_qvar(i, qvar);
-
-        // if cur is of the form s[i] and no quantified variable appears in i
-        if(!has_quant_var)
-        {
-          add_to_index_set(index_set, ns, s, i);
-        }
-        else
-        {
-          // otherwise we add k-1
-          exprt copy(i);
-          const minus_exprt kminus1(
-            axiom.upper_bound(), from_integer(1, axiom.upper_bound().type()));
-          replace_expr(qvar, kminus1, copy);
-          add_to_index_set(index_set, ns, s, copy);
-        }
-      }
+      const auto &index_expr = to_index_expr(*it);
+      const auto &s = index_expr.array();
+      initial_index_set(index_set, ns, qvar, bound, s, index_expr.index());
+      it.next_sibling_or_parent();
     }
     else
-      forall_operands(it, cur)
-        to_process.push_back(*it);
+      ++it;
   }
 }
 
@@ -2090,26 +2097,47 @@ static void update_index_set(
 /// Finds an index on `str` used in `expr` that contains `qvar`, for instance
 /// with arguments ``(str[k]=='a')``, `str`, and `k`, the function should
 /// return `k`.
+/// If two different such indexes exist, an invariant will fail.
 /// \param [in] expr: the expression to search
 /// \param [in] str: the string which must be indexed
 /// \param [in] qvar: the universal variable that must be in the index
-/// \return an index expression in `expr` on `str` containing `qvar`
-static exprt find_index(
-  const exprt &expr, const exprt &str, const symbol_exprt &qvar)
+/// \return an index expression in `expr` on `str` containing `qvar`. Returns
+///   an empty optional when `expr` does not contain `str`.
+static optionalt<exprt>
+find_index(const exprt &expr, const exprt &str, const symbol_exprt &qvar)
 {
-  const auto it=std::find_if(
-    expr.depth_begin(),
-    expr.depth_end(),
-    [&] (const exprt &e) -> bool
+  auto index_str_containing_qvar = [&](const exprt &e) { // NOLINT
+    if(auto index_expr = expr_try_dynamic_cast<index_exprt>(e))
     {
-      return e.id()==ID_index
-             && to_index_expr(e).array()==str
-             && find_qvar(to_index_expr(e).index(), qvar);
-    });
+      const auto &arr = index_expr->array();
+      const auto str_it = std::find(arr.depth_begin(), arr.depth_end(), str);
+      return str_it != arr.depth_end() && find_qvar(index_expr->index(), qvar);
+    }
+    return false;
+  };
+
+  auto it = std::find_if(
+    expr.depth_begin(), expr.depth_end(), index_str_containing_qvar);
+  if(it == expr.depth_end())
+    return {};
+  const exprt &index = to_index_expr(*it).index();
+
+  // Check that there are no two such indexes
+  it.next_sibling_or_parent();
+  while(it != expr.depth_end())
+  {
+    if(index_str_containing_qvar(*it))
+    {
+      INVARIANT(
+        to_index_expr(*it).index() == index,
+        "string should always be indexed by same value in a given formula");
+      it.next_sibling_or_parent();
+    }
+    else
+      ++it;
+  }
 
-  return it==expr.depth_end()
-         ?nil_exprt()
-         :to_index_expr(*it).index();
+  return index;
 }
 
 /// Instantiates a string constraint by substituting the quantifiers.
@@ -2130,19 +2158,19 @@ static exprt instantiate(
   const exprt &str,
   const exprt &val)
 {
-  exprt idx=find_index(axiom.body(), str, axiom.univ_var());
-  if(idx.is_nil())
+  const optionalt<exprt> idx = find_index(axiom.body(), str, axiom.univ_var());
+  if(!idx.has_value())
     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