Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Strange output when reporting quantifier instantiations using newer Z3 versions #786

Open
dnezam opened this issue Dec 15, 2023 · 1 comment

Comments

@dnezam
Copy link

dnezam commented Dec 15, 2023

When using Z3 version 4.8.12-31 (Debian) or 4.12.4 (current upstream), running

./silicon.sh --numberOfParallelVerifiers 1 --z3Args "smt.qi.profile=true smt.qi.profile_freq=1" prog.vpr

prints

Invalid quantifier instances line from prover: [quantifier_instances] $Set[Int]_prog.equality_definition :      1 :   0 :   0 :   0 : 1

When using Z3 version 4.8.7, running the same command prints

[quantifier_instances] $Set[Int]_prog.equality_definition :      1 :   0 : 1

prog.vpr

function EmptySet(): Set[Int]
  ensures result == Set[Int]()
{
	Set[Int]()
}

In particular, the newer versions include Invalid quantifier instances line from prover and two extra columns after the quantifier name.

@dnezam
Copy link
Author

dnezam commented Dec 15, 2023

As a side note, I am not sure where I can find the documentation for the meaning of the columns. The only reference I could find was #587 which links to an issue on Z3 asking about the meaning of the 3 (instead of 5) columns after the name. Pointers in the right direction would be appreciated.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant