search

flyvy-verifier / flyvy

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

running sat sovers with indicator variables produces different results #63

Closed oralmer closed 1 year ago

oralmer commented 1 year ago

Seen in the branch unsat_core_bug by running cargo run -- updr-verify ./examples/lockserver.fly - Sorry for the messy execution, I had to set up a lot of context to get this to run... The added body of code is at the bottom of src/command.rs

When checking sat on a group of terms by assert ing them, and then calling check_sat on an empty hashmap, we get the correct result. However, when checking sat using indicator variables, we get a different, incorrect result - this incorrectness is seen in the calls to eval in the results.

In the branch, I took a term of the form exists n1, n2. f(n1) & g(n1) & h(n2) & ... - to add indicators I converted it to the term exists n1, n2. (ind1 = f(n1)) & (ind2 = g(n1)) & (ind3 = h(n2)) & ... and then called check_sat on a hashmap containing {ind: true} for all indicators. I also tried ind1 <-> f(n1) and got the same results.

tchajed commented 1 year ago

Thanks for setting it up to run!

After staring at both SMT files for a bit I found the bug: the issue is actually with get_minimal_model, which does not remember the indicator variables used for the previous call to check_sat. I think we'll just have to remember the indicator variables in Solver; the API is fundamentally stateful, if only due to the solver state.

I double-checked that in your example both models evaluate to 1 if you use get_model.

oralmer commented 1 year ago

@tchajed thanks!