OpenJML uses the AUFLIA logic by default. Some problems, e.g. using floating point or non-linear arithmetic need a different logic. The logic can be set on the command-line. But it would be more convenient for the user if the logic were chosen automatically. In SMT 1.5, it may be possible to simply use the ALL logic for the default.