Add Counterexamples to Refinement Errors

[rcosta358]

This PR adds counterexamples to refinement errors by extracting the SMT model from Z3.

Changes

• Added the getCounterexample method to TranslatorToZ3 that extracts variable assignments (for constants only)
• In the SMTEvaluator, when the SMT returns SAT we get the SMT model and throw the TypeCheckError containing the counterexample
• In the caller methods, instead of returning boolean it now returns Counterexample - if counterexample is null, then the check succeeded, otherwise it failed
• In the RefinementError, we override the getDetails method to add the counterexamples as extra information in the error message. Also, it filters out fresh variables which don't even exist in the source code, and if the counterexample is the same as the found type (already included in the message), then the counterexample is not shown.

Examples

---

These will need improvements in the future, especially when dealing with ghosts:

 --> Counterexample: #list_4 == java.util.ArrayList!val!1 && #list_8 == java.util.ArrayList!val!0 && #index_7 == 1