void addConstraint(AST axiom, int level) { _c._z3.fixedpoint_add_constraint(_fp, _c._createAST(axiom), level); }