mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-12-18 12:20:53 -08:00
commit 94d1695b01
3 changed files with 7 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/ml/z3.mli
View file

@ -3443,12 +3443,10 @@ sig
(** Parse the given string using the SMT-LIB2 parser.
{!parse_smtlib_string}
@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
(** Parse the given file using the SMT-LIB2 parser.
{!parse_smtlib2_string} *)
(** 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
end

2
src/api/z3_api.h
View file

@ -1331,7 +1331,7 @@ typedef enum {
- Z3_IOB: Index out of bounds.
- Z3_INVALID_ARG: Invalid argument was provided.
- Z3_PARSER_ERROR: An error occurred when parsing a string or file.
- Z3_NO_PARSER: Parser output is not available, that is, user didn't invoke #Z3_parse_smtlib_string or #Z3_parse_smtlib_file.
- Z3_NO_PARSER: Parser output is not available, that is, user didn't invoke #Z3_parse_smtlib2_string or #Z3_parse_smtlib2_file.
- Z3_INVALID_PATTERN: Invalid pattern was used to build a quantifier.
- Z3_MEMOUT_FAIL: A memory allocation failure was encountered.
- Z3_FILE_ACCESS_ERRROR: A file could not be accessed.