4 files changed, 36 insertions, 2 deletions
diff --git a/examples/smtbmc/.gitignore b/examples/smtbmc/.gitignore
index bf83e0d44..fbddafa8a 100644
--- a/examples/smtbmc/.gitignore
+++ b/examples/smtbmc/.gitignore
@@ -10,3 +10,6 @@ demo2_tb.vcd
 demo3.smt2
 demo3.vcd
 demo3.yslog
+demo4.smt2
+demo4.vcd
+demo4.yslog
diff --git a/examples/smtbmc/Makefile b/examples/smtbmc/Makefile
index b3feb07c7..588e8429b 100644
--- a/examples/smtbmc/Makefile
+++ b/examples/smtbmc/Makefile
@@ -1,5 +1,5 @@
 
-all: demo1 demo2 demo3
+all: demo1 demo2 demo3 demo4
 
 demo1: demo1.smt2
 	yosys-smtbmc --dump-vcd demo1.vcd demo1.smt2
@@ -13,6 +13,9 @@ demo2: demo2.smt2
 demo3: demo3.smt2
 	yosys-smtbmc --dump-vcd demo3.vcd --smtc demo3.smtc demo3.smt2
 
+demo4: demo4.smt2
+	yosys-smtbmc -s yices --dump-vcd demo4.vcd --smtc demo4.smtc demo4.smt2
+
 demo1.smt2: demo1.v
 	yosys -ql demo1.yslog -p 'read_verilog -formal demo1.v; prep -top demo1 -nordff; write_smt2 -wires -mem -bv demo1.smt2'
 
@@ -22,10 +25,14 @@ demo2.smt2: demo2.v
 demo3.smt2: demo3.v
 	yosys -ql demo3.yslog -p 'read_verilog -formal demo3.v; prep -top demo3 -nordff; write_smt2 -wires -mem -bv demo3.smt2'
 
+demo4.smt2: demo4.v
+	yosys -ql demo4.yslog -p 'read_verilog -formal demo4.v; prep -top demo4 -nordff; write_smt2 -wires -mem -bv demo4.smt2'
+
 clean:
 	rm -f demo1.yslog demo1.smt2 demo1.vcd
 	rm -f demo2.yslog demo2.smt2 demo2.vcd demo2.smtc demo2_tb.v demo2_tb demo2_tb.vcd
 	rm -f demo3.yslog demo3.smt2 demo3.vcd
+	rm -f demo4.yslog demo4.smt2 demo4.vcd
 
-.PHONY: demo1 demo2 demo3 clean
+.PHONY: demo1 demo2 demo3 demo4 clean
 
diff --git a/examples/smtbmc/demo4.smtc b/examples/smtbmc/demo4.smtc
new file mode 100644
index 000000000..2f91f8164
--- /dev/null
+++ b/examples/smtbmc/demo4.smtc
@@ -0,0 +1,11 @@
+initial
+assume [rst]
+
+always -1
+assume (not [rst])
+assume (=> [-1:inv2] [inv2])
+
+final -2
+assume [-1:inv2]
+assume (not [-2:inv2])
+assert (= [r1] [r2])
diff --git a/examples/smtbmc/demo4.v b/examples/smtbmc/demo4.v
new file mode 100644
index 000000000..3f1b47277
--- /dev/null
+++ b/examples/smtbmc/demo4.v
@@ -0,0 +1,13 @@
+// Demo for "final" smtc constraints
+
+module demo4(input clk, rst, inv2, input [15:0] in, output reg [15:0] r1, r2);
+	always @(posedge clk) begin
+		if (rst) begin
+			r1 <= in;
+			r2 <= -in;
+		end else begin
+			r1 <= r1 + in;
+			r2 <= inv2 ? -(r2 - in) : (r2 - in);
+		end
+	end
+endmodule