Developer
Sep 11, 2012 at 4:39 PM
Edited Sep 11, 2012 at 4:43 PM

It's important to understand how VCC (and more generally, SMT solvers) treat quantifiers. When VCC needs to prove a formula, it first negates and Skolemizes it, and tries to prove \false. It will have two kinds of formulas to use: ground formulas and formulas
with quantifiers. It reasons only with the ground formulas, using (essentially) logic and linear arithmetic. A quantified formula is used only by matching its trigger(s) using ground subterms in its formulas to obtain a ground instance, and adding this instance
to the collection of ground formulas.
So, for example, if you want to prove (\exists \integer t; t == 5), it will actually have the formula
(\forall \integer t; t != 5)
which it will use to try to prove \false. Even if you had given the existential formula a trigger, to obtain a formula like
(\forall \integer t; {\match_long(t)} t != 5)
it will still fail to prove this because it has no ground term of the form \match_long(a) with which to instantiate the formula. To get it to trigger, you have to provide a ground instance, for example as follows (which verifies):
#include <vcc.h>
_(def \bool match(\integer t) { return \true; })
void test(){
_(assert match(5))
_(assert \exists \integer t; {match(t)} t == 5)
}
void test1(){
int x = 25;
_(assert match(5))
_(assert \exists \integer t; {match(t)} t == 5 ==> x == t * t)
_(assert \exists \integer t; {match(t)} x == t * t)
_(assert \exists \integer t; {match(t)} t == 5)
}
void test2(){
int x = 25;
_(assert match(5))
_(assert \forall \integer t; {match(t)} t == 5 ==> x == t * t)
_(assert \exists \integer t; {match(t)} t == 5 ==> x == t * t)
}
