1 files changed, 13 insertions, 0 deletions
diff --git a/examples/smtbmc/demo4.v b/examples/smtbmc/demo4.v
new file mode 100644
index 00000000..3f1b4727
--- /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