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.
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.