equal
deleted
inserted
replaced
926 in |
926 in |
927 if not (null sound_problems) andalso |
927 if not (null sound_problems) andalso |
928 forall (KK.is_problem_trivially_false o fst) |
928 forall (KK.is_problem_trivially_false o fst) |
929 sound_problems then |
929 sound_problems then |
930 print_n (fn () => |
930 print_n (fn () => |
931 "Warning: The conjecture either trivially holds for the \ |
931 "Warning: The conjecture " ^ |
932 \given scopes or lies outside Nitpick's supported \ |
932 (if falsify then "either trivially holds" |
|
933 else "is either trivially unsatisfiable") ^ |
|
934 " for the given scopes or lies outside Nitpick's supported \ |
933 \fragment." ^ |
935 \fragment." ^ |
934 (if exists (not o KK.is_problem_trivially_false o fst) |
936 (if exists (not o KK.is_problem_trivially_false o fst) |
935 unsound_problems then |
937 unsound_problems then |
936 " Only potentially spurious " ^ das_wort_model ^ |
938 " Only potentially spurious " ^ das_wort_model ^ |
937 "s may be found." |
939 "s may be found." |