Skip to content

Commit 129c081

Browse files
authored
Merge pull request #922 from diffblue/k-induction6
KNOWNBUG test for engine heuristic
2 parents bc38997 + 08e6923 commit 129c081

File tree

2 files changed

+16
-0
lines changed

2 files changed

+16
-0
lines changed
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
KNOWNBUG
2+
k-induction6.sv
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
--
9+
The property should hold, but is reported as refuted.
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
module main(input clk, input x);
2+
3+
a0: assume property (not s_eventually !x);
4+
5+
p0: assert property (x);
6+
7+
endmodule

0 commit comments

Comments
 (0)