return all facts for CVC3 and Yices, since there is no proof parsing / unsat core extraction

--- a/src/HOL/Tools/SMT/smt_solver.ML	Mon Dec 06 10:31:29 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Mon Dec 06 10:32:39 2010 +0100
@@ -347,7 +347,8 @@
     (xrules, map snd xrules)
     ||> distinct (op =) o fst o smt_solver rm ctxt' o append irs o map_index I
     |-> map_filter o try o nth
-    |> (fn xs => {outcome=NONE, used_facts=xs, run_time_in_msecs=NONE})
+    |> (fn xs => {outcome=NONE, used_facts=if solver_name_of ctxt = "z3" (* FIXME *) then xs
+      else xrules, run_time_in_msecs=NONE})
   end
   handle SMT_Failure.SMT fail => {outcome=SOME fail, used_facts=[],
     run_time_in_msecs=NONE}