Strange output when reporting quantifier instantiations using newer Z3 versions
dnezam opened this issue · 1 comments
dnezam commented
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 commented
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.