Function z3_sys::Z3_goal_assert

pub unsafe extern "C" fn Z3_goal_assert(
    c: Z3_context, 
    g: Z3_goal, 
    a: Z3_ast
)

Add a new formula a to the given goal. The formula is split according to the following procedure that is applied until a fixed-point: Conjunctions are split into separate formulas. Negations are distributed over disjunctions, resulting in separate formulas. If the goal is false, adding new formulas is a no-op. If the formula a is true, then nothing is added. If the formula a is false, then the entire goal is replaced by the formula false.