Revert "Revert "Add test that is expecting to fail"" This reverts commit 3fb604c75d3e8ee45d35fac8b787cb95a8adcf84.
diff --git a/tests/sat/initval.ys b/tests/sat/initval.ys index 2079d2f..1627a37 100644 --- a/tests/sat/initval.ys +++ b/tests/sat/initval.ys
@@ -2,3 +2,23 @@ proc;; sat -seq 10 -prove-asserts + +read_verilog <<EOT +module gold(input clk, input i, output reg [1:0] o); +initial o = 2'b10; +always @(posedge clk) + o[0] <= {i,i}; +endmodule + +module gate(input clk, input i, output reg [1:0] o); +initial o = 2'b10; +always @(posedge clk) + o[0] <= i; +always @* + o[1] <= o[0]; +endmodule +EOT + +proc +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -seq 1 -falsify -prove-asserts -show-ports miter