# HG changeset patch
# User blanchet
# Date 1402585322 -7200
# Node ID 2eb14982cd291f194527ed5b6a323b048bc0d93c
# Parent  b0b9a10e4bf42c88150cf58dcf883cea4f8abf71
made CVC3 work with SMT2 stack

diff -r b0b9a10e4bf4 -r 2eb14982cd29 src/HOL/Tools/SMT2/smt2_systems.ML
--- a/src/HOL/Tools/SMT2/smt2_systems.ML	Thu Jun 12 15:47:36 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Thu Jun 12 17:02:02 2014 +0200
@@ -31,9 +31,9 @@
     " failed -- enable tracing using the " ^ quote (Config.name_of SMT2_Config.trace) ^
     " option for details"))
 
-fun on_first_line test_outcome solver_name lines =
+fun on_first_nontrivial_line test_outcome solver_name lines =
   let
-    val empty_line = (fn "" => true | _ => false)
+    val empty_line = (fn "" => true | s => String.isPrefix "***" s)
     val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
     val (l, ls) = split_first (snd (take_prefix empty_line lines))
   in (test_outcome solver_name l, ls) end
@@ -44,7 +44,7 @@
 local
   fun cvc3_options ctxt = [
     "-seed", string_of_int (Config.get ctxt SMT2_Config.random_seed),
-    "-lang", "smtlib", "-output-lang", "presentation",
+    "-lang", "smt2", "-output-lang", "presentation",
     "-timeout", string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout))]
 in
 
@@ -55,7 +55,7 @@
   command = make_command "CVC3",
   options = cvc3_options,
   default_max_relevant = 400 (* FUDGE *),
-  outcome = on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
+  outcome = on_first_nontrivial_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
   parse_proof = NONE,
   replay = NONE }
 
@@ -75,7 +75,7 @@
       string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)),
     "--smtlib"]),
   default_max_relevant = 350 (* FUDGE *),
-  outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
+  outcome = on_first_nontrivial_line (outcome_of "unsat" "sat" "unknown"),
   parse_proof = NONE,
   replay = NONE }
 
@@ -141,7 +141,7 @@
   command = z3_make_command "Z3_NEW",
   options = z3_options,
   default_max_relevant = 350 (* FUDGE *),
-  outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
+  outcome = on_first_nontrivial_line (outcome_of "unsat" "sat" "unknown"),
   parse_proof = SOME Z3_New_Replay.parse_proof,
   replay = SOME Z3_New_Replay.replay }
 
diff -r b0b9a10e4bf4 -r 2eb14982cd29 src/HOL/Tools/SMT2/z3_new_interface.ML
--- a/src/HOL/Tools/SMT2/z3_new_interface.ML	Thu Jun 12 15:47:36 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_interface.ML	Thu Jun 12 17:02:02 2014 +0200
@@ -31,11 +31,8 @@
 
 local
   fun translate_config ctxt =
-    let
-      val {serialize, ...} = SMTLIB2_Interface.translate_config ctxt
-    in
-      {header=K "", serialize=serialize, has_datatypes=true}
-    end
+    {header = K "", has_datatypes = true,
+     serialize = #serialize (SMTLIB2_Interface.translate_config ctxt)}
 
   fun is_div_mod @{const div (int)} = true
     | is_div_mod @{const mod (int)} = true