From 04d8d1a3336633b0665a29d4a6e25828a6674a36 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 23 Jan 2013 17:00:56 -0500
Subject: partially address bug 486: allow some model inspection of quantifiers

---
 test/regress/regress0/Makefile.am |  3 ++-
 test/regress/regress0/bug486.cvc  | 25 +++++++++++++++++++++++++
 2 files changed, 27 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress0/bug486.cvc

(limited to 'test/regress/regress0')

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 3b30a8d9e..d5b35594f 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -149,7 +149,8 @@ TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
 EXTRA_DIST = $(TESTS) \
 	simplification_bug4.smt2.expect \
-	bug216.smt2.expect
+	bug216.smt2.expect \
+	bug486.cvc
 
 if CVC4_BUILD_PROFILE_COMPETITION
 else
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
-- 
cgit v1.2.3