diff --git a/NEWS b/NEWS
index 58cbcb28c..dd4431071 100644
--- a/NEWS
+++ b/NEWS
@@ -41,6 +41,11 @@ New in spot 2.11.5.dev  (not yet released)
   - Using "randltl -S" did not correctly go through the SERE printer
     functions.
 
+  - Our copy of BuDDy's bdd_forall() had a 20 year old typo that
+    caused cache entries from bdd_exist() and bdd_forall() to be
+    mixed.  Spot was safe from this bug because it was only using
+    bdd_exist().  (Issue #535)
+
 New in spot 2.11.5  (2023-04-20)
 
   Bug fixes:
diff --git a/THANKS b/THANKS
index 93155f9d1..7986c3875 100644
--- a/THANKS
+++ b/THANKS
@@ -21,6 +21,7 @@ Felix Klaedtke
 Florian Perlié-Long
 František Blahoudek
 Gerard J. Holzmann
+Guillermo A. Perez
 Hashim Ali
 Heikki Tauriainen
 Henrich Lauko