I am experimenting with OpenJML in combination with Z3, and I'm trying to reason about double or float values: class Test { //@ requires b > 0; void a(double b) { } void b() { a(2.4); }...