Existence of 0: "failed to find a pattern for quantifier"

Mar 18, 2011 at 12:38 PM
Edited Mar 18, 2011 at 12:39 PM

Hi, I'm trying to show that there is an unsigned int equalling "0".


~/sandbox/elementary/existence$ cat ex0.c 
#include "vcc.h"

void test() 
    _(assert \exists unsigned int i; i == 0)
~/sandbox/elementary/existence$ vcc /2 ex0.c 
Verification of test failed.
Prover warning: failed to find a pattern for quantifier (quantifier id: ex0c.5:28)
p:\tool\vcc\sandbox\elementary\existence\ex0.c(5,28) : error VC9500: Assertion '\exists unsigned int i; i == 0)' did not verify.
Exiting with 3 (1 error(s).)


Which trigger/annotation do I need to prove it?

Thanks, Holger

Mar 22, 2011 at 6:38 PM

Hi Holger,

  "vcc /2 /z:SATURATE=true" seems to prove it, other than that I'm not aware of a way to make it work... Unfortunately, I also don't know where to find additional info on Z3's saturate flag...

  Best, Mark