riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
13,378 Commits 98 Branches 49 Tags 42 MiB
Commit Graph

3 Commits

Author SHA1 Message Date
Jannis Harder 42122e240e smtbmc: Add --track-assumes and --minimize-assumes options 
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.
 2024-03-11 15:13:11 +01:00
Jannis Harder 3fab4d42ec smtbmc: Allow raw SMT-LIBv2 comamnds and expressions for --incremental 2023-12-14 16:44:21 +01:00
Jannis Harder e319606ec9 smtbmc: Add --incremental mode 2023-11-16 13:22:17 +01:00