assertExpr method

void assertExpr(
  1. AST a
)

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.

Implementation

void assertExpr(AST a) {
  _c._z3.goal_assert(_goal, _c._createAST(a));
}