15:23:57scymtymsomething to look at on a slow day: https://techfak.de/~jmoringe/difference-logic-and-equality.png . this is partial integration of difference logic (i.e. x - y ≤ c) and equivalence with uninterpreted functions into the SMT solver
15:25:16beachI don't understand much, but I like how you are using McCLIM for it.
15:26:06scymtymfor debugging as always. this stuff is hard to think about without visualization (for me)