nmgfifotestcasefail

======================================================================
FAIL: test_reversible (nmigen.test.test_lib_coding.GrayCoderTestCase)
----------------------------------------------------------------------
Traceback (most recent call last):
  File "/home/fubar/software/nmigen/nmigen/test/test_lib_coding.py", line 122, in test_reversible
    self.assertFormal(spec, mode="prove")
  File "/home/fubar/software/nmigen/nmigen/test/tools.py", line 103, in assertFormal
    self.fail("Formal verification failed:\n" + stdout)
AssertionError: Formal verification failed:
SBY 20:45:31 [spec_lib_coding_reversible] Removing direcory 'spec_lib_coding_reversible'.
SBY 20:45:31 [spec_lib_coding_reversible] Writing 'spec_lib_coding_reversible/src/top.il'.
SBY 20:45:31 [spec_lib_coding_reversible] engine_0: smtbmc
SBY 20:45:31 [spec_lib_coding_reversible] base: starting process "cd spec_lib_coding_reversible/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 20:45:31 [spec_lib_coding_reversible] base: finished (returncode=0)
SBY 20:45:31 [spec_lib_coding_reversible] smt2: starting process "cd spec_lib_coding_reversible/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 20:45:31 [spec_lib_coding_reversible] smt2: finished (returncode=0)
SBY 20:45:31 [spec_lib_coding_reversible] engine_0.basecase: starting process "cd spec_lib_coding_reversible; yosys-smtbmc --presat --unroll --noprogress -t 1 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 20:45:31 [spec_lib_coding_reversible] engine_0.induction: starting process "cd spec_lib_coding_reversible; yosys-smtbmc --presat --unroll -i --noprogress -t 1 --append 0 --dump-vcd engine_0/trace_induct.vcd --dump-vlogtb engine_0/trace_induct_tb.v --dump-smtc engine_0/trace_induct.smtc model/design_smt2.smt2"
SBY 20:45:31 [spec_lib_coding_reversible] engine_0.basecase: ##   0:00:00  Solver: yices
SBY 20:45:31 [spec_lib_coding_reversible] engine_0.basecase: Traceback (most recent call last):
SBY 20:45:31 [spec_lib_coding_reversible] engine_0.basecase: File "/usr/local/bin/yosys-smtbmc", line 398, in <module>
SBY 20:45:31 [spec_lib_coding_reversible] engine_0.basecase: smt.write(line)
SBY 20:45:31 [spec_lib_coding_reversible] engine_0.basecase: File "/usr/local/bin/../share/yosys/python3/smtio.py", line 359, in write
SBY 20:45:31 [spec_lib_coding_reversible] engine_0.basecase: self.setup()
SBY 20:45:31 [spec_lib_coding_reversible] engine_0.basecase: File "/usr/local/bin/../share/yosys/python3/smtio.py", line 213, in setup
SBY 20:45:31 [spec_lib_coding_reversible] engine_0.basecase: self.p_open()
SBY 20:45:31 [spec_lib_coding_reversible] engine_0.basecase: File "/usr/local/bin/../share/yosys/python3/smtio.py", line 307, in p_open
SBY 20:45:31 [spec_lib_coding_reversible] engine_0.basecase: self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
SBY 20:45:31 [spec_lib_coding_reversible] engine_0.basecase: File "/usr/lib/python3.7/subprocess.py", line 775, in __init__
SBY 20:45:31 [spec_lib_coding_reversible] engine_0.basecase: restore_signals, start_new_session)
SBY 20:45:31 [spec_lib_coding_reversible] engine_0.basecase: File "/usr/lib/python3.7/subprocess.py", line 1522, in _execute_child
SBY 20:45:31 [spec_lib_coding_reversible] engine_0.basecase: raise child_exception_type(errno_num, err_msg, err_filename)
SBY 20:45:31 [spec_lib_coding_reversible] engine_0.basecase: FileNotFoundError: [Errno 2] No such file or directory: 'yices-smt2': 'yices-smt2'
SBY 20:45:31 [spec_lib_coding_reversible] engine_0.basecase: finished (returncode=1)
SBY 20:45:31 [spec_lib_coding_reversible] ERROR: engine_0: Engine terminated without status.
SBY 20:45:31 [spec_lib_coding_reversible] DONE (ERROR, rc=16)