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

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

execute_notrace_1(A,B,C,D,E,heap(dynamicHeap([array(locationArray(B,primitiveType(int)),A)]),staticHeap([])),[],method(methodSignature(methodName(className(packageName(''),shortClassName('Signs')),shortMethodName(signs)),[refType(arrayType(primitiveType(int)))],primitiveType(int)),bytecodeMethod(5,2,0,methodId('0',1),[]),final(false),static(true),public),56,[ref(loc(1)),num(int(B)),num(int(C)),num(int(D)),num(int(E))],num(int(D)),[]) :-
        C>=B .
execute_notrace_1(A,B,C,D,E,F,G,H,I,J,K,L) :-
        C<B,
        0=<C,
        C<B,
        M is C+1,
        mynth(M,A,num(int(N))),
        N>=0,
        0=<C,
        C<B,
        O is C+1,
        mynth(O,A,num(int(P))),
        P=<0,
        Q is E+1,
        R is D+Q,
        S is C+1,
        execute_notrace_1(A,B,S,R,Q,F,G,H,I,J,K,L) .
execute_notrace_1(A,B,C,D,E,F,G,H,I,J,K,L) :-
        C<B,
        0=<C,
        C<B,
        M is C+1,
        mynth(M,A,num(int(N))),
        N>=0,
        0=<C,
        C<B,
        O is C+1,
        mynth(O,A,num(int(P))),
        P>0,
        Q is D+E,
        R is C+1,
        execute_notrace_1(A,B,R,Q,E,F,G,H,I,J,K,L) .
execute_notrace_1(A,B,C,_1,_2,heap(dynamicHeap([array(locationArray(B,primitiveType(int)),A),object(locationObject(className(packageName('java/lang/'),shortClassName('ArrayIndexOutOfBoundsException'))),[])]),staticHeap([])),[],method(methodSignature(methodName(className(packageName(''),shortClassName('Signs')),shortMethodName(signs)),[refType(arrayType(primitiveType(int)))],primitiveType(int)),bytecodeMethod(5,2,0,methodId('0',1),[]),final(false),static(true),public),29,_3,ref(loc(2)),[]) :-
        C<B,
        0=<C,
        C<B,
        D is C+1,
        mynth(D,A,num(int(E))),
        E>=0,
        C<0 .
execute_notrace_1(A,B,C,_1,_2,heap(dynamicHeap([array(locationArray(B,primitiveType(int)),A),object(locationObject(className(packageName('java/lang/'),shortClassName('ArrayIndexOutOfBoundsException'))),[])]),staticHeap([])),[],method(methodSignature(methodName(className(packageName(''),shortClassName('Signs')),shortMethodName(signs)),[refType(arrayType(primitiveType(int)))],primitiveType(int)),bytecodeMethod(5,2,0,methodId('0',1),[]),final(false),static(true),public),29,_3,ref(loc(2)),[]) :-
        C<B,
        0=<C,
        C<B,
        D is C+1,
        mynth(D,A,num(int(E))),
        E>=0,
        C>=B .
execute_notrace_1(A,B,C,D,E,F,G,H,I,J,K,L) :-
        C<B,
        0=<C,
        C<B,
        M is C+1,
        mynth(M,A,num(int(N))),
        N<0,
        O is E+1,
        P is C+1,
        execute_notrace_1(A,B,P,D,O,F,G,H,I,J,K,L) .
execute_notrace_1(A,B,C,_1,_2,heap(dynamicHeap([array(locationArray(B,primitiveType(int)),A),object(locationObject(className(packageName('java/lang/'),shortClassName('ArrayIndexOutOfBoundsException'))),[])]),staticHeap([])),[],method(methodSignature(methodName(className(packageName(''),shortClassName('Signs')),shortMethodName(signs)),[refType(arrayType(primitiveType(int)))],primitiveType(int)),bytecodeMethod(5,2,0,methodId('0',1),[]),final(false),static(true),public),17,_3,ref(loc(2)),[]) :-
        C<B,
        C<0 .
execute_notrace_1(A,B,C,_1,_2,heap(dynamicHeap([array(locationArray(B,primitiveType(int)),A),object(locationObject(className(packageName('java/lang/'),shortClassName('ArrayIndexOutOfBoundsException'))),[])]),staticHeap([])),[],method(methodSignature(methodName(className(packageName(''),shortClassName('Signs')),shortMethodName(signs)),[refType(arrayType(primitiveType(int)))],primitiveType(int)),bytecodeMethod(5,2,0,methodId('0',1),[]),final(false),static(true),public),17,_3,ref(loc(2)),[]) :-
        C<B,
        C>=B .


