solver.add( // Maximum cycle start constraint
                    ctx.mkLe(
                        port.getCycle().getFirstCycleStartZ3(),
                        this.arrivalTime(ctx, 0, frag)
                    )
                );
                solver.add( // No negative cycle values constraint
                    ctx.mkGe(port.getCycle().getFirstCycleStartZ3(), ctx.mkInt(0))
                );