From 1e9ef1bccd30d5367a71fac85d09810f60391f04 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Thu, 30 Oct 2025 18:59:41 -0700
Subject: [PATCH] Test ebmc-spot s_eventually2.bmc passes

---
 regression/ebmc-spot/sva-buechi/s_eventually2.bmc.desc | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/regression/ebmc-spot/sva-buechi/s_eventually2.bmc.desc b/regression/ebmc-spot/sva-buechi/s_eventually2.bmc.desc
index 0503d5490..3709ae759 100644
--- a/regression/ebmc-spot/sva-buechi/s_eventually2.bmc.desc
+++ b/regression/ebmc-spot/sva-buechi/s_eventually2.bmc.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 ../../verilog/SVA/s_eventually2.sv
 --buechi --module main --bound 20
 ^\[main\.p0\] always s_eventually main.reset \|\| main\.counter == 10: PROVED up to bound 20$
@@ -8,4 +8,3 @@ KNOWNBUG
 --
 ^warning: ignoring
 --
-This gives the wrong answer for main.p0.