fixup! Refactor negation of not contains constraints

Author: romainbrenguier

src/solvers/refinement/string_refinement.cpp

@@ -1204,7 +1204,7 @@ exprt substitute_array_access(
 ///   their valuation in the current model.
 /// \param constraint: the not_contains constraint to add the negation of
 /// \param univ_var: the universal variable for the negation of the axiom
-/// \param get: valuation function
+/// \param get: valuation function, the result should have been simplified
 /// \return: the negation of the axiom under the current evaluation
 static exprt negation_of_not_contains_constraint(
   const string_not_contains_constraintt &constraint,
@@ -1396,7 +1396,8 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
     const symbol_exprt univ_var = generator.fresh_univ_index(
       "not_contains_univ_var", nc_axiom.s0().length().type());
     const exprt negated_axiom = negation_of_not_contains_constraint(
-      nc_axiom, univ_var, [&](const exprt &expr) { return get(expr); });
+      nc_axiom, univ_var, [&](const exprt &expr) {
+        return simplify_expr(get(expr), ns); });
 
     stream << indent << i << ".\n";
     debug_check_axioms_step(