Function z3_sys::Z3_goal_to_dimacs_string

pub unsafe extern "C" fn Z3_goal_to_dimacs_string(
    c: Z3_context, 
    g: Z3_goal
) -> Z3_string

Convert a goal into a DIMACS formatted string. The goal must be in CNF. You can convert a goal to CNF by applying the tseitin-cnf tactic. Bit-vectors are not automatically converted to Booleans either, so the if caller intends to preserve satisfiability, it should apply bit-blasting tactics. Quantifiers and theory atoms will not be encoded.