I have some definitions: let constant realtime = 0 let constant timeshare = 1
However, subsequently why3 seems to have trouble proving things involving these values, particularly things that involve knowing that realtime and timeshare don't have the same value. Inlining the values makes the proofs work out, but is not great for readability. In the end, I put 0(*realtime*) 1(*timeshare*) at all the usage sites. Is there a way to cause uses of realtime and timeshare to behave exactly like uses of 0 and 1? thanks, julia _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
