:- 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=0,
0=0,
00,
execute_notrace_3(A,B,C,1,0,0,_1,_2,_3,_4,_5,D,_6) .
main([[ref(loc(1))],[array(A,[num(int(B))|_1])]],[ref(loc(2))]) :-
0=0,
0>=A .
main([[ref(loc(1))],[array(A,[num(int(C))|B])]],[D]) :-
0=A .
main([[null],[]],[ref(loc(1))]).
execute_notrace_1(A,B,C,heap(dynamicHeap([array(locationArray(A,primitiveType(int)),[num(int(C))|B])]),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(A)),num(int(1)),num(int(1)),num(int(1))],num(int(1)),[]) :-
1>=A .
execute_notrace_1(A,[num(int(D))|C],B,E,F,G,H,I,J,K) :-
1=0,
1=0,
10,
execute_notrace_3(A,[num(int(D))|C],B,2,2,1,E,F,G,H,I,J,K) .
execute_notrace_1(A,[num(int(D))|C],B,heap(dynamicHeap([array(locationArray(A,primitiveType(int)),[num(int(B)),num(int(D))|C]),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,_1,ref(loc(2)),[]) :-
1=0,
1>=A .
execute_notrace_1(A,[num(int(D))|C],B,E,F,G,H,I,J,K) :-
1=A .
execute_notrace_2(A,B,C,D,E,heap(dynamicHeap([array(locationArray(A,primitiveType(int)),[num(int(C))|B])]),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(A)),num(int(D)),num(int(E)),num(int(D))],num(int(E)),[]) :-
D>=A .
execute_notrace_2(A,B,C,D,E,F,G,H,I,J,K,L) :-
D=0,
0==0,
0=0,
Q is E+D,
R is D+1,
execute_notrace_3(A,B,C,R,Q,D,F,G,H,I,J,K,L) .
execute_notrace_2(A,B,C,D,_1,heap(dynamicHeap([array(locationArray(A,primitiveType(int)),[num(int(C))|B]),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,_2,ref(loc(2)),[]) :-
D=0,
D<0 .
execute_notrace_2(A,B,C,D,_1,heap(dynamicHeap([array(locationArray(A,primitiveType(int)),[num(int(C))|B]),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,_2,ref(loc(2)),[]) :-
D=0,
D>=A .
execute_notrace_2(A,B,C,D,E,F,G,H,I,J,K,L) :-
D=A .
execute_notrace_3(A,B,C,D,E,F,heap(dynamicHeap([array(locationArray(A,primitiveType(int)),[num(int(C))|B])]),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(A)),num(int(D)),num(int(E)),num(int(F))],num(int(E)),[]) :-
D>=A .
execute_notrace_3(A,B,C,D,E,F,G,H,I,J,K,L,M) :-
D=0,
0==0,
0=0,
R is E+F,
S is D+1,
execute_notrace_3(A,B,C,S,R,F,G,H,I,J,K,L,M) .
execute_notrace_3(A,B,C,D,_1,_2,heap(dynamicHeap([array(locationArray(A,primitiveType(int)),[num(int(C))|B]),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)),[]) :-
D=0,
D<0 .
execute_notrace_3(A,B,C,D,_1,_2,heap(dynamicHeap([array(locationArray(A,primitiveType(int)),[num(int(C))|B]),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)),[]) :-
D=0,
D>=A .
execute_notrace_3(A,B,C,D,E,F,G,H,I,J,K,L,M) :-
D=A .