int nondet() { int a; return a; } _Bool nondet_bool() { _Bool a; return a; } int main() { int v1 = nondet(); int v2 = nondet(); int v3 = nondet(); int v4 = nondet(); int v5 = nondet(); int v6 = nondet(); int v7 = nondet(); int v8 = nondet(); int v9 = nondet(); int v10 = nondet(); int v11 = nondet(); int v12 = nondet(); int v13 = nondet(); int v14 = nondet(); int v15 = nondet(); int v16 = nondet(); int v17 = nondet(); int v18 = nondet(); int v19 = nondet(); int v20 = nondet(); int v21 = nondet(); int v22 = nondet(); int v23 = nondet(); int v24 = nondet(); int v25 = nondet(); int v26 = nondet(); int v27 = nondet(); int v28 = nondet(); int v29 = nondet(); int v30 = nondet(); int v31 = nondet(); int v32 = nondet(); int v33 = nondet(); int v34 = nondet(); int v35 = nondet(); int v36 = nondet(); int v37 = nondet(); int v38 = nondet(); int v39 = nondet(); int v40 = nondet(); int v41 = nondet(); int v42 = nondet(); int v43 = nondet(); int v44 = nondet(); int v45 = nondet(); int v46 = nondet(); int v47 = nondet(); int v48 = nondet(); int v49 = nondet(); int v50 = nondet(); int v51 = nondet(); int v52 = nondet(); int v53 = nondet(); int v54 = nondet(); int v55 = nondet(); int v56 = nondet(); int v57 = nondet(); int v58 = nondet(); int v59 = nondet(); int v60 = nondet(); int v61 = nondet(); int v62 = nondet(); int v63 = nondet(); int v64 = nondet(); int v65 = nondet(); int v66 = nondet(); int v67 = nondet(); int v68 = nondet(); int v69 = nondet(); int v70 = nondet(); int v71 = nondet(); int v72 = nondet(); int v73 = nondet(); int v74 = nondet(); int v75 = nondet(); int v76 = nondet(); int v77 = nondet(); int v78 = nondet(); int v79 = nondet(); int v80 = nondet(); int v81 = nondet(); int v82 = nondet(); int v83 = nondet(); int v84 = nondet(); int v85 = nondet(); int v86 = nondet(); int v87 = nondet(); int v88 = nondet(); int v89 = nondet(); int v90 = nondet(); int v91 = nondet(); int v92 = nondet(); int v93 = nondet(); int v94 = nondet(); int v95 = nondet(); int v96 = nondet(); int v97 = nondet(); int v98 = nondet(); int v99 = nondet(); int v100 = nondet(); int v101 = nondet(); int v102 = nondet(); int v103 = nondet(); goto loc_42; loc_42: if (nondet_bool()) { goto loc_41; } goto end; loc_CP_1: if (nondet_bool()) { goto loc_6; } goto end; loc_CP_7: if (nondet_bool()) { goto loc_8; } goto end; loc_CP_9: if (nondet_bool()) { v72 = nondet(); v11 = -1; v82 = 0; v91 = v82; goto loc_10; } goto end; loc_CP_11: if (nondet_bool()) { goto loc_12; } goto end; loc_CP_21: if (nondet_bool()) { goto loc_22; } goto end; loc_0: if (nondet_bool()) { v62 = nondet(); v34 = nondet(); v63 = nondet(); v52 = v51; v102 = 0; v86 = nondet(); v5 = 1; v3 = 0; v55 = v54; v64 = nondet(); v103 = 0; v54 = nondet(); if (!( 1 <= v54 )) goto end; v49 = v25; v47 = v54; goto loc_CP_1; } goto end; loc_2: if (nondet_bool()) { if (!( v92 <= 0 )) goto end; goto loc_0; } if (nondet_bool()) { if (!( 1 <= v92 )) goto end; v8 = 1; goto loc_0; } goto end; loc_3: if (nondet_bool()) { v85 = 0; v92 = v85; goto loc_2; } goto end; loc_4: if (nondet_bool()) { v7 = 1; goto loc_3; } goto end; loc_5: if (nondet_bool()) { if (!( v91 <= 7 )) goto end; if (!( 7 <= v91 )) goto end; goto loc_3; } if (nondet_bool()) { if (!( 8 <= v91 )) goto end; goto loc_4; } if (nondet_bool()) { if (!( 1+v91 <= 7 )) goto end; goto loc_4; } goto end; loc_12: if (nondet_bool()) { goto loc_CP_11; } goto end; loc_13: if (nondet_bool()) { goto loc_14; } goto end; loc_15: if (nondet_bool()) { v44 = 1; goto loc_16; } goto end; loc_17: if (nondet_bool()) { if (!( v31 <= 0 )) goto end; if (!( 0 <= v31 )) goto end; goto loc_16; } if (nondet_bool()) { if (!( 1 <= v31 )) goto end; goto loc_15; } if (nondet_bool()) { if (!( 1+v31 <= 0 )) goto end; goto loc_15; } goto end; loc_18: if (nondet_bool()) { goto loc_17; } goto end; loc_16: if (nondet_bool()) { goto loc_CP_7; } goto end; loc_19: if (nondet_bool()) { if (!( 8 <= v100 )) goto end; goto loc_18; } if (nondet_bool()) { if (!( 1+v100 <= 7 )) goto end; goto loc_18; } if (nondet_bool()) { if (!( v100 <= 7 )) goto end; if (!( 7 <= v100 )) goto end; v44 = 1; goto loc_16; } goto end; loc_20: if (nondet_bool()) { v16 = nondet(); v95 = nondet(); v80 = v95; v100 = v80; goto loc_19; } goto end; loc_22: if (nondet_bool()) { goto loc_CP_21; } goto end; loc_23: if (nondet_bool()) { if (!( v41 <= 0 )) goto end; goto loc_20; } if (nondet_bool()) { if (!( 1 <= v41 )) goto end; v42 = v41; v40 = nondet(); v43 = v41; goto loc_20; } goto end; loc_24: if (nondet_bool()) { goto loc_16; } goto end; loc_25: if (nondet_bool()) { if (!( v91 <= 7 )) goto end; if (!( 7 <= v91 )) goto end; goto loc_26; } if (nondet_bool()) { if (!( 8 <= v91 )) goto end; goto loc_24; } if (nondet_bool()) { if (!( 1+v91 <= 7 )) goto end; goto loc_24; } goto end; loc_26: if (nondet_bool()) { v75 = nondet(); v35 = nondet(); v39 = nondet(); v53 = v51; v88 = nondet(); v37 = nondet(); v81 = 0; v41 = v81; goto loc_23; } goto end; loc_27: if (nondet_bool()) { if (!( 5 <= v91 )) goto end; goto loc_25; } if (nondet_bool()) { if (!( 1+v91 <= 4 )) goto end; goto loc_25; } if (nondet_bool()) { if (!( v91 <= 4 )) goto end; if (!( 4 <= v91 )) goto end; v15 = 1; goto loc_26; } goto end; loc_28: if (nondet_bool()) { v49 = 1; goto loc_29; } goto end; loc_30: if (nondet_bool()) { if (!( 1+v48 <= v56 )) goto end; goto loc_28; } if (nondet_bool()) { if (!( v56 <= v48 )) goto end; v48 = 0; goto loc_28; } goto end; loc_31: if (nondet_bool()) { goto loc_32; } goto end; loc_32: if (nondet_bool()) { goto loc_CP_9; } goto end; loc_33: if (nondet_bool()) { if (!( v90 <= 0 )) goto end; goto loc_32; } if (nondet_bool()) { if (!( 1 <= v90 )) goto end; goto loc_CP_11; } goto end; loc_34: if (nondet_bool()) { if (!( v57 <= 0 )) goto end; goto loc_32; } if (nondet_bool()) { if (!( 1 <= v57 )) goto end; goto loc_33; } goto end; loc_35: if (nondet_bool()) { if (!( v98 <= 0 )) goto end; v13 = 1; goto loc_30; } if (nondet_bool()) { if (!( 1 <= v98 )) goto end; goto loc_34; } goto end; loc_36: if (nondet_bool()) { v12 = v91; v77 = 0; v98 = v77; goto loc_35; } goto end; loc_10: if (nondet_bool()) { if (!( v91 <= 7 )) goto end; if (!( 7 <= v91 )) goto end; goto loc_30; } if (nondet_bool()) { if (!( 8 <= v91 )) goto end; goto loc_36; } if (nondet_bool()) { if (!( 1+v91 <= 7 )) goto end; goto loc_36; } goto end; loc_29: if (nondet_bool()) { v91 = nondet(); v78 = 0; v99 = v78; v14 = v99; goto loc_27; } goto end; loc_37: if (nondet_bool()) { if (!( 2 <= v54 )) goto end; goto loc_CP_9; } if (nondet_bool()) { if (!( 1+v54 <= 1 )) goto end; goto loc_CP_9; } if (nondet_bool()) { if (!( v54 <= 1 )) goto end; if (!( 1 <= v54 )) goto end; v49 = v25; goto loc_29; } goto end; loc_38: if (nondet_bool()) { v87 = nondet(); v6 = 1; v4 = 0; v79 = 0; v97 = v79; v10 = v97; v45 = 1; v45 = 0; goto loc_37; } goto end; loc_39: if (nondet_bool()) { if (!( 1+v96 <= v30 )) goto end; goto loc_38; } if (nondet_bool()) { if (!( v30 <= v96 )) goto end; v9 = 0; goto loc_38; } goto end; loc_40: if (nondet_bool()) { if (!( v30 <= 0 )) goto end; goto loc_38; } if (nondet_bool()) { if (!( 1 <= v30 )) goto end; v96 = v76; v76 = 1+v76; goto loc_39; } goto end; loc_8: if (nondet_bool()) { if (!( v44 <= 0 )) goto end; v74 = nondet(); goto loc_40; } if (nondet_bool()) { if (!( 1 <= v44 )) goto end; v17 = 0; goto loc_CP_21; } goto end; loc_6: if (nondet_bool()) { if (!( 1 <= v47 )) goto end; v66 = 0; v69 = 6; v68 = 1; v70 = 5; v67 = v49; v71 = nondet(); v47 = -1+v47; goto loc_CP_1; } if (nondet_bool()) { if (!( v47 <= 0 )) goto end; v50 = 8; goto loc_CP_7; } goto end; loc_41: if (nondet_bool()) { v38 = nondet(); if (!( 1 <= v38 )) goto end; v45 = 0; v44 = 0; v48 = 0; v36 = 0; v24 = 0; v23 = 0; v22 = 0; v21 = 0; v89 = 256; v46 = 0; v25 = nondet(); if (!( 1 <= v25 )) goto end; v50 = 9; v51 = v38; v93 = nondet(); v84 = v93; v32 = v84; v76 = 0; v33 = nondet(); v18 = nondet(); v29 = v28; v65 = nondet(); v1 = 0; v19 = nondet(); v20 = nondet(); v58 = nondet(); v59 = nondet(); v73 = nondet(); v60 = nondet(); v2 = 0; v101 = 0; v27 = v26; v61 = nondet(); v94 = nondet(); v83 = v94; v91 = v83; goto loc_5; } goto end; loc_14: end: ; }