diff --git a/wrap/python/ajax/spotcgi.in b/wrap/python/ajax/spotcgi.in
index b5753027c..819356bed 100755
--- a/wrap/python/ajax/spotcgi.in
+++ b/wrap/python/ajax/spotcgi.in
@@ -500,6 +500,11 @@ if output_type == 'f':
unbufprint('
not an obligation')
minimized = 0
automaton = 0
+ if not f.is_syntactic_stutter_invariant():
+ if spot.is_stutter_invariant(f):
+ unbufprint('stutter invariant')
+ else:
+ unbufprint('stutter sensitive')
unbufprint('\n')
finish()
@@ -514,8 +519,9 @@ cannot be translated using this algorithm. Please use Couveur/FM.'''
dict = spot.make_bdd_dict()
-if output_type == 't' and not f.is_syntactic_stutter_invariant():
- unbufprint('Warning: The following result assumes the input formula is stuttering insensitive.')
+if output_type == 't' and not spot.is_stutter_invariant(f):
+ unbufprint('Warning: Testing automata are only valid '
+ + 'for stutter-insensitive formulas, but the input is not.')
# Should the automaton be displayed as a SBA?
issba = False