From d514291efafeef479b819af3f905f339c85086fb Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 16 Nov 2011 00:48:42 +0000 Subject: [PATCH] * Applying Andy's fix for datatypes bug #286; thanks for the quick work, Andy! * Also some better configure script wording --- config/bindings.m4 | 4 ++-- src/theory/datatypes/theory_datatypes.cpp | 3 ++- test/regress/regress0/datatypes/Makefile.am | 3 ++- test/regress/regress0/datatypes/bug286.cvc | 6 ++++++ 4 files changed, 12 insertions(+), 4 deletions(-) create mode 100644 test/regress/regress0/datatypes/bug286.cvc 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); -- 2.30.2