update changelog

GaloisInc · Sep 19, 2022 · 37e9f97 · 37e9f97
1 parent 207b068
commit 37e9f97
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -86,6 +86,10 @@
 * The experimental and rarely-used `goal_assume` tactic has been
   removed. The use case it was targeting is better solved via sequents.
 
+* A new experimental `llvm_verify_x86_with_invariant` command that
+  allows verification certain kinds of simple loops by using a
+  user-provided loop invariant.
+
 # Version 0.9
 
 ## New Features