An error appears when running exist quantifier and fixedpoint Z3 in C#

I tried to use ctx.mkExist in the fixedpoint, howwever, it occurs error said "contains recursive predicate", I don't know why? and How to use ctx.MkExists in fixedpoint?For example: exist (lamda real) that lamb>=0 AND inv(c,i) AND phi(c+lamb,i) => phi(c，i)

        using (Context ctx = new Context())
        {
            var s = ctx.MkFixedpoint();

            IntSort B = ctx.IntSort;
            BoolSort T = ctx.BoolSort;
            RealSort R = ctx.RealSort;

            FuncDecl phi = ctx.MkFuncDecl("phi", new Sort[] { R,B }, T);
            s.RegisterRelation(phi);
            FuncDecl Inv = ctx.MkFuncDecl("inv", new Sort[] { R, B }, T);
            s.RegisterRelation(Inv);

            RealExpr c= (RealExpr)ctx.MkBound(0, R);
            IntExpr i = (IntExpr) ctx.MkBound(1, B);

            Expr[] InvArg=new Expr[2];
            InvArg[0] = ctx.MkConst("inv0" , Inv.Domain[0]);
            InvArg[1] = ctx.MkConst("inv1", Inv.Domain[1]);

            Expr invExpr = ctx.MkImplies(ctx.MkOr(
                 ctx.MkAnd(ctx.MkEq(InvArg[1], ctx.MkInt(0)), ctx.MkGe((RealExpr)InvArg[0], ctx.MkReal(0))),
                 ctx.MkAnd(ctx.MkEq(InvArg[1], ctx.MkInt(1)), ctx.MkGe((RealExpr)InvArg[0], ctx.MkReal(2)))
                 ),
              (BoolExpr)Inv[InvArg]);
            Quantifier invQ = ctx.MkForall(InvArg, invExpr, 1);
            s.AddRule(invQ);

            RealExpr[] lamb = new RealExpr[1];
            lamb[0] = ctx.MkRealConst("lamb");
            Expr existExpr = ctx.MkAnd(
                (BoolExpr)Inv[c,i],
                (BoolExpr)phi[ctx.MkAdd(c,lamb[0]),i],
                ctx.MkGe(lamb[0], ctx.MkReal(0)));
            BoolExpr t= ctx.MkExists(lamb, existExpr, 1);
            s.AddRule(ctx.MkImplies(t,(BoolExpr)phi[c,i]));
        }

sometimes, there is an error said "AccessViolationException was unhandlered,Attempted to read or write protected memory. This is often an indication that other memory is corrupt." when running to ctx.MkExists()

The fixedpoint solver only supports universal quantifiers at the top-level. You should rewrite the rule as follows:

        s.AddRule(ctx.MkForall(lamb, 
          ctx.MkImplies((BoolExpr)existExpr,(BoolExpr)phi[c,i])));

Z3 should ideally not result in any access violation. This is typically indicating a bug. I would really appreciate repros for such bugs when/if you encounter them.