viperproject/silicon

Strange output when reporting quantifier instantiations using newer Z3 versions

dnezam opened this issue · 1 comments

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.

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.