1 files changed, 25 insertions, 0 deletions
diff --git a/test/regress/regress0/bug486.cvc b/test/regress/regress0/bug486.cvc
new file mode 100644
index 000000000..6e8ee0018
--- /dev/null
+++ b/test/regress/regress0/bug486.cvc
@@ -0,0 +1,25 @@
+prin:TYPE;
+form:TYPE;
+
+signed:(prin,form)->BOOLEAN;
+says:(prin,form)->BOOLEAN;
+
+speaksfor:(prin,prin)->form;
+signedE:BOOLEAN = FORALL(x:prin,y:form) : signed(x,y) => says(x,y);
+saysE:BOOLEAN = FORALL(x,y:prin,z:form) : says(x,speaksfor(y,x)) AND says(y,z) => says(x,z); 
+
+ASSERT(signedE);
+ASSERT(saysE);
+
+julie:prin;
+dave:prin;
+alice:prin;
+openfile:form;
+
+x2:BOOLEAN = signed(alice,openfile);
+ASSERT(x2);
+x3:BOOLEAN = signed(dave,speaksfor(alice,dave));
+ASSERT(x3);
+
+QUERY NOT says(dave,openfile); % this is invalid
+QUERY says(dave,openfile); % this is valid