CBMC
|
Directories | |
bdd | |
flattening | |
floatbv | |
lowering | |
prop | |
qbf | |
refinement | |
sat | |
smt2 | |
smt2_incremental | |
strings | |
Files | |
conflict_provider.h | |
Capability to check whether an expression is a reason for the solver returning UNSAT. | |
decision_procedure.cpp | |
Decision Procedure Interface. | |
decision_procedure.h | |
Decision Procedure Interface. | |
hardness_collector.h | |
Capability to collect the statistics of the complexity of individual solver queries. | |
stack_decision_procedure.h | |
Decision procedure with incremental solving with contexts and assumptions. | |