Add support for optimizing exists-forall problems.

[yosys.git] / examples / smtbmc / Makefile

diff --git a/examples/smtbmc/Makefile b/examples/smtbmc/Makefile
index 96fa058d6fbeea1fa5d1da58a711a5385bff9d6f..61994f942fb524c07fc77072fa3ec4013b9c829e 100644 (file)
--- a/examples/smtbmc/Makefile
+++ b/examples/smtbmc/Makefile
@@ -1,5 +1,5 @@
 
-all: demo1 demo2 demo3 demo4 demo5 demo6 demo7 demo8
+all: demo1 demo2 demo3 demo4 demo5 demo6 demo7 demo8 demo9
 
 demo1: demo1.smt2
        yosys-smtbmc --dump-vcd demo1.vcd demo1.smt2
@@ -28,6 +28,9 @@ demo7: demo7.smt2
 demo8: demo8.smt2
        yosys-smtbmc -s z3 -t 1 -g demo8.smt2
 
+demo9: demo9.smt2
+       yosys-smtbmc -s z3 -t 1 -g demo9.smt2
+
 demo1.smt2: demo1.v
        yosys -ql demo1.yslog -p 'read_verilog -formal demo1.v; prep -top demo1 -nordff; write_smt2 -wires demo1.smt2'
 
@@ -52,6 +55,9 @@ demo7.smt2: demo7.v
 demo8.smt2: demo8.v
        yosys -ql demo8.yslog -p 'read_verilog -formal demo8.v; prep -top demo8 -nordff; write_smt2 -stbv -wires demo8.smt2'
 
+demo9.smt2: demo9.v
+       yosys -ql demo9.yslog -p 'read_verilog -formal demo9.v; prep -top demo9 -nordff; write_smt2 -stbv -wires demo9.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
@@ -61,6 +67,7 @@ clean:
        rm -f demo6.yslog demo6.smt2
        rm -f demo7.yslog demo7.smt2
        rm -f demo8.yslog demo8.smt2
+       rm -f demo9.yslog demo9.smt2
 
-.PHONY: demo1 demo2 demo3 demo4 demo5 demo6 demo7 demo8 clean
+.PHONY: demo1 demo2 demo3 demo4 demo5 demo6 demo7 demo8 demo9 clean