Forgotten premise in add_axioms_from_int

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator_valueof.cpp

@@ -209,9 +209,9 @@ string_exprt string_constraint_generatort::add_axioms_from_bool(
 
 /// add axioms to say the string corresponds to the result of String.valueOf(I)
 /// or String.valueOf(J) java functions applied on the integer expression
-/// \par parameters: a signed integer expression, and a maximal size for the
-///   string
-/// representation
+/// \param i: a signed integer expression
+/// \param max_size: a maximal size for the string representation
+/// \param ref_type: type for refined strings
 /// \return a string expression
 string_exprt string_constraint_generatort::add_axioms_from_int(
   const exprt &i, size_t max_size, const refined_string_typet &ref_type)
@@ -299,10 +299,10 @@ string_exprt string_constraint_generatort::add_axioms_from_int(
       sum=new_sum;
     }
 
+    equal_exprt premise=res.axiom_for_has_length(size);
     exprt a5=conjunction(digit_constraints);
-    axioms.push_back(a5);
+    axioms.push_back(implies_exprt(premise, a5));
 
-    equal_exprt premise=res.axiom_for_has_length(size);
     implies_exprt a6(
       and_exprt(premise, starts_with_digit), equal_exprt(i, sum));
     axioms.push_back(a6);