source: src/RTLabs/test/search.RTLabs.ma @ 1157

include "RTLabs/import.ma".
include "common/Animation.ma".




  definition id__div32u := ident_of_nat 0.
  definition lbl__div32u9 := 15.
  definition lbl__div32u8 := 14.
  definition lbl__div32u7 := 13.
  definition lbl__div32u6 := 12.
  definition lbl__div32u5 := 11.
  definition lbl__div32u4 := 10.
  definition lbl__div32u3 := 9.
  definition lbl__div32u2 := 8.
  definition lbl__div32u15 := 7.
  definition lbl__div32u14 := 6.
  definition lbl__div32u13 := 5.
  definition lbl__div32u12 := 4.
  definition lbl__div32u11 := 3.
  definition lbl__div32u10 := 2.
  definition lbl__div32u1 := 1.
  definition lbl__div32u0 := 0.
  definition C_cost0 := costlabel_of_nat 2.
  definition C_cost1 := costlabel_of_nat 1.
  definition C_cost2 := costlabel_of_nat 0.


  definition pre__div32u := mk_pre_internal_function
    (Some ? (pair ?? 4 (ASTint I32 Unsigned)))
    [(pair ?? 0 (ASTint I32 Unsigned)); (pair ?? 1 (ASTint I32 Unsigned))]
    [(pair ?? 2 (ASTint I32 Unsigned)); (pair ?? 3 (ASTint I32 Unsigned)); (pair ?? 4 (ASTint I32 Unsigned)); (pair ?? 5 (ASTint I32 Unsigned)); (pair ?? 6 (ASTint I32 Signed)); (pair ?? 7 (ASTint I32 Signed)); (pair ?? 8 (ASTint I32 Signed)); (pair ?? 9 (ASTint I8 Signed))]
    0
    [
    (pair ?? lbl__div32u9 (make_St_cond 7 lbl__div32u2 lbl__div32u8));
    (pair ?? lbl__div32u8 (make_St_cost C_cost0 lbl__div32u7));
    (pair ?? lbl__div32u7 (make_St_op2 Osub 3 3 1 lbl__div32u6));
    (pair ?? lbl__div32u6 (make_St_const 6 (Ointconst I32 (repr ? 1)) lbl__div32u5));
    (pair ?? lbl__div32u5 (make_St_op1 (Ocastint Signed I32) 5 6 lbl__div32u4));
    (pair ?? lbl__div32u4 (make_St_op2 Oadd 2 2 5 lbl__div32u3));
    (pair ?? lbl__div32u3 (make_St_skip lbl__div32u11));
    (pair ?? lbl__div32u2 (make_St_cost C_cost1 lbl__div32u1));
    (pair ?? lbl__div32u15 (make_St_cost C_cost2 lbl__div32u14));
    (pair ?? lbl__div32u14 (make_St_const 9 (Ointconst I8 (repr ? 0)) lbl__div32u13));
    (pair ?? lbl__div32u13 (make_St_op1 (Ocastint Signed I32) 2 9 lbl__div32u12));
    (pair ?? lbl__div32u12 (make_St_op1 Oid 3 0 lbl__div32u3));
    (pair ?? lbl__div32u11 (make_St_op2 (Ocmpu Cge) 8 3 1 lbl__div32u10));
    (pair ?? lbl__div32u10 (make_St_op1 Onotbool 7 8 lbl__div32u9));
    (pair ?? lbl__div32u1 (make_St_op1 Oid 4 2 lbl__div32u0));
    (pair ?? lbl__div32u0 (make_St_return))
]

    lbl__div32u15
    lbl__div32u0.

  definition id__div32s := ident_of_nat 1.
  definition lbl__div32s9 := 25.
  definition lbl__div32s8 := 24.
  definition lbl__div32s7 := 23.
  definition lbl__div32s6 := 22.
  definition lbl__div32s5 := 21.
  definition lbl__div32s4 := 20.
  definition lbl__div32s3 := 19.
  definition lbl__div32s25 := 18.
  definition lbl__div32s24 := 17.
  definition lbl__div32s23 := 16.
  definition lbl__div32s22 := 15.
  definition lbl__div32s21 := 14.
  definition lbl__div32s20 := 13.
  definition lbl__div32s2 := 12.
  definition lbl__div32s19 := 11.
  definition lbl__div32s18 := 10.
  definition lbl__div32s17 := 9.
  definition lbl__div32s16 := 8.
  definition lbl__div32s15 := 7.
  definition lbl__div32s14 := 6.
  definition lbl__div32s13 := 5.
  definition lbl__div32s12 := 4.
  definition lbl__div32s11 := 3.
  definition lbl__div32s10 := 2.
  definition lbl__div32s1 := 1.
  definition lbl__div32s0 := 0.
  definition C_cost3 := costlabel_of_nat 4.
  definition C_cost4 := costlabel_of_nat 3.
  definition C_cost7 := costlabel_of_nat 2.
  definition C_cost5 := costlabel_of_nat 1.
  definition C_cost6 := costlabel_of_nat 0.


  definition pre__div32s := mk_pre_internal_function
    (Some ? (pair ?? 7 (ASTint I32 Signed)))
    [(pair ?? 0 (ASTint I32 Signed)); (pair ?? 1 (ASTint I32 Signed))]
    [(pair ?? 2 (ASTint I32 Unsigned)); (pair ?? 3 (ASTint I32 Signed)); (pair ?? 4 (ASTint I32 Unsigned)); (pair ?? 5 (ASTint I32 Unsigned)); (pair ?? 6 (ASTint I32 Unsigned)); (pair ?? 7 (ASTint I32 Signed)); (pair ?? 8 (ASTint I32 Signed)); (pair ?? 9 (ASTint I32 Signed)); (pair ?? 10 (ASTint I32 Signed)); (pair ?? 11 (ASTint I32 Signed)); (pair ?? 12 (ASTint I32 Signed)); (pair ?? 13 (ASTint I32 Signed)); (pair ?? 14 (ASTint I32 Signed)); (pair ?? 15 (ASTint I8 Signed))]
    0
    [
    (pair ?? lbl__div32s9 (make_St_cost C_cost3 lbl__div32s8));
    (pair ?? lbl__div32s8 (make_St_op1 Onegint 9 1 lbl__div32s7));
    (pair ?? lbl__div32s7 (make_St_op1 (Ocastint Signed I32) 5 9 lbl__div32s6));
    (pair ?? lbl__div32s6 (make_St_op1 Onegint 3 3 lbl__div32s4));
    (pair ?? lbl__div32s5 (make_St_cost C_cost4 lbl__div32s4));
    (pair ?? lbl__div32s4 (make_St_call_id id__div32u [4; 5] (Some ? 6) lbl__div32s3));
    (pair ?? lbl__div32s3 (make_St_op1 Oid 2 6 lbl__div32s2));
    (pair ?? lbl__div32s25 (make_St_cost C_cost7 lbl__div32s24));
    (pair ?? lbl__div32s24 (make_St_op1 (Ocastint Signed I32) 4 0 lbl__div32s23));
    (pair ?? lbl__div32s23 (make_St_op1 (Ocastint Signed I32) 5 1 lbl__div32s22));
    (pair ?? lbl__div32s22 (make_St_const 15 (Ointconst I8 (repr ? 1)) lbl__div32s21));
    (pair ?? lbl__div32s21 (make_St_op1 (Ocastint Signed I32) 3 15 lbl__div32s20));
    (pair ?? lbl__div32s20 (make_St_const 14 (Ointconst I32 (repr ? 0)) lbl__div32s19));
    (pair ?? lbl__div32s2 (make_St_op1 (Ocastint Unsigned I32) 8 2 lbl__div32s1));
    (pair ?? lbl__div32s19 (make_St_op2 (Ocmp Clt) 13 0 14 lbl__div32s18));
    (pair ?? lbl__div32s18 (make_St_cond 13 lbl__div32s17 lbl__div32s13));
    (pair ?? lbl__div32s17 (make_St_cost C_cost5 lbl__div32s16));
    (pair ?? lbl__div32s16 (make_St_op1 Onegint 12 0 lbl__div32s15));
    (pair ?? lbl__div32s15 (make_St_op1 (Ocastint Signed I32) 4 12 lbl__div32s14));
    (pair ?? lbl__div32s14 (make_St_op1 Onegint 3 3 lbl__div32s12));
    (pair ?? lbl__div32s13 (make_St_cost C_cost6 lbl__div32s12));
    (pair ?? lbl__div32s12 (make_St_const 11 (Ointconst I32 (repr ? 0)) lbl__div32s11));
    (pair ?? lbl__div32s11 (make_St_op2 (Ocmp Clt) 10 1 11 lbl__div32s10));
    (pair ?? lbl__div32s10 (make_St_cond 10 lbl__div32s9 lbl__div32s5));
    (pair ?? lbl__div32s1 (make_St_op2 Omul 7 3 8 lbl__div32s0));
    (pair ?? lbl__div32s0 (make_St_return))
]

    lbl__div32s25
    lbl__div32s0.

  definition id_search := ident_of_nat 2.
  definition lbl_search9 := 65.
  definition lbl_search8 := 64.
  definition lbl_search7 := 63.
  definition lbl_search65 := 62.
  definition lbl_search64 := 61.
  definition lbl_search63 := 60.
  definition lbl_search62 := 59.
  definition lbl_search61 := 58.
  definition lbl_search60 := 57.
  definition lbl_search6 := 56.
  definition lbl_search59 := 55.
  definition lbl_search58 := 54.
  definition lbl_search57 := 53.
  definition lbl_search56 := 52.
  definition lbl_search55 := 51.
  definition lbl_search54 := 50.
  definition lbl_search53 := 49.
  definition lbl_search52 := 48.
  definition lbl_search51 := 47.
  definition lbl_search50 := 46.
  definition lbl_search5 := 45.
  definition lbl_search49 := 44.
  definition lbl_search48 := 43.
  definition lbl_search47 := 42.
  definition lbl_search46 := 41.
  definition lbl_search45 := 40.
  definition lbl_search44 := 39.
  definition lbl_search43 := 38.
  definition lbl_search42 := 37.
  definition lbl_search41 := 36.
  definition lbl_search40 := 35.
  definition lbl_search4 := 34.
  definition lbl_search39 := 33.
  definition lbl_search38 := 32.
  definition lbl_search37 := 31.
  definition lbl_search36 := 30.
  definition lbl_search35 := 29.
  definition lbl_search34 := 28.
  definition lbl_search33 := 27.
  definition lbl_search32 := 26.
  definition lbl_search31 := 25.
  definition lbl_search30 := 24.
  definition lbl_search3 := 23.
  definition lbl_search29 := 22.
  definition lbl_search28 := 21.
  definition lbl_search27 := 20.
  definition lbl_search26 := 19.
  definition lbl_search25 := 18.
  definition lbl_search24 := 17.
  definition lbl_search23 := 16.
  definition lbl_search22 := 15.
  definition lbl_search21 := 14.
  definition lbl_search20 := 13.
  definition lbl_search2 := 12.
  definition lbl_search19 := 11.
  definition lbl_search18 := 10.
  definition lbl_search17 := 9.
  definition lbl_search16 := 8.
  definition lbl_search15 := 7.
  definition lbl_search14 := 6.
  definition lbl_search13 := 5.
  definition lbl_search12 := 4.
  definition lbl_search11 := 3.
  definition lbl_search10 := 2.
  definition lbl_search1 := 1.
  definition lbl_search0 := 0.
  definition C_cost16 := costlabel_of_nat 8.
  definition C_cost9 := costlabel_of_nat 7.
  definition C_cost14 := costlabel_of_nat 6.
  definition C_cost15 := costlabel_of_nat 5.
  definition C_cost12 := costlabel_of_nat 4.
  definition C_cost13 := costlabel_of_nat 3.
  definition C_cost10 := costlabel_of_nat 2.
  definition C_cost11 := costlabel_of_nat 1.
  definition C_cost8 := costlabel_of_nat 0.


  definition pre_search := mk_pre_internal_function
    (Some ? (pair ?? 8 (ASTint I8 Unsigned)))
    [(pair ?? 0 (ASTptr Any)); (pair ?? 1 (ASTint I8 Unsigned)); (pair ?? 2 (ASTint I8 Unsigned))]
    [(pair ?? 3 (ASTint I32 Signed)); (pair ?? 4 (ASTint I8 Unsigned)); (pair ?? 5 (ASTint I8 Unsigned)); (pair ?? 6 (ASTint I8 Unsigned)); (pair ?? 7 (ASTint I32 Signed)); (pair ?? 8 (ASTint I8 Unsigned)); (pair ?? 9 (ASTint I32 Signed)); (pair ?? 10 (ASTint I32 Signed)); (pair ?? 11 (ASTint I32 Signed)); (pair ?? 12 (ASTint I32 Signed)); (pair ?? 13 (ASTint I32 Signed)); (pair ?? 14 (ASTint I32 Signed)); (pair ?? 15 (ASTint I32 Signed)); (pair ?? 16 (ASTint I32 Signed)); (pair ?? 17 (ASTint I8 Unsigned)); (pair ?? 18 (ASTptr Any)); (pair ?? 19 (ASTint I8 Unsigned)); (pair ?? 20 (ASTint I8 Unsigned)); (pair ?? 21 (ASTint I32 Signed)); (pair ?? 22 (ASTint I32 Signed)); (pair ?? 23 (ASTint I32 Signed)); (pair ?? 24 (ASTint I32 Signed)); (pair ?? 25 (ASTint I32 Signed)); (pair ?? 26 (ASTint I32 Signed)); (pair ?? 27 (ASTint I8 Unsigned)); (pair ?? 28 (ASTptr Any)); (pair ?? 29 (ASTint I8 Unsigned)); (pair ?? 30 (ASTint I8 Unsigned)); (pair ?? 31 (ASTint I32 Signed)); (pair ?? 32 (ASTint I32 Signed)); (pair ?? 33 (ASTint I32 Signed)); (pair ?? 34 (ASTint I8 Unsigned)); (pair ?? 35 (ASTptr Any)); (pair ?? 36 (ASTint I8 Unsigned)); (pair ?? 37 (ASTint I8 Unsigned)); (pair ?? 38 (ASTint I32 Signed)); (pair ?? 39 (ASTint I32 Signed)); (pair ?? 40 (ASTint I8 Signed)); (pair ?? 41 (ASTint I32 Signed)); (pair ?? 42 (ASTint I32 Signed)); (pair ?? 43 (ASTint I32 Signed)); (pair ?? 44 (ASTint I32 Signed)); (pair ?? 45 (ASTint I32 Signed)); (pair ?? 46 (ASTint I32 Signed)); (pair ?? 47 (ASTint I32 Signed)); (pair ?? 48 (ASTint I32 Signed)); (pair ?? 49 (ASTint I32 Signed)); (pair ?? 50 (ASTint I8 Signed))]
    0
    [
    (pair ?? lbl_search9 (make_St_const 13 (Ointconst I32 (repr ? 1)) lbl_search8));
    (pair ?? lbl_search8 (make_St_op2 Oadd 11 12 13 lbl_search7));
    (pair ?? lbl_search7 (make_St_op1 (Ocastint Signed I8) 6 11 lbl_search5));
    (pair ?? lbl_search65 (make_St_cost C_cost16 lbl_search64));
    (pair ?? lbl_search64 (make_St_const 50 (Ointconst I8 (repr ? 0)) lbl_search63));
    (pair ?? lbl_search63 (make_St_op1 (Ocastint Signed I8) 6 50 lbl_search62));
    (pair ?? lbl_search62 (make_St_op1 (Ocastint Unsigned I32) 48 1 lbl_search61));
    (pair ?? lbl_search61 (make_St_const 49 (Ointconst I32 (repr ? 1)) lbl_search60));
    (pair ?? lbl_search60 (make_St_op2 Osub 47 48 49 lbl_search59));
    (pair ?? lbl_search6 (make_St_cost C_cost9 lbl_search5));
    (pair ?? lbl_search59 (make_St_op1 (Ocastint Signed I8) 4 47 lbl_search5));
    (pair ?? lbl_search58 (make_St_op1 (Ocastint Unsigned I32) 45 4 lbl_search57));
    (pair ?? lbl_search57 (make_St_op1 (Ocastint Unsigned I32) 46 6 lbl_search56));
    (pair ?? lbl_search56 (make_St_op2 (Ocmp Cge) 44 45 46 lbl_search55));
    (pair ?? lbl_search55 (make_St_op1 Onotbool 43 44 lbl_search54));
    (pair ?? lbl_search54 (make_St_cond 43 lbl_search4 lbl_search53));
    (pair ?? lbl_search53 (make_St_cost C_cost14 lbl_search52));
    (pair ?? lbl_search52 (make_St_op1 (Ocastint Unsigned I32) 41 4 lbl_search51));
    (pair ?? lbl_search51 (make_St_op1 (Ocastint Unsigned I32) 42 6 lbl_search50));
    (pair ?? lbl_search50 (make_St_op2 Oadd 38 41 42 lbl_search49));
    (pair ?? lbl_search5 (make_St_skip lbl_search58));
    (pair ?? lbl_search49 (make_St_const 40 (Ointconst I8 (repr ? 2)) lbl_search48));
    (pair ?? lbl_search48 (make_St_op1 (Ocastint Signed I32) 39 40 lbl_search47));
    (pair ?? lbl_search47 (make_St_call_id id__div32s [38; 39] (Some ? 7) lbl_search46));
    (pair ?? lbl_search46 (make_St_op1 Oid 3 7 lbl_search45));
    (pair ?? lbl_search45 (make_St_op1 (Ocastint Signed I8) 5 3 lbl_search44));
    (pair ?? lbl_search44 (make_St_const 37 (Ointconst I8 (repr ? 1)) lbl_search43));
    (pair ?? lbl_search43 (make_St_op2 Omul 36 5 37 lbl_search42));
    (pair ?? lbl_search42 (make_St_op2 Oaddp 35 0 36 lbl_search41));
    (pair ?? lbl_search41 (make_St_load Mint8unsigned 35 34 lbl_search40));
    (pair ?? lbl_search40 (make_St_op1 (Ocastint Unsigned I32) 32 34 lbl_search39));
    (pair ?? lbl_search4 (make_St_cost C_cost15 lbl_search3));
    (pair ?? lbl_search39 (make_St_op1 (Ocastint Unsigned I32) 33 2 lbl_search38));
    (pair ?? lbl_search38 (make_St_op2 (Ocmp Ceq) 31 32 33 lbl_search37));
    (pair ?? lbl_search37 (make_St_cond 31 lbl_search36 lbl_search34));
    (pair ?? lbl_search36 (make_St_cost C_cost12 lbl_search35));
    (pair ?? lbl_search35 (make_St_op1 Oid 8 5 lbl_search0));
    (pair ?? lbl_search34 (make_St_cost C_cost13 lbl_search33));
    (pair ?? lbl_search33 (make_St_const 30 (Ointconst I8 (repr ? 1)) lbl_search32));
    (pair ?? lbl_search32 (make_St_op2 Omul 29 5 30 lbl_search31));
    (pair ?? lbl_search31 (make_St_op2 Oaddp 28 0 29 lbl_search30));
    (pair ?? lbl_search30 (make_St_load Mint8unsigned 28 27 lbl_search29));
    (pair ?? lbl_search3 (make_St_const 10 (Ointconst I32 (repr ? 1)) lbl_search2));
    (pair ?? lbl_search29 (make_St_op1 (Ocastint Unsigned I32) 25 27 lbl_search28));
    (pair ?? lbl_search28 (make_St_op1 (Ocastint Unsigned I32) 26 2 lbl_search27));
    (pair ?? lbl_search27 (make_St_op2 (Ocmp Cgt) 24 25 26 lbl_search26));
    (pair ?? lbl_search26 (make_St_cond 24 lbl_search25 lbl_search20));
    (pair ?? lbl_search25 (make_St_cost C_cost10 lbl_search24));
    (pair ?? lbl_search24 (make_St_op1 (Ocastint Unsigned I32) 22 5 lbl_search23));
    (pair ?? lbl_search23 (make_St_const 23 (Ointconst I32 (repr ? 1)) lbl_search22));
    (pair ?? lbl_search22 (make_St_op2 Osub 21 22 23 lbl_search21));
    (pair ?? lbl_search21 (make_St_op1 (Ocastint Signed I8) 4 21 lbl_search19));
    (pair ?? lbl_search20 (make_St_cost C_cost11 lbl_search19));
    (pair ?? lbl_search2 (make_St_op1 Onegint 9 10 lbl_search1));
    (pair ?? lbl_search19 (make_St_const 20 (Ointconst I8 (repr ? 1)) lbl_search18));
    (pair ?? lbl_search18 (make_St_op2 Omul 19 5 20 lbl_search17));
    (pair ?? lbl_search17 (make_St_op2 Oaddp 18 0 19 lbl_search16));
    (pair ?? lbl_search16 (make_St_load Mint8unsigned 18 17 lbl_search15));
    (pair ?? lbl_search15 (make_St_op1 (Ocastint Unsigned I32) 15 17 lbl_search14));
    (pair ?? lbl_search14 (make_St_op1 (Ocastint Unsigned I32) 16 2 lbl_search13));
    (pair ?? lbl_search13 (make_St_op2 (Ocmp Clt) 14 15 16 lbl_search12));
    (pair ?? lbl_search12 (make_St_cond 14 lbl_search11 lbl_search6));
    (pair ?? lbl_search11 (make_St_cost C_cost8 lbl_search10));
    (pair ?? lbl_search10 (make_St_op1 (Ocastint Unsigned I32) 12 5 lbl_search9));
    (pair ?? lbl_search1 (make_St_op1 (Ocastint Signed I8) 8 9 lbl_search0));
    (pair ?? lbl_search0 (make_St_return))
]

    lbl_search65
    lbl_search0.

  definition id_main := ident_of_nat 3.
  definition lbl_main9 := 61.
  definition lbl_main8 := 60.
  definition lbl_main7 := 59.
  definition lbl_main61 := 58.
  definition lbl_main60 := 57.
  definition lbl_main6 := 56.
  definition lbl_main59 := 55.
  definition lbl_main58 := 54.
  definition lbl_main57 := 53.
  definition lbl_main56 := 52.
  definition lbl_main55 := 51.
  definition lbl_main54 := 50.
  definition lbl_main53 := 49.
  definition lbl_main52 := 48.
  definition lbl_main51 := 47.
  definition lbl_main50 := 46.
  definition lbl_main5 := 45.
  definition lbl_main49 := 44.
  definition lbl_main48 := 43.
  definition lbl_main47 := 42.
  definition lbl_main46 := 41.
  definition lbl_main45 := 40.
  definition lbl_main44 := 39.
  definition lbl_main43 := 38.
  definition lbl_main42 := 37.
  definition lbl_main41 := 36.
  definition lbl_main40 := 35.
  definition lbl_main4 := 34.
  definition lbl_main39 := 33.
  definition lbl_main38 := 32.
  definition lbl_main37 := 31.
  definition lbl_main36 := 30.
  definition lbl_main35 := 29.
  definition lbl_main34 := 28.
  definition lbl_main33 := 27.
  definition lbl_main32 := 26.
  definition lbl_main31 := 25.
  definition lbl_main30 := 24.
  definition lbl_main3 := 23.
  definition lbl_main29 := 22.
  definition lbl_main28 := 21.
  definition lbl_main27 := 20.
  definition lbl_main26 := 19.
  definition lbl_main25 := 18.
  definition lbl_main24 := 17.
  definition lbl_main23 := 16.
  definition lbl_main22 := 15.
  definition lbl_main21 := 14.
  definition lbl_main20 := 13.
  definition lbl_main2 := 12.
  definition lbl_main19 := 11.
  definition lbl_main18 := 10.
  definition lbl_main17 := 9.
  definition lbl_main16 := 8.
  definition lbl_main15 := 7.
  definition lbl_main14 := 6.
  definition lbl_main13 := 5.
  definition lbl_main12 := 4.
  definition lbl_main11 := 3.
  definition lbl_main10 := 2.
  definition lbl_main1 := 1.
  definition lbl_main0 := 0.
  definition C_cost17 := costlabel_of_nat 0.


  definition pre_main := mk_pre_internal_function
    (Some ? (pair ?? 2 (ASTint I32 Signed)))
    []
    [(pair ?? 0 (ASTint I8 Unsigned)); (pair ?? 1 (ASTint I8 Unsigned)); (pair ?? 2 (ASTint I32 Signed)); (pair ?? 3 (ASTptr Any)); (pair ?? 4 (ASTint I8 Unsigned)); (pair ?? 5 (ASTint I8 Unsigned)); (pair ?? 6 (ASTint I8 Signed)); (pair ?? 7 (ASTint I8 Signed)); (pair ?? 8 (ASTptr Any)); (pair ?? 9 (ASTint I32 Unsigned)); (pair ?? 10 (ASTptr Any)); (pair ?? 11 (ASTint I8 Unsigned)); (pair ?? 12 (ASTint I8 Signed)); (pair ?? 13 (ASTptr Any)); (pair ?? 14 (ASTint I32 Signed)); (pair ?? 15 (ASTint I32 Signed)); (pair ?? 16 (ASTint I32 Signed)); (pair ?? 17 (ASTptr Any)); (pair ?? 18 (ASTint I32 Unsigned)); (pair ?? 19 (ASTptr Any)); (pair ?? 20 (ASTint I8 Unsigned)); (pair ?? 21 (ASTint I8 Signed)); (pair ?? 22 (ASTptr Any)); (pair ?? 23 (ASTint I32 Signed)); (pair ?? 24 (ASTint I32 Signed)); (pair ?? 25 (ASTint I32 Signed)); (pair ?? 26 (ASTptr Any)); (pair ?? 27 (ASTint I32 Unsigned)); (pair ?? 28 (ASTptr Any)); (pair ?? 29 (ASTint I8 Unsigned)); (pair ?? 30 (ASTint I8 Signed)); (pair ?? 31 (ASTptr Any)); (pair ?? 32 (ASTint I32 Signed)); (pair ?? 33 (ASTint I32 Signed)); (pair ?? 34 (ASTint I32 Signed)); (pair ?? 35 (ASTptr Any)); (pair ?? 36 (ASTint I32 Unsigned)); (pair ?? 37 (ASTptr Any)); (pair ?? 38 (ASTint I8 Unsigned)); (pair ?? 39 (ASTint I8 Signed)); (pair ?? 40 (ASTptr Any)); (pair ?? 41 (ASTint I32 Signed)); (pair ?? 42 (ASTint I32 Signed)); (pair ?? 43 (ASTint I32 Signed)); (pair ?? 44 (ASTptr Any)); (pair ?? 45 (ASTint I32 Unsigned)); (pair ?? 46 (ASTptr Any)); (pair ?? 47 (ASTint I8 Unsigned)); (pair ?? 48 (ASTint I8 Signed)); (pair ?? 49 (ASTptr Any)); (pair ?? 50 (ASTint I32 Signed)); (pair ?? 51 (ASTint I32 Signed)); (pair ?? 52 (ASTint I32 Signed)); (pair ?? 53 (ASTptr Any)); (pair ?? 54 (ASTint I32 Unsigned))]
    5
    [
    (pair ?? lbl_main9 (make_St_const 9 (Ointconst I32 (repr ? 0)) lbl_main8));
    (pair ?? lbl_main8 (make_St_op2 Oaddp 3 8 9 lbl_main7));
    (pair ?? lbl_main7 (make_St_const 7 (Ointconst I8 (repr ? 5)) lbl_main6));
    (pair ?? lbl_main61 (make_St_cost C_cost17 lbl_main60));
    (pair ?? lbl_main60 (make_St_const 53 (Oaddrstack 0) lbl_main59));
    (pair ?? lbl_main6 (make_St_op1 (Ocastint Signed I8) 4 7 lbl_main5));
    (pair ?? lbl_main59 (make_St_const 54 (Ointconst I32 (repr ? 0)) lbl_main58));
    (pair ?? lbl_main58 (make_St_op2 Oaddp 49 53 54 lbl_main57));
    (pair ?? lbl_main57 (make_St_const 51 (Ointconst I32 (repr ? 0)) lbl_main56));
    (pair ?? lbl_main56 (make_St_const 52 (Ointconst I32 (repr ? 1)) lbl_main55));
    (pair ?? lbl_main55 (make_St_op2 Omul 50 51 52 lbl_main54));
    (pair ?? lbl_main54 (make_St_op2 Oaddp 46 49 50 lbl_main53));
    (pair ?? lbl_main53 (make_St_const 48 (Ointconst I8 (repr ? 0)) lbl_main52));
    (pair ?? lbl_main52 (make_St_op1 (Ocastint Signed I8) 47 48 lbl_main51));
    (pair ?? lbl_main51 (make_St_store Mint8unsigned 46 47 lbl_main50));
    (pair ?? lbl_main50 (make_St_const 44 (Oaddrstack 0) lbl_main49));
    (pair ?? lbl_main5 (make_St_const 6 (Ointconst I8 (repr ? 57)) lbl_main4));
    (pair ?? lbl_main49 (make_St_const 45 (Ointconst I32 (repr ? 0)) lbl_main48));
    (pair ?? lbl_main48 (make_St_op2 Oaddp 40 44 45 lbl_main47));
    (pair ?? lbl_main47 (make_St_const 42 (Ointconst I32 (repr ? 1)) lbl_main46));
    (pair ?? lbl_main46 (make_St_const 43 (Ointconst I32 (repr ? 1)) lbl_main45));
    (pair ?? lbl_main45 (make_St_op2 Omul 41 42 43 lbl_main44));
    (pair ?? lbl_main44 (make_St_op2 Oaddp 37 40 41 lbl_main43));
    (pair ?? lbl_main43 (make_St_const 39 (Ointconst I8 (repr ? 18)) lbl_main42));
    (pair ?? lbl_main42 (make_St_op1 (Ocastint Signed I8) 38 39 lbl_main41));
    (pair ?? lbl_main41 (make_St_store Mint8unsigned 37 38 lbl_main40));
    (pair ?? lbl_main40 (make_St_const 35 (Oaddrstack 0) lbl_main39));
    (pair ?? lbl_main4 (make_St_op1 (Ocastint Signed I8) 5 6 lbl_main3));
    (pair ?? lbl_main39 (make_St_const 36 (Ointconst I32 (repr ? 0)) lbl_main38));
    (pair ?? lbl_main38 (make_St_op2 Oaddp 31 35 36 lbl_main37));
    (pair ?? lbl_main37 (make_St_const 33 (Ointconst I32 (repr ? 2)) lbl_main36));
    (pair ?? lbl_main36 (make_St_const 34 (Ointconst I32 (repr ? 1)) lbl_main35));
    (pair ?? lbl_main35 (make_St_op2 Omul 32 33 34 lbl_main34));
    (pair ?? lbl_main34 (make_St_op2 Oaddp 28 31 32 lbl_main33));
    (pair ?? lbl_main33 (make_St_const 30 (Ointconst I8 (repr ? 23)) lbl_main32));
    (pair ?? lbl_main32 (make_St_op1 (Ocastint Signed I8) 29 30 lbl_main31));
    (pair ?? lbl_main31 (make_St_store Mint8unsigned 28 29 lbl_main30));
    (pair ?? lbl_main30 (make_St_const 26 (Oaddrstack 0) lbl_main29));
    (pair ?? lbl_main3 (make_St_call_id id_search [3; 4; 5] (Some ? 1) lbl_main2));
    (pair ?? lbl_main29 (make_St_const 27 (Ointconst I32 (repr ? 0)) lbl_main28));
    (pair ?? lbl_main28 (make_St_op2 Oaddp 22 26 27 lbl_main27));
    (pair ?? lbl_main27 (make_St_const 24 (Ointconst I32 (repr ? 3)) lbl_main26));
    (pair ?? lbl_main26 (make_St_const 25 (Ointconst I32 (repr ? 1)) lbl_main25));
    (pair ?? lbl_main25 (make_St_op2 Omul 23 24 25 lbl_main24));
    (pair ?? lbl_main24 (make_St_op2 Oaddp 19 22 23 lbl_main23));
    (pair ?? lbl_main23 (make_St_const 21 (Ointconst I8 (repr ? 57)) lbl_main22));
    (pair ?? lbl_main22 (make_St_op1 (Ocastint Signed I8) 20 21 lbl_main21));
    (pair ?? lbl_main21 (make_St_store Mint8unsigned 19 20 lbl_main20));
    (pair ?? lbl_main20 (make_St_const 17 (Oaddrstack 0) lbl_main19));
    (pair ?? lbl_main2 (make_St_op1 Oid 0 1 lbl_main1));
    (pair ?? lbl_main19 (make_St_const 18 (Ointconst I32 (repr ? 0)) lbl_main18));
    (pair ?? lbl_main18 (make_St_op2 Oaddp 13 17 18 lbl_main17));
    (pair ?? lbl_main17 (make_St_const 15 (Ointconst I32 (repr ? 4)) lbl_main16));
    (pair ?? lbl_main16 (make_St_const 16 (Ointconst I32 (repr ? 1)) lbl_main15));
    (pair ?? lbl_main15 (make_St_op2 Omul 14 15 16 lbl_main14));
    (pair ?? lbl_main14 (make_St_op2 Oaddp 10 13 14 lbl_main13));
    (pair ?? lbl_main13 (make_St_const 12 (Ointconst I8 (repr ? 120)) lbl_main12));
    (pair ?? lbl_main12 (make_St_op1 (Ocastint Signed I8) 11 12 lbl_main11));
    (pair ?? lbl_main11 (make_St_store Mint8unsigned 10 11 lbl_main10));
    (pair ?? lbl_main10 (make_St_const 8 (Oaddrstack 0) lbl_main9));
    (pair ?? lbl_main1 (make_St_op1 (Ocastint Unsigned I32) 2 0 lbl_main0));
    (pair ?? lbl_main0 (make_St_return))
]

    lbl_main61
    lbl_main0.



definition prog : res RTLabs_program :=
  do f_main \larr make_internal_function pre_main;
  do f_search \larr make_internal_function pre_search;
  do f__div32s \larr make_internal_function pre__div32s;
  do f__div32u \larr make_internal_function pre__div32u;

OK ? (mk_program ??
(  (pair ?? id_main f_main)::
  (pair ?? id_search f_search)::
  (pair ?? id__div32s f__div32s)::
  (pair ?? id__div32u f__div32u)::
(nil ?))
  id_main
  (*globals:*)
  []
).

   example exec: finishes_with (repr I32 3) ? (do p ← prog; do r ← exec_up_to RTLabs_fullexec p 1000 [ ]; OK ? r).
   normalize  (* you can examine the result here *)
   @refl qed.