From 3bcf46b51f33f94efc388ca87e30e64c41551f37 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 18 Oct 2023 06:05:08 -0700
Subject: [PATCH] ebmc: add a basic test for CEGAR

---
 regression/ebmc/cegar/basic1.desc |  6 ++++++
 regression/ebmc/cegar/basic1.sv   | 12 ++++++++++++
 2 files changed, 18 insertions(+)
 create mode 100644 regression/ebmc/cegar/basic1.desc
 create mode 100644 regression/ebmc/cegar/basic1.sv

diff --git a/regression/ebmc/cegar/basic1.desc b/regression/ebmc/cegar/basic1.desc
new file mode 100644
index 000000000..0db2b67c5
--- /dev/null
+++ b/regression/ebmc/cegar/basic1.desc
@@ -0,0 +1,6 @@
+KNOWNBUG
+basic1.sv
+--cegar
+SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
diff --git a/regression/ebmc/cegar/basic1.sv b/regression/ebmc/cegar/basic1.sv
new file mode 100644
index 000000000..105aa9418
--- /dev/null
+++ b/regression/ebmc/cegar/basic1.sv
@@ -0,0 +1,12 @@
+module top(input clk);
+
+  reg important;
+  reg not_important;
+
+  initial important = 1;
+  always @(posedge clk)
+    important = important;
+
+  assert property (important == 1);
+
+endmodule