diff --git a/test-suite/output/Extraction_ffi.ouf b/test-suite/output/Extraction_ffi.out
similarity index 61%
rename from test-suite/output/Extraction_ffi.ouf
rename to test-suite/output/Extraction_ffi.out
index a625bdc5d1e7a..b7f22c4f2372f 100644
--- a/test-suite/output/Extraction_ffi.ouf
+++ b/test-suite/output/Extraction_ffi.out
@@ -5,14 +5,14 @@ external ax_fun: nat -> nat = "my_c_fun"
 (** val exact_fun : nat -> nat **)
 
 let exact_fun a =
-  add a (S O)
+  add (ax_fun a) (S O)
 (** User defined extraction *)
 (** val exact_fun : nat -> nat **)
 
 external exact_fun: nat -> nat = "my_exact_c_fun"
-(** User defined extraction *)
-(** val exact_fun : nat -> nat **)
+(** val exact_fun2 : nat -> nat **)
 
-let exact_fun = my_exact_c_fun
+let exact_fun2 a =
+  add (ax_fun a) (S O)
 
-let _ = Stdlib.Callback.register "call_exact_fun" exact_fun
+let _ = Stdlib.Callback.register "call_exact_fun" exact_fun2
diff --git a/test-suite/output/Extraction_ffi.v b/test-suite/output/Extraction_ffi.v
index 4584b3533d39c..68b8eaa735d6f 100644
--- a/test-suite/output/Extraction_ffi.v
+++ b/test-suite/output/Extraction_ffi.v
@@ -5,21 +5,23 @@ From Coq Require Extraction.
 (* Define an axiomatic function. *)
 Axiom ax_fun : nat -> nat.
 
-(* Define a fully specified function *)
-Definition exact_fun (a : nat) := a + 1.
+(* Define a fully specified function*)
+Definition exact_fun (a : nat) := (ax_fun a) + 1.
+
+(* Define duplicate of the fully specified function*)
+Definition exact_fun2 (a : nat) := (ax_fun a) + 1.
 
 (* ax_fun shall be a FFI call to the C function my_c_fun *)
 Extract Foreign Constant ax_fun => "my_c_fun".
 Extraction ax_fun.
 
-(* Extract the defined exact_fun *)
+(* Extract exact_fun *)
 Extraction exact_fun.
 
 (* exact_fun shall now be a FFI call to the C function my_c_fun *)
 Extract Foreign Constant exact_fun => "my_exact_c_fun".
 Extraction exact_fun.
 
-(* Now, exact_fun is an entry point exposed to C *)
-Reset Extraction Foreign.
-Extract Callback "call_exact_fun" exact_fun.
-Extraction exact_fun.
\ No newline at end of file
+(* Now, exact_fun is an entry point exposed to C. *)
+Extract Callback "call_exact_fun" exact_fun2.
+Extraction exact_fun2.