Function z3_sys::Z3_benchmark_to_smtlib_string[][src]

pub unsafe extern "C" fn Z3_benchmark_to_smtlib_string(
    c: Z3_context,
    name: Z3_string,
    logic: Z3_string,
    status: Z3_string,
    attributes: Z3_string,
    num_assumptions: c_uint,
    assumptions: *const Z3_ast,
    formula: Z3_ast
) -> Z3_string
Expand description

Convert the given benchmark into SMT-LIB formatted string.

Warning: The result buffer is statically allocated by Z3. It will be automatically deallocated when Z3_del_context is invoked. So, the buffer is invalidated in the next call to Z3_benchmark_to_smtlib_string.

  • c: - context.
  • name: - name of benchmark. The argument is optional.
  • logic: - the benchmark logic.
  • status: - the status string (sat, unsat, or unknown)
  • attributes: - other attributes, such as source, difficulty or category.
  • num_assumptions: - number of assumptions.
  • assumptions: - auxiliary assumptions.
  • formula: - formula to be checked for consistency in conjunction with assumptions.