constannot.c: (in function foo2)
constannot.c:11:3: Possible out-of-bounds store: str[20]
    Unable to resolve constraint:
    requires maxSet(str @ constannot.c:11:3) >= 20
     needed to satisfy precondition:
    requires maxSet(str @ constannot.c:11:3) >= 20
constannot.c: (in function foo3)
constannot.c:20:3: Likely out-of-bounds store: foo(buf)
    Unable to resolve constraint:
    requires <const int=20> <= 19
     needed to satisfy precondition:
    requires maxSet(buf @ constannot.c:20:8) >= <const int=20>
     derived from foo precondition: requires maxSet(<parameter 1>) >= <const
    int=20>

Finished checking --- 2 code warnings, as expected