# HG changeset patch
# User blanchet
# Date 1444054473 -7200
# Node ID 1cfc476198c937820239c0c40e7b826168ae7e46
# Parent  d4ec7594f558f3149bb2203749311cdbee5518bb
avoid too aggressive optimization of 'finite' predicate

diff -r d4ec7594f558 -r 1cfc476198c9 NEWS
--- a/NEWS	Mon Oct 05 15:57:25 2015 +0200
+++ b/NEWS	Mon Oct 05 16:14:33 2015 +0200
@@ -253,6 +253,7 @@
   - Eliminated obsolete "blocking" option and related subcommands.
 
 * Nitpick:
+  - Fixed soundness bug in translation of "finite" predicate.
   - Fixed soundness bug in "destroy_constrs" optimization.
   - Removed "check_potential" and "check_genuine" options.
   - Eliminated obsolete "blocking" option.
diff -r d4ec7594f558 -r 1cfc476198c9 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Oct 05 15:57:25 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Oct 05 16:14:33 2015 +0200
@@ -787,8 +787,8 @@
              case polar of
                Neut =>
                if opt1 then raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u])
-               else KK.True
-             | Pos => formula_for_bool (not opt1)
+               else KK.True (* sound? *)
+             | Pos => KK.False
              | Neg => KK.True
            end
          | Op1 (IsUnknown, _, _, u1) => kk_no (to_r u1)