An experimental framework for temporal verification based on first-order linear-time temporal logic. Our goal is to express transition systems in first-order logic and verify temporal correctness properties, including safety and liveness.
BSD 2-Clause "Simplified" License
14
stars
1
forks
source link
Remember assumptions from last check_sat in get_minimal_model #66
The sequence of check_sat(assumptions) followed by get_minimal_model() on a solver was previously buggy in that the minimization acted without those assumptions, because it issued check_sat queries without them. In order to fix this, we remember the assumptions in any call to check_sat and then start with those assumptions in the minimization process if the next call is get_minimal_model.
I also added a regression test that fails without this fix.
The sequence of
check_sat(assumptions)followed byget_minimal_model()on a solver was previously buggy in that the minimization acted without those assumptions, because it issuedcheck_satqueries without them. In order to fix this, we remember the assumptions in any call tocheck_satand then start with those assumptions in the minimization process if the next call isget_minimal_model.I also added a regression test that fails without this fix.
Fixes #63.