1 files changed, 17 insertions, 0 deletions
diff --git a/examples/smtbmc/demo1.v b/examples/smtbmc/demo1.v
new file mode 100644
index 000000000..59e497825
--- /dev/null
+++ b/examples/smtbmc/demo1.v
@@ -0,0 +1,17 @@
+module demo1(input clk, input addtwo, output iseven);
+	reg [3:0] cnt = 0;
+	wire [3:0] next_cnt;
+
+	inc inc_inst (addtwo, iseven, cnt, next_cnt);
+
+	always @(posedge clk)
+		cnt = (iseven ? cnt == 10 : cnt == 11) ? 0 : next_cnt;
+	
+	assert property (cnt != 15);
+	// initial expect ((iseven && addtwo) || cnt == 9);
+endmodule
+
+module inc(input addtwo, output iseven, input [3:0] a, output [3:0] y);
+	assign iseven = !a[0];
+	assign y = a + (addtwo ? 2 : 1);
+endmodule