Any significant increase in current levels of air traffic will need the support of efficient decision-aid tools. One of the tasks of air traffic management is to modify trajectories when necessary to maintain a sufficient separation between pairs of aircraft. Several algorithms have been developed to solve this problem, but the underlying assumptions are different, which makes it difficult to compare their performance. In this article, separation is maintained through changes of heading and velocity while minimizing a combination of fuel consumption and delay. For realistic trajectories, the speed is continuous with respect to time, the acceleration and turning rate are bounded, and the planned trajectories are recovered after the maneuvers. After describing the major modifications to existing models that are necessary to comply with this advanced definition of the problem, we compare three mixed integer linear programs. The first model is based on a discretization of the air space, and the second relies on a discretization of the time horizon. The third model implements a time decomposition of the problem; it allows only one initial maneuver, and it is solved periodically with a receding horizon to build a complete trajectory. The computational tests are conducted on a benchmark of artificial instances specifically built to include complex situations. Our analysis of the results highlights the strengths and limits of each model, and the time decomposition proves to be an excellent compromise.