z3 smt example mini_ic3.py

Question

I have downloaded z3 and find a mini_ic3.py program? I think it is for ic3--an inductive invariant -based formal verification program.

is there some reference paper to recommend for understanding mini_ic3.py in z3 directory

Answer 1

Not much directly describing that particular implementation, I'm afraid. Your best bet is to read through https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-bounded-model-checking

The original IC3 papers themselves would help as well. The following is a great introduction: http://theory.stanford.edu/~arbrad/papers/Understanding_IC3.pdf