diff --git a/ChangeLog b/ChangeLog
index 2ce235a6d..087bbeba9 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,14 @@
+2011-02-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Read guard of the form !(x) in neverclaims.
+
+	So far all neverclaims encountered would use (!(x)), but the
+	files from the Büchi store do not.
+
+	* src/neverparse/neverclaimscan.ll: Accept ! in front of guard,
+	so that we can read Promela files from Goal's Büchi store.
+	* src/tgbatest/neverclaimread.test: Test it.
+
 2011-02-03  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Recognize Goal's syntax for Boolean operators.
diff --git a/src/neverparse/neverclaimscan.ll b/src/neverparse/neverclaimscan.ll
index 64b880aad..d92e780bd 100644
--- a/src/neverparse/neverclaimscan.ll
+++ b/src/neverparse/neverclaimscan.ll
@@ -1,4 +1,4 @@
-/* Copyright (C) 2010 Laboratoire de Recherche et Développement de
+/* Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement de
 ** l'Epita (LRDE).
 **
 ** This file is part of Spot, a model checking library.
@@ -56,7 +56,7 @@ eol      \n|\r|\n\r|\r\n
 "goto"			return token::GOTO;
 "false"|"0"		return token::FALSE;
 
-"(".*")"|"true"|"1"     {
+"!"?"(".*")"|"true"|"1"   {
                           yylval->str = new std::string(yytext, yyleng);
 			  return token::FORMULA;
                         }
diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test
index 3aac302be..1fbc0182e 100755
--- a/src/tgbatest/neverclaimread.test
+++ b/src/tgbatest/neverclaimread.test
@@ -35,6 +35,7 @@ T1:
 if
 :: (p1 && (! p0)) -> goto accept_all
 :: (p1) -> goto T1
+:: !(p1) -> goto T2_init
 fi;
 accept_all:
 skip
@@ -53,6 +54,7 @@ digraph G {
   2 [label="T1"]
   2 -> 3 [label="p1 & !p0\n"]
   2 -> 2 [label="p1\n"]
+  2 -> 1 [label="!p1\n"]
   3 [label="accept_all"]
   3 -> 3 [label="1\n{Acc[1]}"]
 }