Oh, I don't mind adversarial examples. As a user of SMT solvers (for semi-automated program verification), I just find them unpredictable and frustrating. But I

Oh, I don't mind adversarial examples. As a user of SMT solvers (for semi-automated program verification), I just find them unpredictable and frustrating. But I've never employed SMT solvers as a library in some production system, and it's good to hear that in that case the instances could be controlled well enough for the normal operation to be predictable.