alexanderjsummers

The following example gives an error, although after expansion the code should be accepted (pasting it manually in place of the macro invocation works): ``` define foo(lname) { label lname...

While many sources of well-definedness can't happen in a domain axiom (no dependency on state, no calling functions with preconditions), potential division by zero can and should be checked for.