Challenging SMT solvers to verify neural networks