I am currently writing an automatic Verifier for my programming language on top of Z3 as a fun project and I am trying to use it to prove that a fibonacci implementation using a loop is equivalent to one with recursion.
It seems to work if the input program is correct, i.e. it generates reasonable input for Z3 and Z3 says it is unsatisfiable, which means in my context, that the program is correct. But when I changed one variable initialization and thereby render the program incorrect, my verifier came up with the following Z3 formula which doesn't seem too complicated to me, but Z3 says "unknown".
(set-option :smt.auto-config false)
(set-option :smt.mbqi false)
(declare-fun fib (Int) Int)
(declare-fun fakeFib (Int) Int)
(declare-fun n () Int)
(assert (forall ((n Int))
(! (= (fib n)
(ite (= n 0) 0
(ite (= n 1) 1
(+ (fakeFib (- n 1)) (fakeFib (- n 2))))))
:pattern ((fib n)))))
(assert (forall ((n Int))
(! (= (fib n) (fakeFib n)) :pattern ((fib n)))))
(assert (>= n 0))
(assert (not (and (<= 0 n) (= 1 (fib 1)) (= 1 (fib 0)))))
(check-sat)
Note that the two quantifiers represent the recursive definition of fibonacci. A friend of mine told me this trick to avoid a matching loop: Instead of defining fib as a recursive function, I introduce another function fakeFib for which I don't provide the definition and I use that one in the recursive definition of fib. Also, I tell the verifier that they are equal, but that quantifier only gets a pattern for fib, not for fakeFib. Because of the restrictive patterns, it is incomplete, i.e., it can only prove the correctness of the program as long as looking at one level of recursion suffices to prove it (but it can easily be extended to k levels). But I can live with that restriction in order to avoid matching loops.
The "bug" of the code was that I initialized a variable incorrectly and this eventually lead to the incorrect component (= 1 (fib 0)) in the last assertion. For the correct program, it would be (= 0 (fib 0)).
Some observations:
(= 1 (fib 0)) by (= 0 (fib 0)), then Z3 immediately finds that it is unsatisfiable.(set-option :smt.auto-config false) and (set-option :smt.mbqi false) set and then it ran out of memory on my machine and out of time on rise4fun.(set-option :smt.macro-finder true) which seems to have worked for people with similar questions didn't work for me. I am guessing that this is caused by the fact that I have two quantifiers for fib and not just one.(= 1 (fib 0)) is false, therefore the whole last assertion is automatically true. (>= n 0) is also easy to satisfy.I am not a Z3 expert but maybe I can shed a bit of light.
By disabling MBQI you are disabling the ability of Z3 to produce models for quantified formulas, so I guess that when Z3 cannot find a way to prove your problem unsatisfiable, it quickly reports it as unknown.
Note that a model for your problem needs to be satisfied by the four assertions, not only by the last two. As you point out Z3 cannot eliminate your first assert as if it were a macro, because you provide two definitions for fib n.
If you enable MBQI you will see that Z3 tries to find a model, and consumes quite a lot of memory on it! I presume that this is because the only way to satisfy your specification requires building the recursive function fib, feature that Z3 does not support.
how I will approach this
What you are doing right now it is a nice trick that allows Z3 to expand fib definition as much as needed in order to prove a problem unsat. But it does not play nice with the model finder, because you indirectly introduce a recursive definition.
So, if Z3 reports unsat then you know that your program is correct. If it reports unknown, you have to start an iterative process. Before this, you remove the second assert (= (fib n) (fakeFib n)) to prevent an infinite loop constructing the model.
fib, where fib(k+1) is abstracted in terms of fakeFib. You can leave fakeFib n unconstrained, or you may impose light constraints on it (e.g. must be a positive integer), without adding recursion.unsat, then your program is correct.sat, you must check whether the returned model is consistent with fib. If it is consistent, then you got a counterexample. If it is not consistent, then you increase k and goto step 1.You may want to read about k-induction, what I propose you is more or less that.