CONTROL AUTOMATON CounterexampleAutomaton

INITIAL STATE ARG1;

STATE USEFIRST ARG1 :
    MATCH "" -> GOTO ARG35_1_1;
STATE USEFIRST ARG35_0_1 :
    MATCH "" -> GOTO ARG35_1_1;
STATE USEFIRST ARG35_1_1 :
    MATCH "void __VERIFIER_assert(int cond)" -> GOTO ARG35_2_1;
STATE USEFIRST ARG35_2_1 :
    MATCH "unsigned int __VERIFIER_nondet_uint();" -> GOTO ARG35_3_1;
STATE USEFIRST ARG35_3_1 :
    MATCH "int main()" -> GOTO ARG35_4_1;
STATE USEFIRST ARG35_4_1 :
    MATCH "" -> GOTO ARG35_5_1;
STATE USEFIRST ARG35_5_1 :
    MATCH "unsigned int SIZE=__VERIFIER_nondet_uint();" -> GOTO ARG35_6_1;
STATE USEFIRST ARG35_6_1 :
    MATCH "unsigned int SIZE=__VERIFIER_nondet_uint();" -> GOTO ARG35_7_1;
STATE USEFIRST ARG35_7_1 :
    MATCH "int i, j, k, key;" -> GOTO ARG35_8_1;
STATE USEFIRST ARG35_8_1 :
    MATCH "int i, j, k, key;" -> GOTO ARG35_9_1;
STATE USEFIRST ARG35_9_1 :
    MATCH "int i, j, k, key;" -> GOTO ARG35_10_1;
STATE USEFIRST ARG35_10_1 :
    MATCH "int i, j, k, key;" -> GOTO ARG35_11_1;
STATE USEFIRST ARG35_11_1 :
    MATCH "int v[SIZE];" -> GOTO ARG35_12_1;
STATE USEFIRST ARG35_12_1 :
    MATCH "" -> GOTO ARG35_13_1;
STATE USEFIRST ARG35_13_1 :
    MATCH "j=1" -> GOTO ARG35;
    TRUE -> STOP;

STATE USEFIRST ARG35 :
    MATCH "[j < SIZE]" -> GOTO ARG36;
    TRUE -> STOP;

STATE USEFIRST ARG36 :
    MATCH "key = v[j];" -> GOTO ARG52_1_2;
STATE USEFIRST ARG52_0_2 :
    MATCH "key = v[j];" -> GOTO ARG52_1_2;
STATE USEFIRST ARG52_1_2 :
    MATCH "i = j - 1;" -> GOTO ARG52_2_2;
STATE USEFIRST ARG52_2_2 :
    MATCH "" -> GOTO ARG52;
    TRUE -> STOP;

STATE USEFIRST ARG52 :
    MATCH "[i >= 0]" -> GOTO ARG53;
    MATCH "[!(i >= 0)]" -> GOTO ARG57;
    TRUE -> STOP;

STATE USEFIRST ARG53 :
    MATCH "[!((v[i]) > key)]" -> GOTO ARG57;
    TRUE -> STOP;

STATE USEFIRST ARG57 :
    MATCH "v[i+1] = key;" -> GOTO ARG59_1_3;
STATE USEFIRST ARG59_0_3 :
    MATCH "v[i+1] = key;" -> GOTO ARG59_1_3;
STATE USEFIRST ARG59_1_3 :
    MATCH "" -> GOTO ARG59_2_3;
STATE USEFIRST ARG59_2_3 :
    MATCH "j++" -> GOTO ARG59;
    TRUE -> STOP;

STATE USEFIRST ARG59 :
    MATCH "[!(j < SIZE)]" -> GOTO ARG61;
    TRUE -> STOP;

STATE USEFIRST ARG61 :
    MATCH "" -> GOTO ARG63_1_4;
STATE USEFIRST ARG63_0_4 :
    MATCH "" -> GOTO ARG63_1_4;
STATE USEFIRST ARG63_1_4 :
    MATCH "k=1" -> GOTO ARG63;
    TRUE -> STOP;

STATE USEFIRST ARG63 :
    MATCH "[k < SIZE]" -> GOTO ARG64;
    TRUE -> STOP;

STATE USEFIRST ARG64 :
    MATCH "__VERIFIER_assert(v[k-1]<=v[k]);" -> GOTO ARG67;
    TRUE -> STOP;

STATE USEFIRST ARG67 :
    MATCH "" -> GOTO ARG68;
    TRUE -> STOP;

STATE USEFIRST ARG68 :
    MATCH "[cond == 0]" -> GOTO ARG69;
    TRUE -> STOP;

STATE USEFIRST ARG69 :
    MATCH "ERROR: goto ERROR;" -> ERROR;
    TRUE -> STOP;

STATE USEFIRST ARG73 :
    TRUE -> STOP;

END AUTOMATON