Function 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.