Expr congruenceRoot(Expr a) { return _c._getExpr(_c._z3.solver_congruence_root( _solver, _c._createAST(a), )); }