Does not work on z3 logs generated using Silicon

[Jankoekenpan]

I have a 2gb z3.log file generated using .\silicon --numberOfParallelVerifiers 1 --z3Args """""trace=true proof=true""""" --z3Exe ..\..\STMCors\deps\z3\4.8.6\z3.exe .\temp.sil

The file temp.sil passes verification:

Silicon finished verification successfully in 02m:20s.

Yet, axiom-profiler produces a dialog box stating that an array contains no elements, but after clicking OK, it shows a bunch of quantifiers, but the number of instances are all 0.

I can't upload the log file here because it is over 2gb in size, but I attached the temp.sil silver file that was used as an input for Silicon (renamed as temp.txt, because GitHub won't accept files ending with .sil).
temp.txt

[bobismijnnaam]

I investigated a bit more, here's a summary of what I've found.

First, here are the files of interest:

• I used the viper input file from Jan above.
• The smt2 files produced by viper, in case someone needs them in the future
  • jan_repro.smt2-00.smt2.txt
  • jan_repro.smt2-01.smt2.txt
• A log file, truncated from 4G to 2.6MB. I guess we are lucky the first problem is always around 80.000 lines into the log!
  • jan_repro.z3.486.log

These files were procured using the following command:

$ ~/Workbench/Tools/silicon/silicon.sh --z3Exe $(which z3) --numberOfParallelVerifiers 1 --z3Args "trace=true proof=true" --z3LogFile jan_repro.smt2 jan_repro.sil
Silicon 1.1-SNAPSHOT (c3dc27c0)
Silicon finished verification successfully in 57.47s.
$ z3 --version
Z3 version 4.8.7 - 64 bit

The problem in the log files is that I think there's a cycle in the equality relation that's reported there. I instrumented axiom profiler with many Console.WriteLines, which yields the following output:

Line count: 79434
Parsing line...
Parse trace line
[new-match]
Model call...
Ok.
Get binding info...
endIndex: 10
Bindings.Select... 4
GetExplanationToRoot
Done or break
TransitiveEqExpl
Transitive Equality constructor...
Ok.
Ok.
GetExplanationToRoot
Done or break
TransitiveEqExpl
Transitive Equality constructor...
Ok.
Ok.
GetExplanationToRoot
Done or break
TransitiveEqExpl
Transitive Equality constructor...
Ok.
Ok.
GetExplanationToRoot
-Id: 7588
Id: 26779
Current Id: 7588

Line count here indicates the line number axiom profiler is on, and [new-match] the type of the current line. Everything below that is just tracing the call stack of axiom profiler. Then, at the end, it enters GetExplanationToRoot. This method gets stuck on a cycle in the equality relation. Specifically, between ids 7588 and 26779. This can be seen in the log file as well:

$ grep -E "(7588|26779)" jan_repro.z3.486.log
...
[mk-app] #26780 = #7588 #26779
...
[mk-app] #27047 = #26779 #7588
...

I tried adding a break statement whenever such a cycle is encountered, but then axiom profiler hangs further down on some part of reconstructing the explanation. So if there is an easy fix like just putting break somewhere, it needs to be applied in more places than just GetExplanationToRoot.

I'm not sure how to proceed here. My gut feeling is that z3 shouldn't output cycles in the log, but I don't know both axiom profiler & z3 well enough to be sure about this. Filing a bug with z3 is a bit difficult because the repro file from Jan is, afaict, too difficult to minimize. FWIW, I tried with z3 4.8.17, which exhibits the exact same behavior, except that the equality cycle is established in only one step (the log contains something like [mk-app] #X = #Y #Y). Oh, also, in that case verification of the repro file actually fails, but I don't think that really matters for this bug.

If anyone could provide further guidance on how to minimize Jan's example further, or could give some idea about if it would be useful to file a bug with the z3 team, that would be great.

Finally, I think this bug is an instance of #35, so we could close that one in favour of this one.

[bobismijnnaam]

I did another round of debugging with another input file of mine. This time I'm pretty sure I pinpointed the exact statement after which axiom profiler freezes. Specifically:

• I started with summation.vpr, which when run with viper produces summation-00.smt2 and summation-01.smt2.
• If you run summation-01.smt2 in through z3 this results in a 9 gigabyte log file, summation-01.log.
• If you cut summation-01.log off just before line 43386, meaning, not including line 43386, axiom profiler imports it just fine within a second.
• If you cut summation-01.log off just after line 43386, meaning, including line 43386 but nothing after it, axiom profiler freezes.

These files are included with the zips below.

I've reproduced this a few times now, both with different viper input files, as well as between different runs of the same viper input file. I haven't been able to eyeball detect any syntactic similarities between any of the log files. The only thing they have in common is that the line that causes the freeze is usually before line 50.000 or so. This means the axiom-profiler freeze happens somewhere between the 5th and the 10th check-sat (which doesn't matter much, except that we're lucky because this means the log files at that point are around a few megabytes).

I also tried to cut out the section between [begin-check]s where the freezing occurs, but it doesn't seem to help.

As far as I know, axiom profiler is the only way to analyze z3's behaviour w.r.t. quantifiers, so I'd really like to use it to get some hints to optimize my viper/vercors file. The statistics in viper's smt output indicate that my viper program is somehow generating tons of quantifier instantiations. Any thoughts on this are also very welcome; if people use other tricks to analyze or optimize their quantifiers I would love to hear about them!

Technical info 1

package1.zip

Silicon commit: 3f8bd55d3cbc3a8fbe73aa68a62c872218159b06

Silicon command:

$ ~/Workbench/Tools/silicon/silicon.sh --z3Exe $(which z3) --proverLogFile summation --numberOfParallelVerifiers 1 summation.vpr

z3 command:

$ z3 trace=true proof=true trace-file-name=summation.log ./summation-01.smt2

Z3 version: 4.8.7 - 64 bit

Technical info 2

package2.zip

Here's another log file I minimized. It's produced in the same way as the files above, but has different contents. In this log file axiom profiler freezes about 80 log file entries after a [begin-check]. As it might be easier to debug axiom profiler with this file I'm including it as well.