# HG changeset patch
# User bulwahn
# Date 1322774075 -3600
# Node ID 6bd0acefaedbdd871d10c89ede7d4f1111fca9a1
# Parent  a709e1a0f3ddbb2f7551461ed2d997a5ef1c6944
outputing if counterexample is potentially spurious or not

diff -r a709e1a0f3dd -r 6bd0acefaedb src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Thu Dec 01 22:14:35 2011 +0100
+++ b/src/Tools/quickcheck.ML	Thu Dec 01 22:14:35 2011 +0100
@@ -113,7 +113,7 @@
 fun found_counterexample (Result r) = is_some (#counterexample r)
 
 fun response_of (Result r) = case (#counterexample r, #evaluation_terms r) of
-    (SOME (_, ts), SOME evals) => SOME (ts, evals)
+    (SOME ts, SOME evals) => SOME (ts, evals)
   | (NONE, NONE) => NONE
 
 fun timings_of (Result r) = #timings r
@@ -328,8 +328,9 @@
 fun tool_name auto = (if auto then "Auto " else "") ^ "Quickcheck"
 
 fun pretty_counterex ctxt auto NONE = Pretty.str (tool_name auto ^ " found no counterexample.")
-  | pretty_counterex ctxt auto (SOME (cex, eval_terms)) =
-      Pretty.chunks ((Pretty.str (tool_name auto ^ " found a counterexample:\n") ::
+  | pretty_counterex ctxt auto (SOME ((genuine, cex), eval_terms)) =
+      Pretty.chunks ((Pretty.str (tool_name auto ^ " found a " ^
+        (if genuine then "counterexample:" else  "potentially spurious counterexample due to underspecified functions:") ^ "\n") ::
         map (fn (s, t) =>
           Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex))
         @ (if null eval_terms then []