From 37e9f9723b922ab67f1e0633b6f5bfc682d1ee87 Mon Sep 17 00:00:00 2001 From: Robert Dockins Date: Mon, 29 Aug 2022 13:57:35 -0700 Subject: [PATCH] update changelog --- CHANGES.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index 9bb19507d3..686d137c21 100644 --- 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