test/regress/regress0/bug486.cvc

   1 % COMMAND-LINE: --finite-model-find -i
   2 % EXPECT: not_entailed
   3 % EXPECT: entailed
   4 prin:TYPE;
   5 form:TYPE;
   6
   7 signed:(prin,form)->BOOLEAN;
   8 says:(prin,form)->BOOLEAN;
   9
  10 speaksfor:(prin,prin)->form;
  11 signedE:BOOLEAN = FORALL(x:prin,y:form) : signed(x,y) => says(x,y);
  12 saysE:BOOLEAN = FORALL(x,y:prin,z:form) : says(x,speaksfor(y,x)) AND says(y,z) => says(x,z);
  13
  14 ASSERT(signedE);
  15 ASSERT(saysE);
  16
  17 julie:prin;
  18 dave:prin;
  19 alice:prin;
  20 openfile:form;
  21
  22 x2:BOOLEAN = signed(alice,openfile);
  23 ASSERT(x2);
  24 x3:BOOLEAN = signed(dave,speaksfor(alice,dave));
  25 ASSERT(x3);
  26
  27 QUERY NOT says(dave,openfile); % this is invalid
  28 QUERY says(dave,openfile); % this is valid