usi-verification-and-security / golem

Solver for Constrained Horn Clauses
MIT License
34 stars 7 forks source link

Everywhere: Simplify typical use of SMT solver #38

Closed blishko closed 1 year ago

blishko commented 1 year ago

The goal is to provide a simple abstraction over OpenSMT's solver so that we do not have to repeat unnecessary complicated setup of OpenSMT's SMTConfig and MainSolver. It would also better contain future changes in OpenSMT.

In the future, this abstraction can be extended to completly isolate OpenSMT's solver in a single place.