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 exponential number of combinatorial cases of activated neurons. In this paper, we propose to develop an effective pruning method to deal with this problem. Firstly, we propose to construct a 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 binary search algorithm and variable dependency graph, to support that method. Finally, we demonstrate their impact via a thorough experimental evaluation and promising results.