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(); int v104 = nondet(); int v105 = nondet(); int v106 = nondet(); int v107 = nondet(); int v108 = nondet(); int v109 = nondet(); int v110 = nondet(); int v111 = nondet(); int v112 = nondet(); int v113 = nondet(); int v114 = nondet(); int v115 = nondet(); int v116 = nondet(); int v117 = nondet(); int v118 = nondet(); goto loc_46; loc_46: if (nondet_bool()) { goto loc_45; } goto end; loc_CP_1: if (nondet_bool()) { v109 = v58; v58 = -1+v58; goto loc_7; } goto end; loc_CP_8: if (nondet_bool()) { goto loc_9; } goto end; loc_CP_10: if (nondet_bool()) { v83 = nondet(); v17 = -1; v93 = 0; v102 = v93; goto loc_11; } goto end; loc_CP_12: if (nondet_bool()) { goto loc_13; } goto end; loc_CP_27: if (nondet_bool()) { goto loc_28; } goto end; loc_0: if (nondet_bool()) { v73 = nondet(); v42 = nondet(); v74 = nondet(); v63 = v62; v117 = 0; v97 = nondet(); v9 = 1; v7 = 0; v66 = v65; v75 = nondet(); v118 = 0; v65 = nondet(); if (!( 1 <= v65 )) goto end; v60 = v32; v58 = v65; goto loc_CP_1; } goto end; loc_2: if (nondet_bool()) { v14 = 1; goto loc_0; } goto end; loc_3: if (nondet_bool()) { if (!( v105 <= 0 )) goto end; if (!( 0 <= v105 )) goto end; goto loc_0; } if (nondet_bool()) { if (!( 1 <= v105 )) goto end; goto loc_2; } if (nondet_bool()) { if (!( 1+v105 <= 0 )) goto end; goto loc_2; } goto end; loc_4: if (nondet_bool()) { v96 = 0; v105 = v96; goto loc_3; } goto end; loc_5: if (nondet_bool()) { v3 = 3; v1 = 1; v103 = v102; v41 = nondet(); v12 = nondet(); v46 = v33; v48 = v27; v13 = 1; goto loc_4; } goto end; loc_6: if (nondet_bool()) { if (!( v102 <= 7 )) goto end; if (!( 7 <= v102 )) goto end; goto loc_4; } if (nondet_bool()) { if (!( 8 <= v102 )) goto end; goto loc_5; } if (nondet_bool()) { if (!( 1+v102 <= 7 )) goto end; goto loc_5; } goto end; loc_13: if (nondet_bool()) { goto loc_CP_12; } goto end; loc_14: if (nondet_bool()) { goto loc_15; } goto end; loc_16: if (nondet_bool()) { v55 = 1; goto loc_17; } goto end; loc_18: if (nondet_bool()) { if (!( v38 <= v114 )) goto end; if (!( v114 <= v38 )) goto end; goto loc_17; } if (nondet_bool()) { if (!( 1+v114 <= v38 )) goto end; goto loc_16; } if (nondet_bool()) { if (!( 1+v38 <= v114 )) goto end; goto loc_16; } goto end; loc_19: if (nondet_bool()) { v114 = nondet(); goto loc_18; } goto end; loc_17: if (nondet_bool()) { goto loc_CP_8; } goto end; loc_20: if (nondet_bool()) { if (!( 8 <= v115 )) goto end; goto loc_19; } if (nondet_bool()) { if (!( 1+v115 <= 7 )) goto end; goto loc_19; } if (nondet_bool()) { if (!( v115 <= 7 )) goto end; if (!( 7 <= v115 )) goto end; v55 = 1; goto loc_17; } goto end; loc_21: if (nondet_bool()) { v23 = nondet(); v106 = nondet(); v91 = v106; v115 = v91; goto loc_20; } goto end; loc_22: if (nondet_bool()) { v53 = v52; v51 = nondet(); v54 = v52; goto loc_21; } goto end; loc_23: if (nondet_bool()) { if (!( v52 <= 0 )) goto end; if (!( 0 <= v52 )) goto end; goto loc_21; } if (nondet_bool()) { if (!( 1 <= v52 )) goto end; goto loc_22; } if (nondet_bool()) { if (!( 1+v52 <= 0 )) goto end; goto loc_22; } goto end; loc_24: if (nondet_bool()) { goto loc_17; } goto end; loc_25: if (nondet_bool()) { if (!( v102 <= 7 )) goto end; if (!( 7 <= v102 )) goto end; goto loc_26; } if (nondet_bool()) { if (!( 8 <= v102 )) goto end; goto loc_24; } if (nondet_bool()) { if (!( 1+v102 <= 7 )) goto end; goto loc_24; } goto end; loc_26: if (nondet_bool()) { v86 = nondet(); v44 = nondet(); v50 = nondet(); v64 = v62; v99 = nondet(); v47 = nondet(); v92 = 0; v52 = v92; goto loc_23; } goto end; loc_28: if (nondet_bool()) { goto loc_CP_27; } goto end; loc_29: if (nondet_bool()) { if (!( 5 <= v102 )) goto end; goto loc_25; } if (nondet_bool()) { if (!( 1+v102 <= 4 )) goto end; goto loc_25; } if (nondet_bool()) { if (!( v102 <= 4 )) goto end; if (!( 4 <= v102 )) goto end; v22 = 1; goto loc_26; } goto end; loc_30: if (nondet_bool()) { v60 = 1; goto loc_31; } goto end; loc_32: if (nondet_bool()) { if (!( 1+v59 <= v67 )) goto end; goto loc_30; } if (nondet_bool()) { if (!( v67 <= v59 )) goto end; v59 = 0; goto loc_30; } goto end; loc_33: if (nondet_bool()) { goto loc_34; } goto end; loc_34: if (nondet_bool()) { goto loc_CP_10; } goto end; loc_35: if (nondet_bool()) { if (!( v101 <= 0 )) goto end; if (!( 0 <= v101 )) goto end; goto loc_34; } if (nondet_bool()) { if (!( 1 <= v101 )) goto end; goto loc_CP_12; } if (nondet_bool()) { if (!( 1+v101 <= 0 )) goto end; goto loc_CP_12; } goto end; loc_36: if (nondet_bool()) { if (!( v68 <= 0 )) goto end; if (!( 0 <= v68 )) goto end; goto loc_34; } if (nondet_bool()) { if (!( 1 <= v68 )) goto end; goto loc_35; } if (nondet_bool()) { if (!( 1+v68 <= 0 )) goto end; goto loc_35; } goto end; loc_37: if (nondet_bool()) { if (!( v112 <= 0 )) goto end; if (!( 0 <= v112 )) goto end; v4 = 3; v2 = 2; v104 = v102; v43 = nondet(); v19 = nondet(); v20 = 1; goto loc_32; } if (nondet_bool()) { if (!( 1 <= v112 )) goto end; goto loc_36; } if (nondet_bool()) { if (!( 1+v112 <= 0 )) goto end; goto loc_36; } goto end; loc_38: if (nondet_bool()) { v18 = v102; v88 = 0; v112 = v88; goto loc_37; } goto end; loc_11: if (nondet_bool()) { if (!( v102 <= 7 )) goto end; if (!( 7 <= v102 )) goto end; goto loc_32; } if (nondet_bool()) { if (!( 8 <= v102 )) goto end; goto loc_38; } if (nondet_bool()) { if (!( 1+v102 <= 7 )) goto end; goto loc_38; } goto end; loc_31: if (nondet_bool()) { v102 = nondet(); v89 = 0; v113 = v89; v21 = v113; goto loc_29; } goto end; loc_39: if (nondet_bool()) { if (!( 2 <= v65 )) goto end; goto loc_CP_10; } if (nondet_bool()) { if (!( 1+v65 <= 1 )) goto end; goto loc_CP_10; } if (nondet_bool()) { if (!( v65 <= 1 )) goto end; if (!( 1 <= v65 )) goto end; v60 = v32; goto loc_31; } goto end; loc_40: if (nondet_bool()) { v98 = nondet(); v10 = 1; v8 = 0; v90 = 0; v111 = v90; v16 = v111; v56 = 1; v56 = 0; goto loc_39; } goto end; loc_41: if (nondet_bool()) { if (!( 1+v110 <= v37 )) goto end; goto loc_40; } if (nondet_bool()) { if (!( v37 <= v110 )) goto end; v15 = 0; goto loc_40; } goto end; loc_42: if (nondet_bool()) { if (!( v37 <= 0 )) goto end; goto loc_40; } if (nondet_bool()) { if (!( 1 <= v37 )) goto end; v110 = v87; v87 = 1+v87; goto loc_41; } goto end; loc_43: if (nondet_bool()) { v11 = 0; goto loc_CP_27; } goto end; loc_9: if (nondet_bool()) { if (!( 1 <= v55 )) goto end; goto loc_43; } if (nondet_bool()) { if (!( 1+v55 <= 0 )) goto end; goto loc_43; } if (nondet_bool()) { if (!( v55 <= 0 )) goto end; if (!( 0 <= v55 )) goto end; v85 = nondet(); goto loc_42; } goto end; loc_44: if (nondet_bool()) { v77 = 0; v80 = 6; v79 = 1; v81 = 5; v78 = v60; v82 = nondet(); goto loc_CP_1; } goto end; loc_7: if (nondet_bool()) { if (!( v109 <= 0 )) goto end; if (!( 0 <= v109 )) goto end; v61 = 8; goto loc_CP_8; } if (nondet_bool()) { if (!( 1 <= v109 )) goto end; goto loc_44; } if (nondet_bool()) { if (!( 1+v109 <= 0 )) goto end; goto loc_44; } goto end; loc_45: if (nondet_bool()) { v49 = nondet(); if (!( 1 <= v49 )) goto end; v56 = 0; v55 = 0; v59 = 0; v45 = 0; v31 = 0; v30 = 0; v29 = 0; v28 = 0; v100 = 256; v57 = 0; v32 = nondet(); if (!( 1 <= v32 )) goto end; v61 = 9; v62 = v49; v107 = nondet(); v95 = v107; v39 = v95; v87 = 0; v40 = nondet(); v24 = nondet(); v36 = v35; v76 = nondet(); v5 = 0; v25 = nondet(); v26 = nondet(); v69 = nondet(); v70 = nondet(); v84 = nondet(); v71 = nondet(); v6 = 0; v116 = 0; v34 = v33; v72 = nondet(); v108 = nondet(); v94 = v108; v102 = v94; goto loc_6; } goto end; loc_15: end: ; }