From: Tim King <taking@cs.nyu.edu>
Date: Sat, 19 May 2012 17:45:37 +0000 (+0000)
Subject: Adding regress test for bug 341.
X-Git-Tag: cvc5-1.0.0~8150
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=50ad9f07cb754c2c09a4775e1bc73230f440cfed;p=cvc5.git

Adding regress test for bug 341.
---

diff --git a/test/regress/regress0/datatypes/bug341.cvc b/test/regress/regress0/datatypes/bug341.cvc
new file mode 100644
index 000000000..f6f810893
--- /dev/null
+++ b/test/regress/regress0/datatypes/bug341.cvc
@@ -0,0 +1,6 @@
+% EXPECT: invalid
+% EXIT: 10
+
+f : [0..2] ->  INT;
+
+QUERY( f(0) = 0 );