diff --git a/ChangeLog b/ChangeLog
index 06af3201c..5e47e7a10 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,16 @@
+2011-11-16  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Fully quote guards used by neverclaims.
+
+	Especially with should write !(p0) and not !p0, because p0 is
+	usually #define'd by the user and he may have forgotten to quote
+	the value of the macro.  This issue was discovered by Kristin
+	Yvonne Rozier and diagnosed by Gerard Holzmann.
+
+	* src/tgbaalgos/neverclaim.cc (process_link): Call
+	to_spin_string(..., true) to fully parentheses the string.
+	* src/tgbatest/neverclaimread.test: Add a test.
+
 2011-11-11  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Fix a g++-4.7 warning about a variable used only in an assert().
diff --git a/THANKS b/THANKS
index 2379c63d2..e64120bd7 100644
--- a/THANKS
+++ b/THANKS
@@ -1,6 +1,7 @@
 We are grateful to these people for their comments, help, or
 suggestions.
 
+Gerard J. Holzmann
 Heikki Tauriainen
 Jean-Michel Couvreur
 Jean-Michel Ilié
diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc
index d44787fc3..4ff700bd7 100644
--- a/src/tgbaalgos/neverclaim.cc
+++ b/src/tgbaalgos/neverclaim.cc
@@ -186,7 +186,7 @@ namespace spot
 	    os_ << "  :: (";
 	    const ltl::formula* f = bdd_to_formula(si->current_condition(),
 						   automata_->get_dict());
-	    to_spin_string(f, os_);
+	    to_spin_string(f, os_, true);
 	    f->destroy();
 	    state* current = si->current_state();
 	    os_ << ") -> goto " << get_state_label(current, out) << std::endl;
diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test
index 9de8eae35..d652c2a02 100755
--- a/src/tgbatest/neverclaimread.test
+++ b/src/tgbatest/neverclaimread.test
@@ -118,5 +118,9 @@ do
 	run 0 ../ltl2tgba -E -Pf.tgba -XN f.ltl2ba
     fi
     run 0 ../ltl2tgba -DS -NN -f "$f" > f.spot
+    # Make sure there is no `!x' occurring in the
+    # output.  Because `x' is usually #define'd, we
+    # should use `!(x)' in guards.
+    grep '![^(].*->' f.spot && exit 1
     run 0 ../ltl2tgba -E -Pf.tgba -XN f.spot
 done  <formulae