Dynamic symbolic execution is widely used for test case generation and software bug/vulnerability detection because of its two advantages: high coverage and low false positives. It has also been used in the context of testing Deep Neural Networks (DNNs). Here, each activation value of a neuron is modelled as a decision/choice point (similarly to the way a conditional program statement is handled). However, the main challenge is still the \emph{exponential} number of combinatorial cases of activated neurons. In this paper, we propose to develop an \emph{effective pruning} method to deal with this problem. Firstly, we propose to construct a \emph{better symbolic tree representation} of DNNs for effective search space pruning both in test case generation and in bug/vulnerability detection. Secondly, we propose a novel unsatisfiable core extraction technique, based on the \emph{binary search} algorithm and \emph{variable dependency graph}, to support that method. Finally, we demonstrate their impact via a thorough experimental evaluation and promising results.