Bug in translating real constant

[davidcok]

Problem with this code:

public class X {

/*@
  model public static void test(\real j, \real k) {
    //@ assert j >= 0 && k > 0 ==> j%k >= 0;
  }
*/
}

[davidcok]

Fixed in x12ce0f95fd821e56a48dadcfb21d48bc0a1cf160