Hi,

I am tring to verify some case with \exists quantifier. But I always get the error infor. I even get the error message for the simplest case. What can I do to handle this?

I tried to add some triggers like: \match_ulong(t) to get rid of the warnings. But it doesn't work for error message.

Thanks very much!

#include<vcc.h>

void test(){
    _(assert \exists unsigned t; \true)
}

/*
=== VCC started. ===
Command Line: "C:\Program Files (x86)\Microsoft Research\Vcc\Binaries\vcc.exe"  /bvd /loc:"c:\Users\Hare\documents\visual studio 2010\Projects\Vcc-test\Vcc-test\test.h":4  "c:\Users\Hare\documents\visual studio 2010\Projects\Vcc-test\Vcc-test\test.h" /p:/D_MBCS  /clpath:"C:\PROGRAM FILES (X86)\MICROSOFT VISUAL STUDIO 10.0\VC\bin\cl.exe"

c:\Users\Hare\documents\visual studio 2010\Projects\Vcc-test\Vcc-test\test.h(4,14) : warning VC9121: failed to infer triggers for '\exists unsigned t; \true)'
Verification of test failed. [0.64]
Prover warning: failed to find a pattern for quantifier (quantifier id: testh.4:14)
c:\Users\Hare\documents\visual studio 2010\Projects\Vcc-test\Vcc-test\test.h(4,14) : error VC9500: Assertion '\exists unsigned t; \true)' did not verify.
Verification errors in 1 function(s)
Exiting with 3 (1 error(s).)

=== Verification failed. ===
*/

Hi Hare,

I don't have any answers to offer you right now, but you (and any devs looking into this) may be interested in the follwing facts:

• The following succeeds.
  
  

  #include<vcc.h>
  
  void test(){
      _(assert \exists \integer t; \true)
  }
  

• The following fails.
  
  

  #include<vcc.h>
  
  void test(){
  _(assert \exists \natural t; \true)
  } 
  

• The following succeeds (with the usual trigger warning).
  
  

  #include<vcc.h>
  
  void test(){
      _(assert \exists \integer t; 0 <= t ==> \true)
  } 

In the meantime, I would advise using \integer variables in everything spec, and casting where appropriate. If you need the fact that it's non-negative, you can easily switch between \natural and \integer with a side-condition, although you'll have to add explicit casts where appropriate.

Cheers,

Francois

Hi Francois,

Thanks very much!

Shu Cheng

Hi Francois,

When I go back to my case, it seems \integer also can't help. For instance,

#include<vcc.h>

void test(){
    _(assert \exists \integer t; t == 5)
}

void test1(){
    int x = 25;
    
    _(assert \exists \integer t; t == 5 ==> x == t * t)
    _(assert \exists \integer t; x == t * t)
    _(assert \exists \integer t; t == 5)
}

void test2(){
    int x = 25;

    _(assert \forall \integer t; t == 5 ==> x == t * t)
    _(assert \exists \integer t; t == 5 ==> x == t * t)
}

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)
}