Show differences of UNSAT cores given by SMT solvers

For the added test case, MathSAT5 produces a smaller UNSAT core
than Z3. These differences are relevant for symbolic execution
with non-chronological backtracking.