1void __VERIFIER_assert(int cond) {
2 if (!(cond)) {
3 ERROR: goto ERROR;
4 }
5 return;
6}
7int INFINITY = 899;
8unsigned int __VERIFIER_nondet_uint();
9void main(){
10 int nodecount = __VERIFIER_nondet_uint()%5;
11 int edgecount = __VERIFIER_nondet_uint()%20;
12 int source = 0;
13 int Source[20] = {0,4,1,1,0,0,1,3,4,4,2,2,3,0,0,3,1,2,2,3};
14 int Dest[20] = {1,3,4,1,1,4,3,4,3,0,0,0,0,2,3,0,2,1,0,4};
15 int Weight[20] = {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19};
16 int distance[5];
17 int x,y;
18 int i,j;
19
20 for(i = 0; i < nodecount; i++){
21 if(i == source){
22 distance[i] = 0;
23 }
24 else {
25 distance[i] = INFINITY;
26 }
27 }
28
29 for(i = 0; i < nodecount; i++)
30 {
31 for(j = 0; j < edgecount; j++)
32 {
33 x = Dest[j];
34 y = Source[j];
35 if(distance[x] > distance[y] + Weight[j])
36 {
37 distance[x] = -1;
38 }
39 }
40 }
41 for(i = 0; i < edgecount; i++)
42 {
43 x = Dest[i];
44 y = Source[i];
45 if(distance[x] > distance[y] + Weight[i])
46 {
47 return;
48 }
49 }
50
51 for(i = 0; i < nodecount; i++)
52 {
53 __VERIFIER_assert(distance[i]>=0);
54 }
55
56}