diff --git a/bench/bench b/bench/bench
index 28ae69a210c7c8268262aca3ef8ca0e546c58c03..e637fd0092d0d4a08ffc2b76bb8cc2e371f63355 100755
--- a/bench/bench
+++ b/bench/bench
@@ -225,6 +225,18 @@ execute examples/vstte10_queens.mlw NQueens.test8
 echo ""
 
 
+echo "=== Extraction to Ocaml ==="
+extract_and_run examples/euler001 euler001.ml 1000000
+extract_and_run examples/gcd gcd.ml 6 15
+echo "TODO: update 4 more extraction examples"
+# extract_and_run examples/vstte10_max_sum vstte10_max_sum__*.ml
+# extract_and_run examples/vstte12_combinators vstte12_combinators__*.ml "((((K K) K) K) K)"
+# extract_and_run examples/sudoku sudoku__*.ml 2,0,9,0,0,0,0,1,0,0,0,0,0,6,0,0,0,0,0,5,3,8,0,2,7,0,0,3,0,0,0,0,0,0,0,0,0,0,0,0,7,5,0,0,3,0,4,1,2,0,8,9,0,0,0,0,4,0,9,0,0,2,0,8,0,0,0,0,1,0,0,5,0,0,0,0,0,0,0,7,6
+# extract_and_run examples/defunctionalization defunctionalization__*.ml
+echo ""
+
+
+
 echo "=== Checking good files ==="
 goods bench/typing/good
 goods bench/programs/good
@@ -244,15 +256,6 @@ goods examples/double_wp "-L examples/double_wp"
 goods examples/in_progress
 echo ""
 
-echo "=== Extraction to Ocaml ==="
-extract_and_run examples/euler001 euler001__*.ml 1000000
-extract_and_run examples/gcd gcd__*.ml 6 15
-extract_and_run examples/vstte10_max_sum vstte10_max_sum__*.ml
-extract_and_run examples/vstte12_combinators vstte12_combinators__*.ml "((((K K) K) K) K)"
-extract_and_run examples/sudoku sudoku__*.ml 2,0,9,0,0,0,0,1,0,0,0,0,0,6,0,0,0,0,0,5,3,8,0,2,7,0,0,3,0,0,0,0,0,0,0,0,0,0,0,0,7,5,0,0,3,0,4,1,2,0,8,9,0,0,0,0,4,0,9,0,0,2,0,8,0,0,0,0,1,0,0,5,0,0,0,0,0,0,0,7,6
-extract_and_run examples/defunctionalization defunctionalization__*.ml
-echo ""
-
 echo "=== Checking valid goals ==="
 valid_goals bench/valid
 echo ""
diff --git a/examples/TODO b/examples/TODO
index a7ba948ae548f8b2752edd235a5ae977811ee96e..203e12b0b61801ad5e820cf87e5dea4d64a13c5d 100644
--- a/examples/TODO
+++ b/examples/TODO
@@ -4,11 +4,9 @@ bignum.mlw
 counting_sort.mlw
 cursor.mlw
 dijkstra.mlw
-fibonacci.mlw
 find.mlw
 gcd.mlw
 hashtbl_impl.mlw
-ieee_float.mlw
 kmp.mlw
 knuth_prime_numbers.mlw
 koda_ruskey.mlw
diff --git a/examples/euler001/Makefile b/examples/euler001/Makefile
index 81379e271f460b944b50c52f8f6fd2a8e2bafec8..53da786aaa8e54efee956736c2b4629a11e4cb3a 100644
--- a/examples/euler001/Makefile
+++ b/examples/euler001/Makefile
@@ -20,7 +20,7 @@ ifeq ($(BENCH),yes)
 endif
 
 MAIN=main
-OBJ=euler001__Euler001
+OBJ=euler001
 
 ML  = $(addsuffix .ml, $(OBJ))
 CMO = $(addsuffix .cmo, $(OBJ))
@@ -45,7 +45,7 @@ $(MAIN).opt: $(CMX)  $(MAIN).cmx
 $(MAIN).cmx: $(CMX)
 
 $(ML): ../euler001.mlw
-	$(WHY3) extract -D ocaml32 ../euler001.mlw -o .
+	$(WHY3) extract -D ocaml64 $< -o $@
 
 %.cmx: %.ml
 	$(OCAMLOPT) $(INCLUDE) -annot -c $<
@@ -59,4 +59,3 @@ $(ML): ../euler001.mlw
 clean::
 	rm -f $(ML) *.cm[xio] *.o *.annot $(MAIN).opt $(MAIN).byte
 	rm -f why3__*.ml* euler001__*.ml* int__*.ml*
-
diff --git a/examples/euler001/main.ml b/examples/euler001/main.ml
index 9fd5195ef633114a49a71335e88a7c31d5d3b2e9..b714f44b349dada5ebe423e24a70d80339bf930c 100644
--- a/examples/euler001/main.ml
+++ b/examples/euler001/main.ml
@@ -11,11 +11,13 @@ let input =
   if Array.length Sys.argv <> 2 then usage ();
   Sys.argv.(1)
 
+(*
 let () =
   if input = "go" then begin
-    Euler001__Euler001.go ();
+    Euler001.go ();
     exit 0
   end
+*)
 
 let input_num =
   try
@@ -23,6 +25,6 @@ let input_num =
   with _ -> usage ()
 
 let () =
-  let a = Euler001__Euler001.solve input_num in
+  let a = Euler001.solve input_num in
   printf "The sum of all the multiples of 3 or 5 below %s is %s@."
     (Why3__BigInt.to_string input_num) (Why3__BigInt.to_string a)
diff --git a/examples/gcd.mlw b/examples/gcd.mlw
index 55da8366fa240109e1a745092fa7902493a2633d..3076ba609b6ededc0dbab9ceab989c2808cef869 100644
--- a/examples/gcd.mlw
+++ b/examples/gcd.mlw
@@ -93,6 +93,7 @@ end
     Note that we assume parameters u, v to be nonnegative.
     Otherwise, for u = v = min_int, the gcd could not be represented. *)
 
+(* does not work with extraction driver ocaml64
 module EuclideanAlgorithm31
 
   use import mach.int.Int31
@@ -109,3 +110,21 @@ module EuclideanAlgorithm31
       euclid v (u % v)
 
 end
+*)
+
+module EuclideanAlgorithm63
+
+  use import mach.int.Int63
+  use import number.Gcd
+
+  let rec euclid (u v: int63) : int63
+    variant  { to_int v }
+    requires { to_int u >= 0 /\ to_int v >= 0 }
+    ensures  { to_int result = gcd (to_int u) (to_int v) }
+  =
+    if Int63.eq v (of_int 0) then
+      u
+    else
+      euclid v (u % v)
+
+end
diff --git a/examples/gcd/Makefile b/examples/gcd/Makefile
index 4d4a104b0fdbae3389f554fb5736873605b9fe31..2d3b3da00841ec782c253398098705e97a81e805 100644
--- a/examples/gcd/Makefile
+++ b/examples/gcd/Makefile
@@ -20,7 +20,7 @@ ifeq ($(BENCH),yes)
 endif
 
 MAIN=main
-GEN=gcd__EuclideanAlgorithm31
+GEN=euclideanAlgorithm63
 OBJ=$(GEN)
 
 GENML = $(addsuffix .ml, $(GEN))
@@ -44,7 +44,7 @@ $(MAIN).opt: $(CMX)  $(MAIN).cmx
 $(MAIN).cmx: $(CMX)
 
 $(GENML): ../gcd.mlw
-	$(WHY3) extract -D ocaml32 $< -o .
+	$(WHY3) extract -D ocaml64 -L .. -o $@ gcd.EuclideanAlgorithm63
 
 %.cmx: %.ml
 	$(OCAMLOPT) $(INCLUDE) -annot -c $<
@@ -78,4 +78,3 @@ $(JSMAIN).byte: $(ML) jsmain.ml
 
 clean::
 	rm -f *.cm[io] $(NAME).byte $(NAME).js
-
diff --git a/examples/gcd/main.ml b/examples/gcd/main.ml
index 14fdcbdde32ac921841f2b52bce8bf385eacfbd0..c90b07635bf1e824c02c4133134821b8a4438e19 100644
--- a/examples/gcd/main.ml
+++ b/examples/gcd/main.ml
@@ -4,7 +4,7 @@ open Format
 
 let () =
   printf "%d@."
-    (Gcd__EuclideanAlgorithm31.euclid (int_of_string  Sys.argv.(1)) (int_of_string  Sys.argv.(2)))
+    (EuclideanAlgorithm63.euclid (int_of_string  Sys.argv.(1)) (int_of_string  Sys.argv.(2)))
 
 (*
 let usage () =