From 497d2960a0df54d6980993b90fd74aa32032991d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 22 Jun 2018 17:03:47 +0100
Subject: [PATCH] Fix invariant: value must be strictly positive

A value of zero would result in an invalid memory access later on.
---
 src/solvers/refinement/string_constraint_generator_format.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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<std::size_t>(fs.index)<=args.size(),
             "number of format must match specifiers");