|Title||Picky CDCL: SMT-solving With Flexible Literal Selection|
|Publication Type||Conference Paper|
|Year of Publication||2023|
|Authors||Britikov, Konstantin I., Hyvärinen Antti E. J., and Sharygina Natasha|
SMT solvers have traditionally been optimized for determining the satisfiability of a query as quickly as possible. However, they are increasingly being used in applications where the time required to determine satisfiability might not be the main concern, such as mining inductive invariants for safety proofs.