Thanks for the explanation! > When used as an application, Z3 will tell you something's wrong by spitting this out in the terminal: (+ c1 c2 c3) |-> (* (- 1) o

Thanks for the explanation! > When used as an application, Z3 will tell you something's wrong by spitting this out in the terminal: (+ c1 c2 c3) |-> (* (- 1) oo) This part is what I was looking for. I was surprised that the behavior wasn’t accompanied by any warnings in the article.