diff --git a/src/solvers/refinement/string_constraint_generator_format.cpp b/src/solvers/refinement/string_constraint_generator_format.cpp index 847d7baec4d..1b34a98cdf4 100644 --- a/src/solvers/refinement/string_constraint_generator_format.cpp +++ b/src/solvers/refinement/string_constraint_generator_format.cpp @@ -374,7 +374,7 @@ exprt string_constraint_generatort::add_axioms_for_format( } else { - INVARIANT(fs.index>=0, "index in format should be positive"); + INVARIANT(fs.index > 0, "index in format should be positive"); INVARIANT( static_cast(fs.index)<=args.size(), "number of format must match specifiers");