--- a/src/HOL/Tools/SMT2/smt2_setup_solvers.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_setup_solvers.ML	Thu Mar 13 13:18:13 2014 +0100
@@ -167,7 +167,7 @@
   default_max_relevant = 350 (* FUDGE *),
   supports_filter = true,
   outcome = z3_on_first_or_last_line,
-  cex_parser = NONE,
+  cex_parser = SOME Z3_New_Model.parse_counterex,
   replay = SOME Z3_New_Proof_Replay.replay }
 
 end