Previously, unary minus expressions actually ended up formatted as binary expressions in infix format, which meant that the unary minus operator actually disappeared.
Additionally, SMTCheckerTest was actually always ignoring the invariant message, and we fix that as well.
Previously, unary minus expressions actually ended up formatted as binary expressions in infix format, which meant that the unary minus operator actually disappeared.
Additionally, SMTCheckerTest was actually always ignoring the invariant message, and we fix that as well.