From 4ef02d2c5cf5ea68adee915ab5d2fab261c2dc9c Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Wed, 8 Jun 2022 12:08:34 +0200
Subject: [PATCH] Regression test for smtbmc --unroll --noincr

---
 tests/regression/unroll_noincr_traces.sby | 29 +++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 tests/regression/unroll_noincr_traces.sby

diff --git a/tests/regression/unroll_noincr_traces.sby b/tests/regression/unroll_noincr_traces.sby
new file mode 100644
index 0000000..e93d18f
--- /dev/null
+++ b/tests/regression/unroll_noincr_traces.sby
@@ -0,0 +1,29 @@
+[tasks]
+boolector
+yices
+z3
+
+[options]
+mode bmc
+expect fail
+
+[engines]
+boolector: smtbmc boolector -- --noincr
+yices: smtbmc --unroll yices -- --noincr
+z3: smtbmc --unroll z3 -- --noincr
+
+
+[script]
+read -formal top.sv
+prep -top top
+
+[file top.sv]
+module top(input clk);
+    reg [7:0] counter = 0;
+    wire derived = counter * 7;
+
+    always @(posedge clk) begin
+        counter <= counter + 1;
+        assert (counter < 4);
+    end
+endmodule
-- 
2.30.2