src/HOL/Tools/SMT/z3_model.ML

 
 (* overall procedure *)
 
 val is_free_constraint = Term.exists_subterm (fn Free _ => true | _ => false)
 
+fun is_free_def (Const (@{const_name HOL.eq}, _) $ Free _ $ _) = true
+  | is_free_def _ = false
+
+fun defined tp =
+  try (pairself (fst o HOLogic.dest_eq)) tp
+  |> the_default false o Option.map (op aconv)
+
+fun add_free_defs free_cs defs =
+  let val (free_defs, defs') = List.partition is_free_def defs
+  in (free_cs @ filter_out (member defined free_cs) free_defs, defs') end
+
 fun is_const_def (Const (@{const_name HOL.eq}, _) $ Const _ $ _) = true
   | is_const_def _ = false
 
 fun parse_counterex ctxt ({terms, ...} : SMT_Translate.recon) ls =
   read_cex terms ls

   |> remove_int_nat_coercions
   |> unfold_funapp
   |> unfold_eqs
   |>> map swap_free
   |>> filter is_free_constraint
+  |-> add_free_defs
   |> frees_for_vars ctxt
   ||> filter is_const_def
 
 end