solver_assert method

void solver_assert(
  1. Z3_context c,
  2. Z3_solver s,
  3. Z3_ast a
)

\brief Assert a constraint into the solver.

The functions #Z3_solver_check and #Z3_solver_check_assumptions should be used to check whether the logical context is consistent or not.

\sa Z3_solver_assert_and_track \sa Z3_solver_reset

def_API('Z3_solver_assert', VOID, (_in(CONTEXT), _in(SOLVER), _in(AST)))

Implementation

void solver_assert(
  Z3_context c,
  Z3_solver s,
  Z3_ast a,
) {
  return _solver_assert(
    c,
    s,
    a,
  );
}