Function z3_sys::Z3_parse_smtlib2_string

pub unsafe extern "C" fn Z3_parse_smtlib2_string(
    c: Z3_context, 
    str: Z3_string, 
    num_sorts: c_uint, 
    sort_names: *const Z3_symbol, 
    sorts: *const Z3_sort, 
    num_decls: c_uint, 
    decl_names: *const Z3_symbol, 
    decls: *const Z3_func_decl
) -> Z3_ast

Parse the given string using the SMT-LIB2 parser.

It returns a formula comprising of the conjunction of assertions in the scope (up to push/pop) at the end of the string.