# HG changeset patch
# User blanchet
# Date 1280507298 -7200
# Node ID a9d96531c2ee645dc7270283963790e0f1e74dd6
# Parent  d44a5f602b8c893bede0c002394c71542b98b74f
gracefully handle the case where no integers occur in the formula and the "max" option is used

diff -r d44a5f602b8c -r a9d96531c2ee src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Jul 30 15:03:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Jul 30 18:28:18 2010 +0200
@@ -778,7 +778,8 @@
         val max_axiom =
           if honors_explicit_max then
             KK.True
-          else if is_twos_complement_representable bits (epsilon - delta) then
+          else if bits = 0 orelse
+               is_twos_complement_representable bits (epsilon - delta) then
             KK.LE (KK.Cardinality dom_r, KK.Num explicit_max)
           else
             raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr",