From a5762a78e94dea0d02ba101692b68b847fa72195 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 30 Sep 2018 17:39:18 -0700 Subject: [PATCH] change to ast-vector Signed-off-by: Nikolaj Bjorner --- src/api/ml/z3.ml | 5 +++-- src/api/ml/z3.mli | 4 ++-- 2 files changed, 5 insertions(+), 4 deletions(-) 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