diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index 25b437bc4..7415fc507 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -1815,8 +1815,9 @@ struct
     | _ -> UNKNOWN
 
   let get_model x =
-    let q = Z3native.solver_get_model (gc x) x in
-    if Z3native.is_null_model q then None else Some q
+  let q = Z3native.solver_get_model (gc x) x in
+    try if Z3native.is_null_model q then None else Some q with | _ -> None
+    
 
   let get_proof x =
     let q = Z3native.solver_get_proof (gc x) x in
diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index f67966a0f..18ade29bf 100644
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@@ -3407,10 +3407,10 @@ sig
   (** Parse the given string using the SMT-LIB2 parser.
 
       @return A conjunction of assertions in the scope (up to push/pop) at the end of the string. *)
-  val parse_smtlib2_string : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> Expr.expr
+  val parse_smtlib2_string : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> AST.ASTVector.ast_vector
 
   (** Parse the given file using the SMT-LIB2 parser. *)
-  val parse_smtlib2_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> Expr.expr
+  val parse_smtlib2_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> AST.ASTVector.ast_vector
 end