When using an off-the-shelf Satisfiability Modulo Theory (SMT) solver for solving decision problems, we empirically demonstrate that solver performance is dependent on a number of factors. In particular, these are a combination of (i) constraints modeling the application behaviour, (ii) non-determinism inherent at the application level and the encoding of multiple system behaviours, and (iii) presence (absence) of witnesses, and these can affect solver performance in non-intuitive ways. Further, there is a wide variation in solver performance, e.g., in terms of time and memory consumed across different solvers. Based on controlled experiments on analyzing schedulability problems encoded as SMT formulas, we compare the performance of selected state-of-the-art solvers. Our experiments help develop insights into understanding solver behaviour for domain-specific SMT instances, and help assess the impact of non-determinism on solver performance.