Expr congruenceNext(Expr a) { return _c._getExpr(_c._z3.solver_congruence_next( _solver, _c._createAST(a), )); }