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(); goto loc_76; loc_76: if (nondet_bool()) { goto loc_22; } goto end; loc_CP_3: if (nondet_bool()) { v43 = v49; v42 = v48; v45 = v51; v44 = v50; v47 = v53; v46 = v52; goto loc_2; } goto end; loc_CP_8: if (nondet_bool()) { v50 = 0; v31 = v49; v30 = v48; v33 = v51; v32 = v50; v35 = v53; v34 = v52; goto loc_7; } goto end; loc_CP_17: if (nondet_bool()) { v69 = 8; v67 = nondet(); v69 = 9; goto loc_15; } goto end; loc_CP_19: if (nondet_bool()) { v69 = 1; goto loc_56; } goto end; loc_CP_65: if (nondet_bool()) { if (!( v61 <= 0 )) goto end; goto loc_61; } if (nondet_bool()) { if (!( 1 <= v61 )) goto end; v63 = 10; v62 = 0; v31 = v61; v30 = v60; v33 = v63; v32 = v62; v35 = v65; v34 = v64; goto loc_64; } goto end; loc_0: if (nondet_bool()) { v19 = v24; v24 = v19; goto loc_1; } goto end; loc_2: if (nondet_bool()) { if (!( v44 <= 0 )) goto end; v24 = 0; goto loc_0; } if (nondet_bool()) { if (!( 1 <= v44 )) goto end; v24 = 1; goto loc_0; } goto end; loc_4: if (nondet_bool()) { if (!( 1 <= v24 )) goto end; goto loc_CP_3; } if (nondet_bool()) { if (!( 1+v24 <= 1 )) goto end; v25 = v24; v20 = 0; goto loc_5; } goto end; loc_6: if (nondet_bool()) { v17 = v24; v24 = v17; goto loc_4; } goto end; loc_7: if (nondet_bool()) { if (!( v32 <= 0 )) goto end; v24 = 0; goto loc_6; } if (nondet_bool()) { if (!( 1 <= v32 )) goto end; v24 = 1; goto loc_6; } goto end; loc_9: if (nondet_bool()) { if (!( v49 <= 0 )) goto end; goto loc_CP_3; } if (nondet_bool()) { if (!( 1 <= v49 )) goto end; v51 = 10; goto loc_CP_8; } goto end; loc_10: if (nondet_bool()) { v51 = 8; v49 = nondet(); v51 = 9; goto loc_9; } goto end; loc_11: if (nondet_bool()) { if (!( v48 <= 0 )) goto end; v51 = 6; v53 = -1+v53; goto loc_12; } if (nondet_bool()) { if (!( 1 <= v48 )) goto end; v51 = 5; v53 = 1+v53; goto loc_12; } goto end; loc_13: if (nondet_bool()) { if (!( v53 <= 0 )) goto end; v51 = 3; v48 = nondet(); v51 = 4; goto loc_11; } if (nondet_bool()) { if (!( v53 <= 0 )) goto end; v51 = 2; v51 = 7; goto loc_10; } goto end; loc_12: if (nondet_bool()) { v51 = 1; goto loc_13; } goto end; loc_14: if (nondet_bool()) { v51 = 0; goto loc_12; } goto end; loc_15: if (nondet_bool()) { if (!( v67 <= 0 )) goto end; goto loc_16; } if (nondet_bool()) { if (!( 1 <= v67 )) goto end; v69 = 10; v68 = 0; v49 = v67; v48 = v66; v51 = v69; v50 = v68; v53 = v71; v52 = v70; goto loc_CP_8; } goto end; loc_18: if (nondet_bool()) { if (!( v9 <= 0 )) goto end; goto loc_CP_19; } if (nondet_bool()) { if (!( 1 <= v9 )) goto end; v7 = 1; v5 = v67; v2 = v66; v15 = v69; v12 = v68; v73 = v71; v28 = v70; goto loc_CP_19; } goto end; loc_20: if (nondet_bool()) { if (!( 1 <= 0 )) goto end; goto loc_CP_19; } if (nondet_bool()) { v23 = 0; goto loc_21; } goto end; loc_22: if (nondet_bool()) { v11 = 0; v14 = 0; v67 = v4; v66 = v1; v69 = v14; v68 = v11; v71 = v72; v70 = v27; v8 = 0; v7 = 0; goto loc_CP_19; } goto end; loc_21: if (nondet_bool()) { v26 = v23; goto loc_24; } goto end; loc_24: if (nondet_bool()) { if (!( 1+v26 <= 1 )) goto end; goto loc_23; } if (nondet_bool()) { if (!( 2 <= v26 )) goto end; goto loc_23; } goto end; loc_25: if (nondet_bool()) { if (!( 1+v25 <= 1 )) goto end; goto loc_21; } if (nondet_bool()) { if (!( 1 <= v25 )) goto end; v26 = v25; v23 = 1; goto loc_21; } goto end; loc_26: if (nondet_bool()) { v25 = v21; goto loc_25; } goto end; loc_27: if (nondet_bool()) { if (!( v7 <= 0 )) goto end; v9 = nondet(); goto loc_18; } if (nondet_bool()) { if (!( 1 <= v7 )) goto end; goto loc_20; } goto end; loc_28: if (nondet_bool()) { if (!( 1 <= v24 )) goto end; goto loc_26; } if (nondet_bool()) { if (!( 1+v24 <= 1 )) goto end; v25 = v24; v21 = 0; goto loc_26; } goto end; loc_29: if (nondet_bool()) { v18 = v24; v24 = v18; goto loc_28; } goto end; loc_30: if (nondet_bool()) { if (!( v38 <= 0 )) goto end; v24 = 0; goto loc_29; } if (nondet_bool()) { if (!( 1 <= v38 )) goto end; v24 = 1; goto loc_29; } goto end; loc_31: if (nondet_bool()) { v37 = v55; v36 = v54; v39 = v57; v38 = v56; v41 = v59; v40 = v58; goto loc_30; } goto end; loc_32: if (nondet_bool()) { if (!( 1 <= v24 )) goto end; goto loc_33; } if (nondet_bool()) { if (!( 1+v24 <= 1 )) goto end; v25 = v24; v21 = 0; goto loc_26; } goto end; loc_34: if (nondet_bool()) { v19 = v24; v24 = v19; goto loc_32; } goto end; loc_35: if (nondet_bool()) { if (!( v44 <= 0 )) goto end; v24 = 0; goto loc_34; } if (nondet_bool()) { if (!( 1 <= v44 )) goto end; v24 = 1; goto loc_34; } goto end; loc_36: if (nondet_bool()) { v43 = v55; v42 = v54; v45 = v57; v44 = v56; v47 = v59; v46 = v58; goto loc_35; } goto end; loc_37: if (nondet_bool()) { if (!( 1 <= v24 )) goto end; goto loc_36; } if (nondet_bool()) { if (!( 1+v24 <= 1 )) goto end; v25 = v24; v21 = 0; goto loc_26; } goto end; loc_38: if (nondet_bool()) { v17 = v24; v24 = v17; goto loc_37; } goto end; loc_39: if (nondet_bool()) { if (!( v32 <= 0 )) goto end; v24 = 0; goto loc_38; } if (nondet_bool()) { if (!( 1 <= v32 )) goto end; v24 = 1; goto loc_38; } goto end; loc_40: if (nondet_bool()) { if (!( v55 <= 0 )) goto end; goto loc_36; } if (nondet_bool()) { if (!( 1 <= v55 )) goto end; v57 = 10; v56 = 0; v31 = v55; v30 = v54; v33 = v57; v32 = v56; v35 = v59; v34 = v58; goto loc_39; } goto end; loc_41: if (nondet_bool()) { if (!( v66 <= 0 )) goto end; v69 = 6; v71 = -1+v71; goto loc_27; } if (nondet_bool()) { if (!( 1 <= v66 )) goto end; v69 = 5; v71 = 1+v71; goto loc_27; } goto end; loc_33: if (nondet_bool()) { v57 = 8; v55 = nondet(); v57 = 9; goto loc_40; } goto end; loc_42: if (nondet_bool()) { if (!( v54 <= 0 )) goto end; v57 = 6; v59 = -1+v59; goto loc_43; } if (nondet_bool()) { if (!( 1 <= v54 )) goto end; v57 = 5; v59 = 1+v59; goto loc_43; } goto end; loc_44: if (nondet_bool()) { if (!( v59 <= 0 )) goto end; v57 = 3; v54 = nondet(); v57 = 4; goto loc_42; } if (nondet_bool()) { if (!( v59 <= 0 )) goto end; v57 = 2; v57 = 7; goto loc_33; } goto end; loc_43: if (nondet_bool()) { v57 = 1; goto loc_44; } goto end; loc_45: if (nondet_bool()) { v57 = 0; goto loc_43; } goto end; loc_46: if (nondet_bool()) { v55 = v67; v54 = v66; v57 = v69; v56 = v68; v59 = v71; v58 = v70; goto loc_33; } goto end; loc_47: if (nondet_bool()) { if (!( v10 <= 0 )) goto end; goto loc_CP_17; } if (nondet_bool()) { if (!( 1 <= v10 )) goto end; v8 = 1; v6 = v67; v3 = v66; v16 = v69; v13 = v68; v74 = v71; v29 = v70; goto loc_CP_17; } goto end; loc_48: if (nondet_bool()) { if (!( 1 <= 0 )) goto end; goto loc_CP_17; } if (nondet_bool()) { v23 = 0; goto loc_21; } goto end; loc_49: if (nondet_bool()) { if (!( v8 <= 0 )) goto end; v10 = nondet(); goto loc_47; } if (nondet_bool()) { if (!( 1 <= v8 )) goto end; goto loc_48; } goto end; loc_50: if (nondet_bool()) { if (!( 1+v25 <= 1 )) goto end; goto loc_49; } if (nondet_bool()) { if (!( 1 <= v25 )) goto end; v26 = v25; v23 = 1; goto loc_21; } goto end; loc_51: if (nondet_bool()) { v25 = v22; goto loc_50; } goto end; loc_52: if (nondet_bool()) { if (!( 1 <= v24 )) goto end; goto loc_51; } if (nondet_bool()) { if (!( 1+v24 <= 1 )) goto end; v25 = v24; v22 = 0; goto loc_51; } goto end; loc_53: if (nondet_bool()) { v18 = v24; v24 = v18; goto loc_52; } goto end; loc_54: if (nondet_bool()) { if (!( v38 <= 0 )) goto end; v24 = 0; goto loc_53; } if (nondet_bool()) { if (!( 1 <= v38 )) goto end; v24 = 1; goto loc_53; } goto end; loc_55: if (nondet_bool()) { v37 = v61; v36 = v60; v39 = v63; v38 = v62; v41 = v65; v40 = v64; goto loc_54; } goto end; loc_56: if (nondet_bool()) { if (!( v71 <= 0 )) goto end; v69 = 3; v66 = nondet(); v69 = 4; goto loc_41; } if (nondet_bool()) { if (!( v71 <= 0 )) goto end; v69 = 2; v69 = 7; goto loc_CP_17; } goto end; loc_57: if (nondet_bool()) { if (!( 1 <= v24 )) goto end; goto loc_58; } if (nondet_bool()) { if (!( 1+v24 <= 1 )) goto end; v25 = v24; v22 = 0; goto loc_51; } goto end; loc_59: if (nondet_bool()) { v19 = v24; v24 = v19; goto loc_57; } goto end; loc_60: if (nondet_bool()) { if (!( v44 <= 0 )) goto end; v24 = 0; goto loc_59; } if (nondet_bool()) { if (!( 1 <= v44 )) goto end; v24 = 1; goto loc_59; } goto end; loc_61: if (nondet_bool()) { v43 = v61; v42 = v60; v45 = v63; v44 = v62; v47 = v65; v46 = v64; goto loc_60; } goto end; loc_62: if (nondet_bool()) { if (!( 1 <= v24 )) goto end; goto loc_61; } if (nondet_bool()) { if (!( 1+v24 <= 1 )) goto end; v25 = v24; v22 = 0; goto loc_51; } goto end; loc_63: if (nondet_bool()) { v17 = v24; v24 = v17; goto loc_62; } goto end; loc_64: if (nondet_bool()) { if (!( v32 <= 0 )) goto end; v24 = 0; goto loc_63; } if (nondet_bool()) { if (!( 1 <= v32 )) goto end; v24 = 1; goto loc_63; } goto end; loc_66: if (nondet_bool()) { v69 = 0; goto loc_CP_19; } goto end; loc_58: if (nondet_bool()) { v63 = 8; v61 = nondet(); v63 = 9; goto loc_CP_65; } goto end; loc_67: if (nondet_bool()) { if (!( v60 <= 0 )) goto end; v63 = 6; v65 = -1+v65; goto loc_68; } if (nondet_bool()) { if (!( 1 <= v60 )) goto end; v63 = 5; v65 = 1+v65; goto loc_68; } goto end; loc_69: if (nondet_bool()) { if (!( v65 <= 0 )) goto end; v63 = 3; v60 = nondet(); v63 = 4; goto loc_67; } if (nondet_bool()) { if (!( v65 <= 0 )) goto end; v63 = 2; v63 = 7; goto loc_58; } goto end; loc_68: if (nondet_bool()) { v63 = 1; goto loc_69; } goto end; loc_70: if (nondet_bool()) { v63 = 0; goto loc_68; } goto end; loc_16: if (nondet_bool()) { v61 = v67; v60 = v66; v63 = v69; v62 = v68; v65 = v71; v64 = v70; goto loc_CP_65; } goto end; loc_71: if (nondet_bool()) { if (!( 1+v25 <= 1 )) goto end; goto loc_16; } if (nondet_bool()) { if (!( 1 <= v25 )) goto end; v26 = v25; v23 = 1; goto loc_21; } goto end; loc_5: if (nondet_bool()) { v25 = v20; goto loc_71; } goto end; loc_72: if (nondet_bool()) { if (!( 1 <= v24 )) goto end; goto loc_5; } if (nondet_bool()) { if (!( 1+v24 <= 1 )) goto end; v25 = v24; v20 = 0; goto loc_5; } goto end; loc_73: if (nondet_bool()) { v18 = v24; v24 = v18; goto loc_72; } goto end; loc_74: if (nondet_bool()) { if (!( v38 <= 0 )) goto end; v24 = 0; goto loc_73; } if (nondet_bool()) { if (!( 1 <= v38 )) goto end; v24 = 1; goto loc_73; } goto end; loc_75: if (nondet_bool()) { v37 = v49; v36 = v48; v39 = v51; v38 = v50; v41 = v53; v40 = v52; goto loc_74; } goto end; loc_1: if (nondet_bool()) { if (!( 1 <= v24 )) goto end; goto loc_10; } if (nondet_bool()) { if (!( 1+v24 <= 1 )) goto end; v25 = v24; v20 = 0; goto loc_5; } goto end; loc_23: end: ; }