#include <stdio.h>
#include <stdbool.h>

unsigned search_ok_1 (char *s, unsigned len)
{
        if (len<2)
                return len;       // not found
        for (unsigned i=0; i<len-1; i++)
        {
                if (s[i]=='o' && s[i+1]=='k')
                        return i; // found
        };
        return len;               // not found
};

unsigned search_ok_2 (char *s, unsigned len)
{
        if (len<2)
                return len;           // not found
        bool seen_o=false;
        for (unsigned i=0; i<len; i++)
        {
                char ch=s[i];         // this is single read operation
                if (ch=='o')
                        seen_o=true;
                else if (seen_o && ch=='k')
                        return i-1;   // found
                else
                        seen_o=false; // reset
        };
        return len; // not found
};

#if 1
void check()
{
        unsigned len=LEN;
        char s[len];
        __CPROVER_assert (search_ok_1(s, len)==search_ok_2(s, len), "assert");
};
#endif