# define LIBRARY_MARKER ";;; Splint Library "
/*@constant int MAX_NAME_LENGTH=256; @*/
-# define MAX_NAME_LENGTH 256
+# define MAX_NAME_LENGTH 1024
/*@constant int MAX_LINE_LENGTH=1024; @*/
# define MAX_LINE_LENGTH 1024
*/
/*@constant float SPLINT_LIBVERSION; @*/
-# define SPLINT_LIBVERSION 2.6
+# define SPLINT_LIBVERSION 2.7
/*
** Flex doesn't pre-process input, so remember to copy these manually