Closed Kmanfi closed 8 years ago
Can you reproduce?
cd examples/smtbmc make 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
make
yosys -ql demo1.yslog -p 'read_verilog -formal demo1.v; prep -top demo1 -nordff; write_smt2 -wires demo1.smt2' yosys-smtbmc --dump-vcd demo1.vcd demo1.smt2 Traceback (most recent call last): File "/usr/local/bin/yosys-smtbmc", line 278, in <module> smt = smtio(opts=so) File "/usr/local/bin/../share/yosys/python3/smtio.py", line 74, in __init__ self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) File "/Library/Frameworks/Python.framework/Versions/3.5/lib/python3.5/subprocess.py", line 950, in __init__ restore_signals, start_new_session) File "/Library/Frameworks/Python.framework/Versions/3.5/lib/python3.5/subprocess.py", line 1540, in _execute_child raise child_exception_type(errno_num, err_msg) FileNotFoundError: [Errno 2] No such file or directory: 'z3' make: *** [demo1] Error 1
FileNotFoundError: [Errno 2] No such file or directory: 'z3'
You need to install z3: https://github.com/Z3Prover/z3
demo4 uses yices instead of z3: http://yices.csl.sri.com/
Can you reproduce?
cd examples/smtbmc make clean
make