From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 16 Nov 2011 00:48:42 +0000 (+0000)
Subject: * Applying Andy's fix for datatypes bug #286; thanks for the quick work, Andy!
X-Git-Tag: cvc5-1.0.0~8381
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d514291efafeef479b819af3f905f339c85086fb;p=cvc5.git

* Applying Andy's fix for datatypes bug #286; thanks for the quick work, Andy!
* Also some better configure script wording
---

diff --git a/config/bindings.m4 b/config/bindings.m4
index 416a338da..5306c8c77 100644
--- a/config/bindings.m4
+++ b/config/bindings.m4
@@ -143,9 +143,9 @@ else
       esac
       if test "$binding_error" = yes; then
         if test "$cvc4_check_for_bindings" = no; then
-          AC_MSG_ERROR([Language binding \`$binding' requested by user, but it cannot be built.])
+          AC_MSG_ERROR([Language binding \`$binding' requested by user, but it cannot be built (the preceding few lines should give an indication why this is).])
         else
-          AC_MSG_WARN([Language binding \`$binding' cannot be built.])
+          AC_MSG_WARN([Language binding \`$binding' cannot be built (the preceding few lines should give an indication why this is).])
         fi
       else
         CVC4_LANGUAGE_BINDINGS="${CVC4_LANGUAGE_BINDINGS:+$CVC4_LANGUAGE_BINDINGS }$binding"
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 08b142fe3..6b067c681 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -854,7 +854,8 @@ void TheoryDatatypes::merge(TNode a, TNode b) {
 }
 
 void TheoryDatatypes::addTermToLabels( Node t ) {
-  if( t.getKind() == VARIABLE || t.getKind() == APPLY_SELECTOR ) {
+  if( ( t.getKind() == VARIABLE || t.getKind() == APPLY_SELECTOR ) &&
+      t.getType().isDatatype() ) {
     Node tmp = find( t );
     if( tmp == t ) {
       //add to labels
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index aa9b9ce0b..c4a4e2fdd 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -31,7 +31,8 @@ TESTS =	\
 	v1l20009.cvc \
 	v2l40025.cvc \
 	v3l60006.cvc \
-	v5l30058.cvc
+	v5l30058.cvc \
+	bug286.cvc
 
 
 EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/datatypes/bug286.cvc b/test/regress/regress0/datatypes/bug286.cvc
new file mode 100644
index 000000000..d9b4d8287
--- /dev/null
+++ b/test/regress/regress0/datatypes/bug286.cvc
@@ -0,0 +1,6 @@
+% EXPECT: invalid
+% EXIT: 10
+DATATYPE foo = f(i:INT) END;
+x : foo;
+y : INT;
+QUERY x = f(y);