We consider the problem of verifying the safety of trained, piecewise-linear neural network controllers. Prior work, including Z3 [9], PPL [4], and ReluPlex [19], proves to be poorly suited for the task. We present an alternative approach based on a symbolic representation of the network to efficiently compute strongest postconditions over infinite input regions, extending our earlier work [24] to higher dimensions. We demonstrate significant performance improvements on BMC of three networks from prior work.