search

usi-verification-and-security / golem

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

Refactor MBP so that it does not require OpenSMT's ModelBuilder #82

Open blishko opened 1 week ago

blishko commented 1 week ago

ModelBuilder is internal detail of OpenSMT and we should not be using it.

The problem was that we need to extend a given model with a new variable. This is not possible with OpenSMT's Model. We can build our own wrapper to support this functionality.