From 89a80dacdf013db1072c065231dbcf47e44ed391 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Fri, 23 Jun 2023 13:56:30 -0400
Subject: [PATCH] Mention Heapster in the README

---
 CHANGES.md | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/CHANGES.md b/CHANGES.md
index 55db0d6aca..7c1bd3ee24 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,6 +1,10 @@
 # Version 1.0
 
 ## New Features
+* SAW now implements Heapster, which allows extracting functional specifications
+  of memory-safe C programs to Coq. There is now a family of experimental
+  `heapster_*` commands that support this. For more information, refer to the
+  [Heapster README](heapster-saw/README.md).
 
 * New commands `enable_what4_eval` and `disable_what4_eval` to enable or
   disable What4 translation for SAWCore expressions during Crucible symbolic