Yes, the core supports exact rationals. This is easier to deal with in formal verification than floating point.

I made the UI snap to a fixed precision, such that its easy to reproduce special cases with overlapping edges, coinciding vertices etc. that make up much of the complexity of the algorithm.