// time cbmc --trace --function check -DLEN=15 fname.c

#include <assert.h>
#include <stdio.h>
#include <string.h>

unsigned search_cat_brute (char *s, unsigned len)
{
        unsigned read_ops=0;
        if (len<3)
                return len; // not found
        for (unsigned i=0; i<len-2; i++)
        {
                read_ops++;
                if (s[i]!='c')
                        continue;
                read_ops++;
                if (s[i+1]!='a')
                        continue;
                read_ops++;
                if (s[i+2]!='t')
                        continue;
                printf ("%s read_ops=%d\n", __FUNCTION__, read_ops);
                return i;
        };
        printf ("%s read_ops=%d\n", __FUNCTION__, read_ops);
        return len; // not found
};

unsigned search_cat_BM_v1 (char *s, unsigned len)
{
        if (len<3)
                return len; // not found
        unsigned read_ops=0;
        unsigned skip; // default skip
        for (unsigned i=0; i<len-2; )
        {
                skip=1;
                read_ops++;
                char char3=s[i+2]; // read operation
                if (char3=='t')
                {
                        read_ops++;
                        char char2=s[i+1]; // read operation
                        if (char2=='a')
                        {
                                read_ops++;
                                char char1=s[i]; // read operation
                                if (char1=='c')
                                {
                                        printf ("%s read_ops=%d\n", __FUNCTION__, read_ops);
                                        return i; // found
                                }
                                else
                                {
                                        // 1st character isn't 'c'
                                        if ((char1!='c') && (char1!='a') && (char1!='t'))
                                                skip=3;
                                }
                        }
                        else
                        {
                                // 2nd character isn't 'a'
                                if ((char2!='c') && (char2!='a') && (char2!='t'))
                                        skip=3;
                        }
                }
                else
                {
                        // 3rd character isn't 't'
                        if ((char3!='c') && (char3!='a') && (char3!='t'))
                                skip=3;
                }
                i=i+skip;
        }
        printf ("%s read_ops=%d\n", __FUNCTION__, read_ops);
        return len; // not found
};

#ifdef CBMC
void check()
{
        unsigned len=LEN;
        char s[len];
        __CPROVER_assert (search_cat_brute(s, len)==search_cat_BM_v1(s, len), "assert");
};
#endif

#ifndef CBMC
void test(char *s)
{
        printf ("** %s\n", s);
        size_t len=strlen(s);
        unsigned a1=search_cat_brute(s, len);
        unsigned a2=search_cat_BM_v1(s, len);
        assert (a1==a2);
};

int main()
{
        test("cat");
        test("caz");
        test(" cat");
        test("cat ");
        test("caxc");
        test("ccxc");
        test("cxtca");
        test("tat");
        test("cacat");
        test("cac cat");
        test("cac cac cat");
        test("horse turtle cat");
        test("horse cat turtle");
        test("cat turtle horse");
}
#endif