Skip to content

Commit f50db05

Browse files
committed
Fix invariant: value must be strictly positive
A value of zero would result in an invalid memory access later on.
1 parent 90c56b3 commit f50db05

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/solvers/refinement/string_constraint_generator_format.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -374,7 +374,7 @@ exprt string_constraint_generatort::add_axioms_for_format(
374374
}
375375
else
376376
{
377-
INVARIANT(fs.index>=0, "index in format should be positive");
377+
INVARIANT(fs.index > 0, "index in format should be positive");
378378
INVARIANT(
379379
static_cast<std::size_t>(fs.index)<=args.size(),
380380
"number of format must match specifiers");

0 commit comments

Comments
 (0)