Non-determenism in the defintion of minInt

[geo2a]

In a recent K update in KEVM there was a failing proof caused by the differences in term simplification in Booster vs Kore. Booster started using an SMT solver when applying equations, hence it applied more of those than before.

The deeper reason for the disagreement between Booster and Kore here is the non-determinism in the definition of minInt:

  rule minInt(I1:Int, I2:Int) => I1 requires I1 <=Int I2
  rule minInt(I1:Int, I2:Int) => I2 requires I1 >=Int I2

In the proof, a minInt term is produced as a result of applying the range-memUpdate-in-between simplification. Constrains are such that the minInt are actually equal, therefore both equations apply. Kore chooses to apply the second equation and Booster chooses the first. I do not know exactly why this happens this way, but both scenarios are sound.

We should resolve the non-determinism in the definition of minInt. I suggest we choose the first argument if they are equal.