dftlib.analysis.smt.SMTAnalysis

class SMTAnalysis

Bases: object

Analysis using SMT encoding.

Methods

check_eventually_fail	Check that the DFT will eventually fail using SMT solvers.
check_threshold

check_eventually_fail(dft: Dft, smt_file: str) → tuple[int, int, int]

Check that the DFT will eventually fail using SMT solvers. :param dft: DFT. :param smt_file: Output file in SMT format. #:return: Tuple (lower bound, upper bound, number of failable BEs)