[phung@archlinux examples]$ make setreset yosys-smtbmc -s boolector setreset.smt2 Traceback (most recent call last): File "/usr/bin/yosys-smtbmc", line 296, in <module> smt = SmtIo(opts=so) File "/usr/bin/../share/yosys/python3/smtio.py", line 112, in init self.p = subprocess.Popen(self.popenvargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) File "/usr/lib/python3.6/subprocess.py", line 707, in __init_ restore_signals, start_new_session) File "/usr/lib/python3.6/subprocess.py", line 1333, in _execute_child raise child_exception_type(errno_num, err_msg) FileNotFoundError: [Errno 2] No such file or directory: 'boolector' make: *** [Makefile:194: setreset] Error 1

I have this error for using boolector SMT solver. It seems to me that this is triggered from python 3.6 system file. Could anyone advise ?

Besides, why does 'setreset' example require SMT instead of SAT ? https://gist.github.com/cr1901/a445ef31281e67a0cf286e149deaac41#sat-vs-smt