mirror of https://github.com/YosysHQ/yosys.git
42122e240e
The --track-assumes option makes smtbmc keep track of which assumptions were used by the solver when reaching an unsat case and to output that set of assumptions. This is particularly useful to debug PREUNSAT failures. The --minimize-assumes option can be used in addition to --track-assumes which will cause smtbmc to spend additional solving effort to produce a minimal set of assumptions that are sufficient to cause the unsat result. |
||
|---|---|---|
| .. | ||
| .gitignore | ||
| Makefile.inc | ||
| example.v | ||
| example.ys | ||
| smt2.cc | ||
| smtbmc.py | ||
| smtbmc_incremental.py | ||
| smtio.py | ||
| test_cells.sh | ||
| witness.py | ||
| ywio.py | ||