That is about right. What happens at -O4 is that for every variable, the upper and lower bounds are tested, and if using the bound as the value for the variable would make the problem unsolvable, then that bound is discarded. For some problems, this can be very useful and reduce the time to find a solution significantly. For other problems, it might not find any value to remove, or the values removed might not help solution times at all. The -O5 level is the same, but instead of just testing boundary values for immediate failure, all values in the domain are tested.
As a side note, while MiniZinc uses Gecode for the optimization this is not actually anything special built-in to Gecode, it is just a usage of the library.
As a side note, while MiniZinc uses Gecode for the optimization this is not actually anything special built-in to Gecode, it is just a usage of the library.