Improve algorithm that extracts unsat core from Z3

The way the Z3 unsat core is extracted is now modelled after the
MsatSolver implementation. This patch can dramatically improve the
precision of backtracking points when there are duplicates in
the sequence of path conditions.