:- module( _, [search/2], [assertions , regtypes , basicmodes , nativeprops] ).

search([[ref(loc(1)),num(int(_1))],[array(A,_2)]],[num(int(0))]) :-
        0>=A .
search([[ref(loc(1)),num(int(A))],[array(B,[num(int(D))|C])]],[E]) :-
        0<B,
        0<B,
        D\=A,
        execute_notrace_1(B,C,D,A,_1,_2,_3,_4,_5,E,_6) .
search([[ref(loc(1)),num(int(A))],[array(B,[num(int(A))|C])]],[D]) :-
        0<B,
        0<B,
        execute_notrace_3(B,C,A,A,1,0,_1,_2,_3,_4,_5,D,_6) .
search([[ref(loc(1)),num(int(_1))],[array(A,_2)]],[refE(loc(2))]) :-
        0<A,
        0>=A .
search([[null,num(int(_1))],[]],[refE(loc(1))]).

execute_notrace_1(A,B,C,_1,[array(A,[num(int(C))|B])],_2,_3,_4,_5,num(int(1)),[]) :-
        1>=A .
execute_notrace_1(A,[num(int(D))|C],B,E,F,G,H,I,J,K,L) :-
        1<A,
        1<A,
        D\=E,
        execute_notrace_2(A,[num(int(D))|C],B,E,2,F,G,H,I,J,K,L) .
execute_notrace_1(A,[num(int(D))|C],B,D,E,F,G,H,I,J,K) :-
        1<A,
        1<A,
        execute_notrace_3(A,[num(int(D))|C],B,D,1,1,E,F,G,H,I,J,K) .
execute_notrace_1(A,B,C,_1,[array(A,[num(int(C))|B]),[]],_2,_3,_4,_5,refE(loc(2)),[]) :-
        1<A,
        1>=A .

execute_notrace_2(A,B,C,_1,D,[array(A,[num(int(C))|B])],_2,_3,_4,_5,num(int(D)),[]) :-
        D>=A .
execute_notrace_2(A,B,C,D,E,F,G,H,I,J,K,L) :-
        E<A,
        0=<E,
        E<A,
        M is E+1,
        mynth(M,[num(int(C))|B],num(int(N))),
        N\=D,
        O is E+1,
        execute_notrace_2(A,B,C,D,O,F,G,H,I,J,K,L) .
execute_notrace_2(A,B,C,D,E,F,G,H,I,J,K,L) :-
        E<A,
        0=<E,
        E<A,
        M is E+1,
        mynth(M,[num(int(C))|B],num(int(D))),
        execute_notrace_3(A,B,C,D,1,E,F,G,H,I,J,K,L) .
execute_notrace_2(A,B,C,_1,D,[array(A,[num(int(C))|B]),[]],_2,_3,_4,_5,refE(loc(2)),[]) :-
        D<A,
        D<0 .
execute_notrace_2(A,B,C,_1,D,[array(A,[num(int(C))|B]),[]],_2,_3,_4,_5,refE(loc(2)),[]) :-
        D<A,
        D>=A .

execute_notrace_3(A,B,C,_1,_2,D,[array(A,[num(int(C))|B])],_3,_4,_5,_6,num(int(D)),[]) :-
        D>=A .
execute_notrace_3(A,B,C,_1,D,E,[array(A,[num(int(C))|B])],_2,_3,_4,_5,num(int(E)),[]) :-
        E<A,
        D\=0 .
execute_notrace_3(A,B,C,D,0,E,F,G,H,I,J,K,L) :-
        E<A,
        0=<E,
        E<A,
        M is E+1,
        mynth(M,[num(int(C))|B],num(int(N))),
        N\=D,
        O is E+1,
        execute_notrace(program([class(className(packageName(''),shortClassName('LinearSearch')),final(false),public(true),abstract(false),className(packageName('java/lang/'),shortClassName('Object')),[],[],[method(methodSignature(methodName(className(packageName(''),shortClassName('LinearSearch')),shortMethodName('<init>')),[],none),bytecodeMethod(1,1,0,methodId('0',0),[]),final(false),static(false),public),method(methodSignature(methodName(className(packageName(''),shortClassName('LinearSearch')),shortMethodName(search)),[refType(arrayType(primitiveType(int))),primitiveType(int)],primitiveType(int)),bytecodeMethod(5,2,0,methodId('0',1),[]),final(false),static(true),public)]),class(className(packageName('java/lang/'),shortClassName('Object')),final(false),public(false),abstract(false),none,[],[],[method(methodSignature(methodName(className(packageName('java/lang/'),shortClassName('Object')),shortMethodName('<init>')),[],none),bytecodeMethod(1,1,0,methodId('Object',0),[]),final(false),static(false),public)]),class(className(packageName('java/lang/'),shortClassName('String')),final(false),public(false),abstract(false),className(packageName('java/lang/'),shortClassName('Object')),[],[],[method(methodSignature(methodName(className(packageName('java/lang/'),shortClassName('String')),shortMethodName('<init>')),[],none),bytecodeMethod(1,1,0,methodId('String',0),[]),final(false),static(false),private)]),class(className(packageName('java/lang/'),shortClassName('NullPointerException')),final(false),public(false),abstract(false),className(packageName('java/lang/'),shortClassName('Object')),[],[],[method(methodSignature(methodName(className(packageName('java/lang/'),shortClassName('NullPointerException')),shortMethodName('<init>')),[],none),bytecodeMethod(1,1,0,methodId('NullPointerException',0),[]),final(false),static(false),private)]),class(className(packageName('java/lang/'),shortClassName('ArrayStoreException')),final(false),public(false),abstract(false),className(packageName('java/lang/'),shortClassName('Object')),[],[],[method(methodSignature(methodName(className(packageName('java/lang/'),shortClassName('ArrayStoreException')),shortMethodName('<init>')),[],none),bytecodeMethod(1,1,0,methodId('ArrayStoreException',0),[]),final(false),static(false),private)]),class(className(packageName('java/lang/'),shortClassName('ArrayIndexOutOfBoundsException')),final(false),public(false),abstract(false),className(packageName('java/lang/'),shortClassName('Object')),[],[],[method(methodSignature(methodName(className(packageName('java/lang/'),shortClassName('ArrayIndexOutOfBoundsException')),shortMethodName('<init>')),[],none),bytecodeMethod(1,1,0,methodId('ArrayIndexOutOfBoundsException',0),[]),final(false),static(false),private)]),class(className(packageName('java/lang/'),shortClassName('NegativeArraySizeException')),final(false),public(false),abstract(false),className(packageName('java/lang/'),shortClassName('Object')),[],[],[method(methodSignature(methodName(className(packageName('java/lang/'),shortClassName('NegativeArraySizeException')),shortMethodName('<init>')),[],none),bytecodeMethod(1,1,0,methodId('NegativeArraySizeException',0),[]),final(false),static(false),private)]),class(className(packageName('java/lang/'),shortClassName('ClassCastException')),final(false),public(false),abstract(false),className(packageName('java/lang/'),shortClassName('Object')),[],[],[method(methodSignature(methodName(className(packageName('java/lang/'),shortClassName('ClassCastException')),shortMethodName('<init>')),[],none),bytecodeMethod(1,1,0,methodId('ClassCastException',0),[]),final(false),static(false),private)]),class(className(packageName('java/lang/'),shortClassName('ArithmeticException')),final(false),public(false),abstract(false),className(packageName('java/lang/'),shortClassName('Object')),[],[],[method(methodSignature(methodName(className(packageName('java/lang/'),shortClassName('ArithmeticException')),shortMethodName('<init>')),[],none),bytecodeMethod(1,1,0,methodId('ArithmeticException',0),[]),final(false),static(false),private)])],[]),st(heap(dynamicHeap([array(locationArray(A,primitiveType(int)),[num(int(C))|B])]),staticHeap([])),fr(method(methodSignature(methodName(className(packageName(''),shortClassName('LinearSearch')),shortMethodName(search)),[refType(arrayType(primitiveType(int))),primitiveType(int)],primitiveType(int)),bytecodeMethod(5,2,0,methodId('0',1),[]),final(false),static(true),public),8,[],[ref(loc(1)),num(int(D)),num(int(A)),num(int(0)),num(int(O))]),[]),st(F,fr(H,I,[K|L],J),G)) .
execute_notrace_3(A,B,C,D,0,E,F,G,H,I,J,K,L) :-
        E<A,
        0=<E,
        E<A,
        M is E+1,
        mynth(M,[num(int(C))|B],num(int(D))),
        execute_notrace(program([class(className(packageName(''),shortClassName('LinearSearch')),final(false),public(true),abstract(false),className(packageName('java/lang/'),shortClassName('Object')),[],[],[method(methodSignature(methodName(className(packageName(''),shortClassName('LinearSearch')),shortMethodName('<init>')),[],none),bytecodeMethod(1,1,0,methodId('0',0),[]),final(false),static(false),public),method(methodSignature(methodName(className(packageName(''),shortClassName('LinearSearch')),shortMethodName(search)),[refType(arrayType(primitiveType(int))),primitiveType(int)],primitiveType(int)),bytecodeMethod(5,2,0,methodId('0',1),[]),final(false),static(true),public)]),class(className(packageName('java/lang/'),shortClassName('Object')),final(false),public(false),abstract(false),none,[],[],[method(methodSignature(methodName(className(packageName('java/lang/'),shortClassName('Object')),shortMethodName('<init>')),[],none),bytecodeMethod(1,1,0,methodId('Object',0),[]),final(false),static(false),public)]),class(className(packageName('java/lang/'),shortClassName('String')),final(false),public(false),abstract(false),className(packageName('java/lang/'),shortClassName('Object')),[],[],[method(methodSignature(methodName(className(packageName('java/lang/'),shortClassName('String')),shortMethodName('<init>')),[],none),bytecodeMethod(1,1,0,methodId('String',0),[]),final(false),static(false),private)]),class(className(packageName('java/lang/'),shortClassName('NullPointerException')),final(false),public(false),abstract(false),className(packageName('java/lang/'),shortClassName('Object')),[],[],[method(methodSignature(methodName(className(packageName('java/lang/'),shortClassName('NullPointerException')),shortMethodName('<init>')),[],none),bytecodeMethod(1,1,0,methodId('NullPointerException',0),[]),final(false),static(false),private)]),class(className(packageName('java/lang/'),shortClassName('ArrayStoreException')),final(false),public(false),abstract(false),className(packageName('java/lang/'),shortClassName('Object')),[],[],[method(methodSignature(methodName(className(packageName('java/lang/'),shortClassName('ArrayStoreException')),shortMethodName('<init>')),[],none),bytecodeMethod(1,1,0,methodId('ArrayStoreException',0),[]),final(false),static(false),private)]),class(className(packageName('java/lang/'),shortClassName('ArrayIndexOutOfBoundsException')),final(false),public(false),abstract(false),className(packageName('java/lang/'),shortClassName('Object')),[],[],[method(methodSignature(methodName(className(packageName('java/lang/'),shortClassName('ArrayIndexOutOfBoundsException')),shortMethodName('<init>')),[],none),bytecodeMethod(1,1,0,methodId('ArrayIndexOutOfBoundsException',0),[]),final(false),static(false),private)]),class(className(packageName('java/lang/'),shortClassName('NegativeArraySizeException')),final(false),public(false),abstract(false),className(packageName('java/lang/'),shortClassName('Object')),[],[],[method(methodSignature(methodName(className(packageName('java/lang/'),shortClassName('NegativeArraySizeException')),shortMethodName('<init>')),[],none),bytecodeMethod(1,1,0,methodId('NegativeArraySizeException',0),[]),final(false),static(false),private)]),class(className(packageName('java/lang/'),shortClassName('ClassCastException')),final(false),public(false),abstract(false),className(packageName('java/lang/'),shortClassName('Object')),[],[],[method(methodSignature(methodName(className(packageName('java/lang/'),shortClassName('ClassCastException')),shortMethodName('<init>')),[],none),bytecodeMethod(1,1,0,methodId('ClassCastException',0),[]),final(false),static(false),private)]),class(className(packageName('java/lang/'),shortClassName('ArithmeticException')),final(false),public(false),abstract(false),className(packageName('java/lang/'),shortClassName('Object')),[],[],[method(methodSignature(methodName(className(packageName('java/lang/'),shortClassName('ArithmeticException')),shortMethodName('<init>')),[],none),bytecodeMethod(1,1,0,methodId('ArithmeticException',0),[]),final(false),static(false),private)])],[]),st(heap(dynamicHeap([array(locationArray(A,primitiveType(int)),[num(int(C))|B])]),staticHeap([])),fr(method(methodSignature(methodName(className(packageName(''),shortClassName('LinearSearch')),shortMethodName(search)),[refType(arrayType(primitiveType(int))),primitiveType(int)],primitiveType(int)),bytecodeMethod(5,2,0,methodId('0',1),[]),final(false),static(true),public),8,[],[ref(loc(1)),num(int(D)),num(int(A)),num(int(1)),num(int(E))]),[]),st(F,fr(H,I,[K|L],J),G)) .
execute_notrace_3(A,B,C,_1,0,D,[array(A,[num(int(C))|B]),[]],_2,_3,_4,_5,refE(loc(2)),[]) :-
        D<A,
        D<0 .
execute_notrace_3(A,B,C,_1,0,D,[array(A,[num(int(C))|B]),[]],_2,_3,_4,_5,refE(loc(2)),[]) :-
        D<A,
        D>=A .


