let rec jump_expansion_internal program n =
let labels = PolicyFront.create_label_map (Types.pi1 program) in
let rec aux res =
-prerr_endline "JEI_start";
+prerr_endline "JEI";
let { Types.fst = no_ch; Types.snd = z } = res in
match z with
| Types.None ->
(PolicyStep.jump_expansion_step program (Types.pi1 labels)
op))
in
+prerr_endline "JES";
+let init =(PolicyFront.jump_expansion_start program (Types.pi1 labels)) in
aux
{ Types.fst = Bool.False; Types.snd =
- (Types.pi1
- (PolicyFront.jump_expansion_start program (Types.pi1 labels))) }
+ (Types.pi1 init) }
(*
(match n with
| Nat.O ->
(Nat.S Nat.O)))))))))))))))) ppc x.Types.snd { Types.fst = Nat.O;
Types.snd = Assembly.Short_jump }).Types.fst
in
+(*prerr_endline "Z3";*)
Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
(Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
(Nat.S Nat.O)))))))))))))))) pc); Types.snd = (fun ppc ->