# HG changeset patch
# User boehmes
# Date 1256898467 -3600
# Node ID 1f70087cdef5a93c980f246daa010adb9057f33b
# Parent  17d9c977f928431e46b2970f3e8f0e5eb43136d4
disable printing of unparsed counterexamples for CVC3 and Yices

diff -r 17d9c977f928 -r 1f70087cdef5 src/HOL/SMT/Tools/cvc3_solver.ML
--- a/src/HOL/SMT/Tools/cvc3_solver.ML	Fri Oct 30 11:26:38 2009 +0100
+++ b/src/HOL/SMT/Tools/cvc3_solver.ML	Fri Oct 30 11:27:47 2009 +0100
@@ -15,8 +15,7 @@
 val solver_name = "cvc3"
 val env_var = "CVC3_SOLVER"
 
-val options =
-  ["+counterexample", "-lang", "smtlib", "-output-lang", "presentation"]
+val options = ["-lang", "smtlib", "-output-lang", "presentation"]
 
 val is_sat = String.isPrefix "Satisfiable."
 val is_unsat = String.isPrefix "Unsatisfiable."
@@ -25,11 +24,7 @@
 fun cex_kind true = "Counterexample"
   | cex_kind false = "Possible counterexample"
 
-fun raise_cex real ctxt recon ls =
-  let
-    val ls' = filter_out (String.isPrefix "%") ls
-    val p = Pretty.big_list (cex_kind real ^ " found:") (map Pretty.str ls')
-  in error (Pretty.string_of p) end
+fun raise_cex real = error (cex_kind real ^ " found.")
 
 fun core_oracle ({context, output, recon, ...} : SMT_Solver.proof_data) =
   let
@@ -38,8 +33,8 @@
     val (l, ls) = split_first (dropwhile empty_line output)
   in
     if is_unsat l then @{cprop False}
-    else if is_sat l then raise_cex true context recon ls
-    else if is_unknown l then raise_cex false context recon ls
+    else if is_sat l then raise_cex true
+    else if is_unknown l then raise_cex false
     else error (solver_name ^ " failed")
   end
 
diff -r 17d9c977f928 -r 1f70087cdef5 src/HOL/SMT/Tools/yices_solver.ML
--- a/src/HOL/SMT/Tools/yices_solver.ML	Fri Oct 30 11:26:38 2009 +0100
+++ b/src/HOL/SMT/Tools/yices_solver.ML	Fri Oct 30 11:27:47 2009 +0100
@@ -15,14 +15,12 @@
 val solver_name = "yices"
 val env_var = "YICES_SOLVER"
 
-val options = ["--evidence", "--smtlib"]
+val options = ["--smtlib"]
 
 fun cex_kind true = "Counterexample"
   | cex_kind false = "Possible counterexample"
 
-fun raise_cex real ctxt rtab ls =
-  let val p = Pretty.big_list (cex_kind real ^ " found:") (map Pretty.str ls)
-  in error (Pretty.string_of p) end
+fun raise_cex real = error (cex_kind real ^ " found.")
 
 structure S = SMT_Solver
 
@@ -33,8 +31,8 @@
     val (l, ls) = split_first (dropwhile empty_line output)
   in
     if String.isPrefix "unsat" l then @{cprop False}
-    else if String.isPrefix "sat" l then raise_cex true context recon ls
-    else if String.isPrefix "unknown" l then raise_cex false context recon ls
+    else if String.isPrefix "sat" l then raise_cex true
+    else if String.isPrefix "unknown" l then raise_cex false
     else error (solver_name ^ " failed")
   end