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