From: Jannis Harder <me@jix.one>
Date: Wed, 8 Jun 2022 10:08:34 +0000 (+0200)
Subject: Regression test for smtbmc --unroll --noincr
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4ef02d2c5cf5ea68adee915ab5d2fab261c2dc9c;p=SymbiYosys.git

Regression test for smtbmc --unroll --noincr
---

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