# HG changeset patch
# User blanchet
# Date 1394713094 -3600
# Node ID fa88ff1d30e74bad1c35e5a0746338482eb5e07a
# Parent  34bd10a9a2adca417e16f47762f3d76d6ef831ad
simplified solution parsing

diff -r 34bd10a9a2ad -r fa88ff1d30e7 src/HOL/Tools/SMT2/smt2_systems.ML
--- a/src/HOL/Tools/SMT2/smt2_systems.ML	Thu Mar 13 13:18:14 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -133,26 +133,6 @@
      "-T:" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)),
      "-smt2"]
 
-  fun z3_on_first_or_last_line solver_name lines =
-    let
-      fun junk l =
-        if String.isPrefix "WARNING: Out of allocated virtual memory" l
-        then raise SMT2_Failure.SMT SMT2_Failure.Out_Of_Memory
-        else
-          String.isPrefix "WARNING" l orelse
-          String.isPrefix "ERROR" l orelse
-          forall Symbol.is_ascii_blank (Symbol.explode l)
-      val lines = filter_out junk lines
-      fun outcome split =
-        the_default ("", []) (try split lines)
-        |>> outcome_of "unsat" "sat" "unknown" solver_name
-    in
-      (* Starting with version 4.0, Z3 puts the outcome on the first line of the
-         output rather than on the last line. *)
-      outcome (fn lines => (hd lines, tl lines))
-      handle SMT2_Failure.SMT _ => outcome (swap o split_last)
-    end
-
   fun select_class ctxt =
     if Config.get ctxt z3_extensions then Z3_New_Interface.smtlib2_z3C
     else SMTLIB2_Interface.smtlib2C
@@ -166,7 +146,7 @@
   options = z3_options,
   default_max_relevant = 350 (* FUDGE *),
   supports_filter = true,
-  outcome = z3_on_first_or_last_line,
+  outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
   cex_parser = SOME Z3_New_Model.parse_counterex,
   replay = SOME Z3_New_Replay.replay }
 
diff -r 34bd10a9a2ad -r fa88ff1d30e7 src/HOL/Tools/SMT2/smtlib2_interface.ML
--- a/src/HOL/Tools/SMT2/smtlib2_interface.ML	Thu Mar 13 13:18:14 2014 +0100
+++ b/src/HOL/Tools/SMT2/smtlib2_interface.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -137,7 +137,7 @@
        (sort (fast_string_ord o pairself fst) funcs)
   |> fold (Buffer.add o enclose "(assert " ")\n" o SMTLIB2.str_of o
        tree_of_sterm 0) ts
-  |> Buffer.add "(check-sat)\n(get-proof)\n(get-model)\n"
+  |> Buffer.add "(check-sat)\n(get-proof)\n" (* FIXME: (get-model)\n" *)
   |> Buffer.content
 
 (* interface *)