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

Z3 "incomplete quantifiers" error #71

Closed edenfrenkel closed 1 year ago

edenfrenkel commented 1 year ago

On the qalpha branch, z3 raises an error when running env RUST_LOG=info cargo run -- infer qalpha examples/fol/hybrid_reliable_broadcast_cisa.fly --quantifier "F node 1" --quantifier "E node 1" --qf-body pdnf --cubes 2 --cube-size 1 --non-unit 0 --smt

The error message is thread '<unnamed>' panicked at 'sat solver returned unknown: |(incomplete quantifiers)|', src/inference/basics.rs:160:45, and an example SMT file can be found here.

The same command appears to work when using cvc5, although this takes a long time to run.

tchajed commented 1 year ago

This is probably due to the Z3 configuration. This example should work in mypyvy - can you figure out what options it's using (probably the SMT file is the easiest way)? I tried to check myself but I'm running into some issues with the python z3 bindings.

edenfrenkel commented 1 year ago

This issue was most likely a bug in an old Z3 version, probably Z3 version 4.8.17 - 64 bit, which is not currently used. In any case, it is no longer reproducible, so I'm closing the issue.