diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp
index 2768e97e3..d32bf8b4e 100644
--- a/src/api/api_interp.cpp
+++ b/src/api/api_interp.cpp
@@ -54,8 +54,8 @@ extern "C" {
 			    Z3_ast proof,
 			    int num,
 			    Z3_ast *cnsts,
-			    int *parents,
-			    Z3_interpolation_options options,
+			    unsigned *parents,
+			    Z3_params options,
 			    Z3_ast *interps,
 			    int num_theory,
 			    Z3_ast *theory
@@ -92,7 +92,7 @@ extern "C" {
 		       pre_parents_vec,
 		       interpolants,
 		       theory_vec,
-		       (interpolation_options) options);
+		       0); // ignore params for now FIXME
 
 	// copy result back
 	for(unsigned i = 0; i < interpolants.size(); i++)
@@ -104,8 +104,8 @@ extern "C" {
   Z3_lbool Z3_interpolate(Z3_context ctx,
 			  int num,
 			  Z3_ast *cnsts,
-			  int *parents,
-			  Z3_interpolation_options options,
+			  unsigned *parents,
+			  Z3_params options,
 			  Z3_ast *interps,
 			  Z3_model *model,
 			  Z3_literals *labels,
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 12db470fd..975b45940 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -7750,24 +7750,23 @@ END_MLAPI_EXCLUDE
     are considered to have global scope (i.e., may appear in any
     interpolant formula). 
 
-    def_API('Z3_interpolate', LBOOL, (_in(CONTEXT),), (_in(INT),), (_in_ptr(AST),),
-            (_in_ptr(INT),), (_in(PARAMS),), (_in_ptr(AST),),
-	    (_out(MODEL),), (_out(LITERALS),), (_in(BOOL),), (_in(INT),), (_in_ptr(AST,0),))
+    def_API('Z3_interpolate', INT, (_in(CONTEXT), _in(INT), _in_array(1,AST), _in_array(1,UINT), _in(PARAMS), _out_array(1,AST), _out(MODEL), _out(LITERALS),  _in(BOOL),  _in(INT), _in_array(9,AST),))
 
+   
   */  
 
 
-  Z3_lbool Z3_API Z3_interpolate(Z3_context ctx, 
-				 int num,
-				 Z3_ast *cnsts,
-				 int *parents,
-				 Z3_interpolation_options options,
-				 Z3_ast *interps,
-				 Z3_model *model = 0,
-				 Z3_literals *labels = 0,
-				 bool incremental = false,
-				 int num_theory = 0,
-				 Z3_ast *theory = 0);
+  Z3_lbool Z3_API Z3_interpolate(__in Z3_context ctx, 
+				 __in int num,
+				 __in_ecount(num) Z3_ast *cnsts,
+				 __in_ecount(num) unsigned *parents,
+				 __in Z3_params options,
+				 __out_ecount(num-1) Z3_ast *interps,
+				 __out Z3_model *model = 0,
+				 __out Z3_literals *labels = 0,
+				 __in bool incremental = false,
+				 __in int num_theory = 0,
+				 __in_ecount(num_theory) Z3_ast *theory = 0);
   
   /** Return a string summarizing cumulative time used for
       interpolation.  This string is purely for entertainment purposes