--- 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.
--- 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)