# HG changeset patch
# User bulwahn
# Date 1322641267 -3600
# Node ID 805a2acf47fdb96a30a3eb30d2a183c4f0ab9447
# Parent  06acd5cbb53b122450a010e0b00ea242c1bc5940
quickcheck returns counterexamples that are potentially spurious due to underspecified code equations and match exceptions

diff -r 06acd5cbb53b -r 805a2acf47fd src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Nov 30 09:21:04 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Nov 30 09:21:07 2011 +0100
@@ -287,14 +287,14 @@
 fun mk_test_term lookup mk_closure mk_if none_t return ctxt =
   let
     fun mk_naive_test_term t =
-      fold_rev mk_closure (map lookup (Term.add_free_names t [])) (mk_if (t, none_t, return)) 
+      fold_rev mk_closure (map lookup (Term.add_free_names t [])) (mk_if (t, none_t, return))
     fun mk_smart_test_term' concl bound_vars assms =
       let
         fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
         val (vars, check) =
           case assms of [] => (vars_of concl, (concl, none_t, return))
-            | assm :: assms => (vars_of assm, (assm,
-                mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms, none_t))
+            | assm :: assms => (vars_of assm, (HOLogic.mk_not assm, none_t, 
+                mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms))
       in
         fold_rev mk_closure (map lookup vars) (mk_if check)
       end
@@ -375,9 +375,10 @@
             $ lambda free (lambda term_var t)) $ depth
     val none_t = @{term "None :: term list option"}
     fun mk_safe_if (cond, then_t, else_t) =
-      @{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"} $
-        (@{term "If :: bool => term list option => term list option => term list option"}
-        $ cond $ then_t $ else_t) $ none_t;
+      @{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"}
+        $ (@{term "If :: bool => term list option => term list option => term list option"}
+        $ cond $ then_t $ else_t)
+        $ (if Config.get ctxt Quickcheck.potential then else_t else none_t);
     val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_safe_if none_t return ctxt
   in lambda depth (mk_test_term t) end