Do not compile SMT parser by default. Removed automatically generated

parser files: We really don't want SVN to keep track of changes in
these files while working on the parser.



git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73132 91177308-0d34-0410-b5e6-96231b3b80d8

4 files changed, 1 insertions, 4366 deletions

diff --git a/lib/Makefile b/lib/Makefile
index fa5ab9d4..ec0d1634 100644
--- a/lib/Makefile
+++ b/lib/Makefile
@@ -9,7 +9,6 @@
 
 LEVEL=..
 
-PARALLEL_DIRS=Basic Support SMT Expr Solver Module Core
+PARALLEL_DIRS=Basic Support Expr Solver Module Core
 
 include $(LEVEL)/Makefile.common
-
diff --git a/lib/SMT/smtlib_lexer.cpp b/lib/SMT/smtlib_lexer.cpp
deleted file mode 100644
index f8a2b329..00000000
--- a/lib/SMT/smtlib_lexer.cpp
+++ /dev/null
@@ -1,2364 +0,0 @@
-#line 2 "smtlib_lexer.cpp"
-
-#line 4 "smtlib_lexer.cpp"
-
-#define  YY_INT_ALIGNED short int
-
-/* A lexical scanner generated by flex */
-
-#define yy_create_buffer smtlib_create_buffer
-#define yy_delete_buffer smtlib_delete_buffer
-#define yy_flex_debug smtlib_flex_debug
-#define yy_init_buffer smtlib_init_buffer
-#define yy_flush_buffer smtlib_flush_buffer
-#define yy_load_buffer_state smtlib_load_buffer_state
-#define yy_switch_to_buffer smtlib_switch_to_buffer
-#define yyin smtlibin
-#define yyleng smtlibleng
-#define yylex smtliblex
-#define yylineno smtliblineno
-#define yyout smtlibout
-#define yyrestart smtlibrestart
-#define yytext smtlibtext
-#define yywrap smtlibwrap
-#define yyalloc smtliballoc
-#define yyrealloc smtlibrealloc
-#define yyfree smtlibfree
-
-#define FLEX_SCANNER
-#define YY_FLEX_MAJOR_VERSION 2
-#define YY_FLEX_MINOR_VERSION 5
-#define YY_FLEX_SUBMINOR_VERSION 35
-#if YY_FLEX_SUBMINOR_VERSION > 0
-#define FLEX_BETA
-#endif
-
-/* First, we deal with  platform-specific or compiler-specific issues. */
-
-/* begin standard C headers. */
-#include <stdio.h>
-#include <string.h>
-#include <errno.h>
-#include <stdlib.h>
-
-/* end standard C headers. */
-
-/* flex integer type definitions */
-
-#ifndef FLEXINT_H
-#define FLEXINT_H
-
-/* C99 systems have <inttypes.h>. Non-C99 systems may or may not. */
-
-#if defined (__STDC_VERSION__) && __STDC_VERSION__ >= 199901L
-
-/* C99 says to define __STDC_LIMIT_MACROS before including stdint.h,
- * if you want the limit (max/min) macros for int types. 
- */
-#ifndef __STDC_LIMIT_MACROS
-#define __STDC_LIMIT_MACROS 1
-#endif
-
-#include <inttypes.h>
-typedef int8_t flex_int8_t;
-typedef uint8_t flex_uint8_t;
-typedef int16_t flex_int16_t;
-typedef uint16_t flex_uint16_t;
-typedef int32_t flex_int32_t;
-typedef uint32_t flex_uint32_t;
-#else
-typedef signed char flex_int8_t;
-typedef short int flex_int16_t;
-typedef int flex_int32_t;
-typedef unsigned char flex_uint8_t; 
-typedef unsigned short int flex_uint16_t;
-typedef unsigned int flex_uint32_t;
-#endif /* ! C99 */
-
-/* Limits of integral types. */
-#ifndef INT8_MIN
-#define INT8_MIN               (-128)
-#endif
-#ifndef INT16_MIN
-#define INT16_MIN              (-32767-1)
-#endif
-#ifndef INT32_MIN
-#define INT32_MIN              (-2147483647-1)
-#endif
-#ifndef INT8_MAX
-#define INT8_MAX               (127)
-#endif
-#ifndef INT16_MAX
-#define INT16_MAX              (32767)
-#endif
-#ifndef INT32_MAX
-#define INT32_MAX              (2147483647)
-#endif
-#ifndef UINT8_MAX
-#define UINT8_MAX              (255U)
-#endif
-#ifndef UINT16_MAX
-#define UINT16_MAX             (65535U)
-#endif
-#ifndef UINT32_MAX
-#define UINT32_MAX             (4294967295U)
-#endif
-
-#endif /* ! FLEXINT_H */
-
-#ifdef __cplusplus
-
-/* The "const" storage-class-modifier is valid. */
-#define YY_USE_CONST
-
-#else	/* ! __cplusplus */
-
-/* C99 requires __STDC__ to be defined as 1. */
-#if defined (__STDC__)
-
-#define YY_USE_CONST
-
-#endif	/* defined (__STDC__) */
-#endif	/* ! __cplusplus */
-
-#ifdef YY_USE_CONST
-#define yyconst const
-#else
-#define yyconst
-#endif
-
-/* Returned upon end-of-file. */
-#define YY_NULL 0
-
-/* Promotes a possibly negative, possibly signed char to an unsigned
- * integer for use as an array index.  If the signed char is negative,
- * we want to instead treat it as an 8-bit unsigned char, hence the
- * double cast.
- */
-#define YY_SC_TO_UI(c) ((unsigned int) (unsigned char) c)
-
-/* Enter a start condition.  This macro really ought to take a parameter,
- * but we do it the disgusting crufty way forced on us by the ()-less
- * definition of BEGIN.
- */
-#define BEGIN (yy_start) = 1 + 2 *
-
-/* Translate the current start state into a value that can be later handed
- * to BEGIN to return to the state.  The YYSTATE alias is for lex
- * compatibility.
- */
-#define YY_START (((yy_start) - 1) / 2)
-#define YYSTATE YY_START
-
-/* Action number for EOF rule of a given start state. */
-#define YY_STATE_EOF(state) (YY_END_OF_BUFFER + state + 1)
-
-/* Special action meaning "start processing a new file". */
-#define YY_NEW_FILE smtlibrestart(smtlibin  )
-
-#define YY_END_OF_BUFFER_CHAR 0
-
-/* Size of default input buffer. */
-#ifndef YY_BUF_SIZE
-#define YY_BUF_SIZE 16384
-#endif
-
-/* The state buf must be large enough to hold one state per character in the main buffer.
- */
-#define YY_STATE_BUF_SIZE   ((YY_BUF_SIZE + 2) * sizeof(yy_state_type))
-
-#ifndef YY_TYPEDEF_YY_BUFFER_STATE
-#define YY_TYPEDEF_YY_BUFFER_STATE
-typedef struct yy_buffer_state *YY_BUFFER_STATE;
-#endif
-
-extern int smtlibleng;
-
-extern FILE *smtlibin, *smtlibout;
-
-#define EOB_ACT_CONTINUE_SCAN 0
-#define EOB_ACT_END_OF_FILE 1
-#define EOB_ACT_LAST_MATCH 2
-
-    /* Note: We specifically omit the test for yy_rule_can_match_eol because it requires
-     *       access to the local variable yy_act. Since yyless() is a macro, it would break
-     *       existing scanners that call yyless() from OUTSIDE smtliblex. 
-     *       One obvious solution it to make yy_act a global. I tried that, and saw
-     *       a 5% performance hit in a non-smtliblineno scanner, because yy_act is
-     *       normally declared as a register variable-- so it is not worth it.
-     */
-    #define  YY_LESS_LINENO(n) \
-            do { \
-                int yyl;\
-                for ( yyl = n; yyl < smtlibleng; ++yyl )\
-                    if ( smtlibtext[yyl] == '\n' )\
-                        --smtliblineno;\
-            }while(0)
-    
-/* Return all but the first "n" matched characters back to the input stream. */
-#define yyless(n) \
-	do \
-		{ \
-		/* Undo effects of setting up smtlibtext. */ \
-        int yyless_macro_arg = (n); \
-        YY_LESS_LINENO(yyless_macro_arg);\
-		*yy_cp = (yy_hold_char); \
-		YY_RESTORE_YY_MORE_OFFSET \
-		(yy_c_buf_p) = yy_cp = yy_bp + yyless_macro_arg - YY_MORE_ADJ; \
-		YY_DO_BEFORE_ACTION; /* set up smtlibtext again */ \
-		} \
-	while ( 0 )
-
-#define unput(c) yyunput( c, (yytext_ptr)  )
-
-#ifndef YY_TYPEDEF_YY_SIZE_T
-#define YY_TYPEDEF_YY_SIZE_T
-typedef size_t yy_size_t;
-#endif
-
-#ifndef YY_STRUCT_YY_BUFFER_STATE
-#define YY_STRUCT_YY_BUFFER_STATE
-struct yy_buffer_state
-	{
-	FILE *yy_input_file;
-
-	char *yy_ch_buf;		/* input buffer */
-	char *yy_buf_pos;		/* current position in input buffer */
-
-	/* Size of input buffer in bytes, not including room for EOB
-	 * characters.
-	 */
-	yy_size_t yy_buf_size;
-
-	/* Number of characters read into yy_ch_buf, not including EOB
-	 * characters.
-	 */
-	int yy_n_chars;
-
-	/* Whether we "own" the buffer - i.e., we know we created it,
-	 * and can realloc() it to grow it, and should free() it to
-	 * delete it.
-	 */
-	int yy_is_our_buffer;
-
-	/* Whether this is an "interactive" input source; if so, and
-	 * if we're using stdio for input, then we want to use getc()
-	 * instead of fread(), to make sure we stop fetching input after
-	 * each newline.
-	 */
-	int yy_is_interactive;
-
-	/* Whether we're considered to be at the beginning of a line.
-	 * If so, '^' rules will be active on the next match, otherwise
-	 * not.
-	 */
-	int yy_at_bol;
-
-    int yy_bs_lineno; /**< The line count. */
-    int yy_bs_column; /**< The column count. */
-    
-	/* Whether to try to fill the input buffer when we reach the
-	 * end of it.
-	 */
-	int yy_fill_buffer;
-
-	int yy_buffer_status;
-
-#define YY_BUFFER_NEW 0
-#define YY_BUFFER_NORMAL 1
-	/* When an EOF's been seen but there's still some text to process
-	 * then we mark the buffer as YY_EOF_PENDING, to indicate that we
-	 * shouldn't try reading from the input source any more.  We might
-	 * still have a bunch of tokens to match, though, because of
-	 * possible backing-up.
-	 *
-	 * When we actually see the EOF, we change the status to "new"
-	 * (via smtlibrestart()), so that the user can continue scanning by
-	 * just pointing smtlibin at a new input file.
-	 */
-#define YY_BUFFER_EOF_PENDING 2
-
-	};
-#endif /* !YY_STRUCT_YY_BUFFER_STATE */
-
-/* Stack of input buffers. */
-static size_t yy_buffer_stack_top = 0; /**< index of top of stack. */
-static size_t yy_buffer_stack_max = 0; /**< capacity of stack. */
-static YY_BUFFER_STATE * yy_buffer_stack = 0; /**< Stack as an array. */
-
-/* We provide macros for accessing buffer states in case in the
- * future we want to put the buffer states in a more general
- * "scanner state".
- *
- * Returns the top of the stack, or NULL.
- */
-#define YY_CURRENT_BUFFER ( (yy_buffer_stack) \
-                          ? (yy_buffer_stack)[(yy_buffer_stack_top)] \
-                          : NULL)
-
-/* Same as previous macro, but useful when we know that the buffer stack is not
- * NULL or when we need an lvalue. For internal use only.
- */
-#define YY_CURRENT_BUFFER_LVALUE (yy_buffer_stack)[(yy_buffer_stack_top)]
-
-/* yy_hold_char holds the character lost when smtlibtext is formed. */
-static char yy_hold_char;
-static int yy_n_chars;		/* number of characters read into yy_ch_buf */
-int smtlibleng;
-
-/* Points to current character in buffer. */
-static char *yy_c_buf_p = (char *) 0;
-static int yy_init = 0;		/* whether we need to initialize */
-static int yy_start = 0;	/* start state number */
-
-/* Flag which is used to allow smtlibwrap()'s to do buffer switches
- * instead of setting up a fresh smtlibin.  A bit of a hack ...
- */
-static int yy_did_buffer_switch_on_eof;
-
-void smtlibrestart (FILE *input_file  );
-void smtlib_switch_to_buffer (YY_BUFFER_STATE new_buffer  );
-YY_BUFFER_STATE smtlib_create_buffer (FILE *file,int size  );
-void smtlib_delete_buffer (YY_BUFFER_STATE b  );
-void smtlib_flush_buffer (YY_BUFFER_STATE b  );
-void smtlibpush_buffer_state (YY_BUFFER_STATE new_buffer  );
-void smtlibpop_buffer_state (void );
-
-static void smtlibensure_buffer_stack (void );
-static void smtlib_load_buffer_state (void );
-static void smtlib_init_buffer (YY_BUFFER_STATE b,FILE *file  );
-
-#define YY_FLUSH_BUFFER smtlib_flush_buffer(YY_CURRENT_BUFFER )
-
-YY_BUFFER_STATE smtlib_scan_buffer (char *base,yy_size_t size  );
-YY_BUFFER_STATE smtlib_scan_string (yyconst char *yy_str  );
-YY_BUFFER_STATE smtlib_scan_bytes (yyconst char *bytes,int len  );
-
-void *smtliballoc (yy_size_t  );
-void *smtlibrealloc (void *,yy_size_t  );
-void smtlibfree (void *  );
-
-#define yy_new_buffer smtlib_create_buffer
-
-#define yy_set_interactive(is_interactive) \
-	{ \
-	if ( ! YY_CURRENT_BUFFER ){ \
-        smtlibensure_buffer_stack (); \
-		YY_CURRENT_BUFFER_LVALUE =    \
-            smtlib_create_buffer(smtlibin,YY_BUF_SIZE ); \
-	} \
-	YY_CURRENT_BUFFER_LVALUE->yy_is_interactive = is_interactive; \
-	}
-
-#define yy_set_bol(at_bol) \
-	{ \
-	if ( ! YY_CURRENT_BUFFER ){\
-        smtlibensure_buffer_stack (); \
-		YY_CURRENT_BUFFER_LVALUE =    \
-            smtlib_create_buffer(smtlibin,YY_BUF_SIZE ); \
-	} \
-	YY_CURRENT_BUFFER_LVALUE->yy_at_bol = at_bol; \
-	}
-
-#define YY_AT_BOL() (YY_CURRENT_BUFFER_LVALUE->yy_at_bol)
-
-/* Begin user sect3 */
-
-#define smtlibwrap(n) 1
-#define YY_SKIP_YYWRAP
-
-typedef unsigned char YY_CHAR;
-
-FILE *smtlibin = (FILE *) 0, *smtlibout = (FILE *) 0;
-
-typedef int yy_state_type;
-
-extern int smtliblineno;
-
-int smtliblineno = 1;
-
-extern char *smtlibtext;
-#define yytext_ptr smtlibtext
-
-static yy_state_type yy_get_previous_state (void );
-static yy_state_type yy_try_NUL_trans (yy_state_type current_state  );
-static int yy_get_next_buffer (void );
-static void yy_fatal_error (yyconst char msg[]  );
-
-/* Done after the current pattern has been matched and before the
- * corresponding action - sets up smtlibtext.
- */
-#define YY_DO_BEFORE_ACTION \
-	(yytext_ptr) = yy_bp; \
-	smtlibleng = (size_t) (yy_cp - yy_bp); \
-	(yy_hold_char) = *yy_cp; \
-	*yy_cp = '\0'; \
-	(yy_c_buf_p) = yy_cp;
-
-#define YY_NUM_RULES 67
-#define YY_END_OF_BUFFER 68
-/* This struct is not used in this scanner,
-   but its presence is necessary. */
-struct yy_trans_info
-	{
-	flex_int32_t yy_verify;
-	flex_int32_t yy_nxt;
-	};
-static yyconst flex_int16_t yy_accept[240] =
-    {   0,
-        0,    0,    0,    0,    0,    0,    0,    0,    0,    0,
-       68,   66,    2,    1,    8,   64,   62,   60,   61,    4,
-       55,    5,   63,   65,   56,   57,   65,   65,   65,   65,
-       65,   65,   65,   65,   65,   65,   65,   65,   65,   65,
-       65,   14,   59,    7,    6,   11,   67,   10,   11,   18,
-       17,   18,   16,   55,   58,   13,   64,    0,    4,    0,
-       65,   65,   65,   65,   65,   65,   65,   65,   65,   65,
-       65,   65,   65,   65,   65,   65,   65,   65,   65,   65,
-       26,   65,   65,   65,   65,   65,   65,   65,    9,   15,
-        0,    3,    0,   25,   65,   65,   65,   65,   65,   65,
-
-       65,   65,   65,   65,   65,   65,   65,   28,   65,   21,
-       65,   31,   65,   22,   65,   42,   65,   65,   65,   65,
-       65,   27,    0,   12,   65,   65,   65,   65,   65,   65,
-       65,   65,   65,   65,   32,   65,   65,   36,   65,   65,
-       65,   65,   65,   65,   65,   65,   19,   65,   65,    0,
-        0,   65,   65,   65,   65,   65,   65,   65,   65,   65,
-       20,   65,   65,   65,   65,   65,   41,   33,   37,   35,
-       65,   65,   43,    0,   65,   40,   65,   65,   65,   65,
-       29,   65,   65,   65,   65,   30,   65,   65,   65,   65,
-       47,   65,    0,   65,   65,   65,   65,   65,   65,   65,
-
-       65,   65,   46,   65,   23,   65,   44,   54,   65,   65,
-       65,   65,   53,   65,   65,   65,   65,   65,   52,   65,
-       48,   65,   65,   65,   50,   65,   65,   65,   45,   65,
-       39,   38,   51,   49,   65,   34,   65,   24,    0
-    } ;
-
-static yyconst flex_int32_t yy_ec[256] =
-    {   0,
-        1,    1,    1,    1,    1,    1,    1,    1,    2,    3,
-        1,    2,    2,    1,    1,    1,    1,    1,    1,    1,
-        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
-        1,    2,    1,    4,    5,    6,    5,    5,    7,    8,
-        9,    5,    5,    1,    5,   10,    5,   11,   11,   11,
-       11,   11,   11,   11,   11,   11,   11,   12,   13,    5,
-        5,    5,   14,    5,   15,   15,   15,   15,   15,   15,
-       15,   15,   15,   15,   15,   15,   15,   15,   15,   15,
-       15,   15,   15,   15,   15,   15,   15,   15,   15,   15,
-       16,   17,   18,    1,   19,    1,   20,   21,   22,   23,
-
-       24,   25,   26,   27,   28,   15,   29,   30,   31,   32,
-       33,   34,   15,   35,   36,   37,   38,   39,   40,   41,
-       15,   15,   42,    5,   43,    5,    1,    1,    1,    1,
-        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
-        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
-        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
-        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
-        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
-        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
-        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
-
-        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
-        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
-        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
-        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
-        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
-        1,    1,    1,    1,    1
-    } ;
-
-static yyconst flex_int32_t yy_meta[44] =
-    {   0,
-        1,    1,    2,    1,    1,    1,    3,    1,    1,    3,
-        3,    1,    1,    1,    3,    1,    1,    1,    3,    3,
-        3,    3,    3,    3,    3,    3,    3,    3,    3,    3,
-        3,    3,    3,    3,    3,    3,    3,    3,    3,    3,
-        3,    1,    1
-    } ;
-
-static yyconst flex_int16_t yy_base[245] =
-    {   0,
-        0,    0,  261,  260,   41,   43,   45,   46,   49,   52,
-      262,  265,  265,  265,  265,  256,  265,  265,  265,   40,
-      226,  265,  265,    0,  265,  265,   33,  235,  219,   31,
-      216,   37,   41,   53,  223,  220,  219,   48,  218,  220,
-      218,  265,  265,  265,  265,  265,  265,  265,    0,  265,
-      265,   37,  265,  216,  265,  265,  244,  237,   72,  227,
-        0,  223,  209,  216,  211,  220,  216,  204,   56,  209,
-      214,  202,  204,   71,  201,  210,  201,  195,  205,  193,
-        0,  205,  191,  192,  206,  187,   68,  189,  265,  265,
-      203,  211,  184,    0,  182,  186,  196,  198,  188,  178,
-
-      178,   52,  177,  175,   78,  175,  173,    0,  179,    0,
-      182,    0,  179,  182,  182,    0,  167,  166,  178,  169,
-      180,    0,  162,  161,  166,  165,  168,  172,  161,  164,
-      154,  158,  169,  164,    0,  157,  148,    0,  158,  156,
-      145,  160,  145,  144,  143,  140,    0,  144,  139,  138,
-      150,  139,  136,  140,  137,  141,  136,  131,  130,   74,
-        0,  135,  134,  139,  138,  141,    0,    0,    0,    0,
-      124,  119,    0,  123,  120,    0,  136,  124,  117,  131,
-        0,  124,  113,  115,  116,    0,  128,  115,  110,  119,
-        0,  112,  111,  114,  106,  109,  111,  101,  104,  104,
-
-      111,   99,    0,  114,    0,  108,    0,  265,   98,  101,
-      109,   95,    0,   95,   90,  102,   87,   99,    0,   89,
-        0,   75,   74,   69,    0,   67,   66,   71,    0,   77,
-        0,    0,    0,    0,   35,    0,   30,    0,  265,  110,
-      113,  116,   49,  119
-    } ;
-
-static yyconst flex_int16_t yy_def[245] =
-    {   0,
-      239,    1,  240,  240,  241,  241,  242,  242,    1,    1,
-      239,  239,  239,  239,  239,  239,  239,  239,  239,  239,
-      239,  239,  239,  243,  239,  239,  243,  243,  243,  243,
-      243,  243,  243,  243,  243,  243,  243,  243,  243,  243,
-      243,  239,  239,  239,  239,  239,  239,  239,  244,  239,
-      239,  239,  239,  239,  239,  239,  239,  239,  239,  239,
-      243,  243,  243,  243,  243,  243,  243,  243,  243,  243,
-      243,  243,  243,  243,  243,  243,  243,  243,  243,  243,
-      243,  243,  243,  243,  243,  243,  243,  243,  239,  239,
-      239,  239,  239,  243,  243,  243,  243,  243,  243,  243,
-
-      243,  243,  243,  243,  243,  243,  243,  243,  243,  243,
-      243,  243,  243,  243,  243,  243,  243,  243,  243,  243,
-      243,  243,  239,  239,  243,  243,  243,  243,  243,  243,
-      243,  243,  243,  243,  243,  243,  243,  243,  243,  243,
-      243,  243,  243,  243,  243,  243,  243,  243,  243,  239,
-      239,  243,  243,  243,  243,  243,  243,  243,  243,  243,
-      243,  243,  243,  243,  243,  243,  243,  243,  243,  243,
-      243,  243,  243,  239,  243,  243,  243,  243,  243,  243,
-      243,  243,  243,  243,  243,  243,  243,  243,  243,  243,
-      243,  243,  239,  243,  243,  243,  243,  243,  243,  243,
-
-      243,  243,  243,  243,  243,  243,  243,  239,  243,  243,
-      243,  243,  243,  243,  243,  243,  243,  243,  243,  243,
-      243,  243,  243,  243,  243,  243,  243,  243,  243,  243,
-      243,  243,  243,  243,  243,  243,  243,  243,    0,  239,
-      239,  239,  239,  239
-    } ;
-
-static yyconst flex_int16_t yy_nxt[309] =
-    {   0,
-       12,   13,   14,   15,   16,   17,   12,   18,   19,   12,
-       20,   21,   22,   23,   24,   25,   12,   26,   12,   27,
-       28,   29,   30,   31,   32,   24,   24,   33,   24,   34,
-       24,   35,   36,   37,   24,   38,   39,   40,   24,   24,
-       41,   42,   43,   47,   48,   47,   48,   51,   51,   58,
-       59,   61,   12,  238,   67,   12,   70,   49,   68,   49,
-       54,   52,   52,   54,   62,   74,   71,   83,   63,   72,
-      237,   75,   77,   64,   73,  132,   78,   76,   90,   90,
-       84,   58,   59,  101,   85,   79,  133,   53,   53,  107,
-       55,   56,  102,   55,   56,  108,  120,  136,  183,  236,
-
-      235,  234,  233,  121,  232,  231,  230,  184,  137,  185,
-       44,   44,   44,   46,   46,   46,   50,   50,   50,   89,
-      229,   89,  228,  227,  226,  225,  224,  223,  222,  221,
-      220,  219,  218,  217,  216,  215,  214,  213,  212,  211,
-      210,  209,  208,  207,  206,  205,  204,  203,  202,  201,
-      200,  199,  198,  197,  196,  195,  194,  193,  192,  191,
-      190,  189,  188,  187,  186,  182,  181,  180,  179,  178,
-      177,  176,  175,  174,  151,  173,  172,  171,  170,  169,
-      168,  167,  166,  165,  164,  163,  162,  161,  160,  159,
-      158,  157,  156,  155,  154,  153,  152,  151,  150,  149,
-
-      148,  147,  146,  145,  144,  143,  142,  141,  140,  139,
-      138,  135,  134,  131,  130,  129,  128,  127,  126,  125,
-      124,   92,  123,  122,  119,  118,  117,  116,  115,  114,
-      113,  112,  111,  110,  109,  106,  105,  104,  103,  100,
-       99,   98,   97,   96,   95,   94,   93,   92,   57,   91,
-       88,   87,   86,   82,   81,   80,   69,   66,   65,   60,
-       57,  239,   45,   45,   11,  239,  239,  239,  239,  239,
-      239,  239,  239,  239,  239,  239,  239,  239,  239,  239,
-      239,  239,  239,  239,  239,  239,  239,  239,  239,  239,
-      239,  239,  239,  239,  239,  239,  239,  239,  239,  239,
-
-      239,  239,  239,  239,  239,  239,  239,  239
-    } ;
-
-static yyconst flex_int16_t yy_chk[309] =
-    {   0,
-        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
-        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
-        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
-        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
-        1,    1,    1,    5,    5,    6,    6,    7,    8,   20,
-       20,  243,    9,  237,   30,   10,   32,    5,   30,    6,
-        9,    7,    8,   10,   27,   33,   32,   38,   27,   32,
-      235,   33,   34,   27,   32,  102,   34,   33,   52,   52,
-       38,   59,   59,   69,   38,   34,  102,    7,    8,   74,
-        9,    9,   69,   10,   10,   74,   87,  105,  160,  230,
-
-      228,  227,  226,   87,  224,  223,  222,  160,  105,  160,
-      240,  240,  240,  241,  241,  241,  242,  242,  242,  244,
-      220,  244,  218,  217,  216,  215,  214,  212,  211,  210,
-      209,  206,  204,  202,  201,  200,  199,  198,  197,  196,
-      195,  194,  193,  192,  190,  189,  188,  187,  185,  184,
-      183,  182,  180,  179,  178,  177,  175,  174,  172,  171,
-      166,  165,  164,  163,  162,  159,  158,  157,  156,  155,
-      154,  153,  152,  151,  150,  149,  148,  146,  145,  144,
-      143,  142,  141,  140,  139,  137,  136,  134,  133,  132,
-      131,  130,  129,  128,  127,  126,  125,  124,  123,  121,
-
-      120,  119,  118,  117,  115,  114,  113,  111,  109,  107,
-      106,  104,  103,  101,  100,   99,   98,   97,   96,   95,
-       93,   92,   91,   88,   86,   85,   84,   83,   82,   80,
-       79,   78,   77,   76,   75,   73,   72,   71,   70,   68,
-       67,   66,   65,   64,   63,   62,   60,   58,   57,   54,
-       41,   40,   39,   37,   36,   35,   31,   29,   28,   21,
-       16,   11,    4,    3,  239,  239,  239,  239,  239,  239,
-      239,  239,  239,  239,  239,  239,  239,  239,  239,  239,
-      239,  239,  239,  239,  239,  239,  239,  239,  239,  239,
-      239,  239,  239,  239,  239,  239,  239,  239,  239,  239,
-
-      239,  239,  239,  239,  239,  239,  239,  239
-    } ;
-
-/* Table of booleans, true if rule could match eol. */
-static yyconst flex_int32_t yy_rule_can_match_eol[68] =
-    {   0,
-1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 
-    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 
-    0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 
-    0, 0, 0, 0, 0, 0, 0, 0,     };
-
-static yy_state_type yy_last_accepting_state;
-static char *yy_last_accepting_cpos;
-
-extern int smtlib_flex_debug;
-int smtlib_flex_debug = 0;
-
-/* The intent behind this definition is that it'll catch
- * any uses of REJECT which flex missed.
- */
-#define REJECT reject_used_but_not_detected
-#define yymore() yymore_used_but_not_detected
-#define YY_MORE_ADJ 0
-#define YY_RESTORE_YY_MORE_OFFSET
-char *smtlibtext;
-#line 1 "smtlib.lex"
-#line 2 "smtlib.lex"
-/*****************************************************************************/
-/*!
- * \file smtlib.lex
- * 
- * Author: Clark Barrett
- * 
- * Created: 2005
- *
- * <hr>
- *
- * License to use, copy, modify, sell and/or distribute this software
- * and its documentation for any purpose is hereby granted without
- * royalty, subject to the terms and conditions defined in the \ref
- * LICENSE file provided with this distribution.
- * 
- * <hr>
- * 
- */
-/*****************************************************************************/
-
-#include <iostream>
-#include "parser_temp.h"
-#include "smtlib_parser.h"
-
-namespace CVC3 {
-  extern ParserTemp* parserTemp;
-}
-
-extern int smtlib_inputLine;
-extern char *smtlibtext;
-
-extern int smtliberror (const char *msg);
-
-static int smtlibinput(std::istream& is, char* buf, int size) {
-  int res;
-  if(is) {
-    // If interactive, read line by line; otherwise read as much as we
-    // can gobble
-    if(CVC3::parserTemp->interactive) {
-      // Print the current prompt
-      std::cout << CVC3::parserTemp->getPrompt() << std::flush;
-      // Set the prompt to "middle of the command" one
-      CVC3::parserTemp->setPrompt2();
-      // Read the line
-      is.getline(buf, size-1);
-    } else // Set the terminator char to 0
-      is.getline(buf, size-1, 0);
-    // If failbit is set, but eof is not, it means the line simply
-    // didn't fit; so we clear the state and keep on reading.
-    bool partialStr = is.fail() && !is.eof();
-    if(partialStr)
-      is.clear();
-
-    for(res = 0; res<size && buf[res] != 0; res++) ;
-    if(res == size) smtliberror("Lexer bug: overfilled the buffer");
-    if(!partialStr) { // Insert \n into the buffer
-      buf[res++] = '\n';
-      buf[res] = '\0';
-    }
-  } else {
-    res = YY_NULL;
-  }
-  return res;
-}
-
-// Redefine the input buffer function to read from an istream
-#define YY_INPUT(buf,result,max_size) \
-  result = smtlibinput(*CVC3::parserTemp->is, buf, max_size);
-
-int smtlib_bufSize() { return YY_BUF_SIZE; }
-YY_BUFFER_STATE smtlib_buf_state() { return YY_CURRENT_BUFFER; }
-
-/* some wrappers for methods that need to refer to a struct.
-   These are used by CVC3::Parser. */
-void *smtlib_createBuffer(int sz) {
-  return (void *)smtlib_create_buffer(NULL, sz);
-}
-void smtlib_deleteBuffer(void *buf_state) {
-  smtlib_delete_buffer((struct yy_buffer_state *)buf_state);
-}
-void smtlib_switchToBuffer(void *buf_state) {
-  smtlib_switch_to_buffer((struct yy_buffer_state *)buf_state);
-}
-void *smtlib_bufState() {
-  return (void *)smtlib_buf_state();
-}
-
-void smtlib_setInteractive(bool is_interactive) {
-  yy_set_interactive(is_interactive);
-}
-
-// File-static (local to this file) variables and functions
-static std::string _string_lit;
-
- static char escapeChar(char c) {
-   switch(c) {
-   case 'n': return '\n';
-   case 't': return '\t';
-   default: return c;
-   }
- }
-
-// for now, we don't have subranges.  
-//
-// ".."		{ return DOTDOT_TOK; }
-/*OPCHAR	(['!#?\_$&\|\\@])*/
-
-
-
-
-
-#line 752 "smtlib_lexer.cpp"
-
-#define INITIAL 0
-#define COMMENT 1
-#define STRING_LITERAL 2
-#define USER_VALUE 3
-#define PAT_MODE 4
-
-#ifndef YY_NO_UNISTD_H
-/* Special case for "unistd.h", since it is non-ANSI. We include it way
- * down here because we want the user's section 1 to have been scanned first.
- * The user has a chance to override it with an option.
- */
-#include <unistd.h>
-#endif
-
-#ifndef YY_EXTRA_TYPE
-#define YY_EXTRA_TYPE void *
-#endif
-
-static int yy_init_globals (void );
-
-/* Accessor methods to globals.
-   These are made visible to non-reentrant scanners for convenience. */
-
-int smtliblex_destroy (void );
-
-int smtlibget_debug (void );
-
-void smtlibset_debug (int debug_flag  );
-
-YY_EXTRA_TYPE smtlibget_extra (void );
-
-void smtlibset_extra (YY_EXTRA_TYPE user_defined  );
-
-FILE *smtlibget_in (void );
-
-void smtlibset_in  (FILE * in_str  );
-
-FILE *smtlibget_out (void );
-
-void smtlibset_out  (FILE * out_str  );
-
-int smtlibget_leng (void );
-
-char *smtlibget_text (void );
-
-int smtlibget_lineno (void );
-
-void smtlibset_lineno (int line_number  );
-
-/* Macros after this point can all be overridden by user definitions in
- * section 1.
- */
-
-#ifndef YY_SKIP_YYWRAP
-#ifdef __cplusplus
-extern "C" int smtlibwrap (void );
-#else
-extern int smtlibwrap (void );
-#endif
-#endif
-
-#ifndef yytext_ptr
-static void yy_flex_strncpy (char *,yyconst char *,int );
-#endif
-
-#ifdef YY_NEED_STRLEN
-static int yy_flex_strlen (yyconst char * );
-#endif
-
-#ifndef YY_NO_INPUT
-
-#ifdef __cplusplus
-static int yyinput (void );
-#else
-static int input (void );
-#endif
-
-#endif
-
-/* Amount of stuff to slurp up with each read. */
-#ifndef YY_READ_BUF_SIZE
-#define YY_READ_BUF_SIZE 8192
-#endif
-
-/* Copy whatever the last rule matched to the standard output. */
-#ifndef ECHO
-/* This used to be an fputs(), but since the string might contain NUL's,
- * we now use fwrite().
- */
-#define ECHO fwrite( smtlibtext, smtlibleng, 1, smtlibout )
-#endif
-
-/* Gets input and stuffs it into "buf".  number of characters read, or YY_NULL,
- * is returned in "result".
- */
-#ifndef YY_INPUT
-#define YY_INPUT(buf,result,max_size) \
-	if ( YY_CURRENT_BUFFER_LVALUE->yy_is_interactive ) \
-		{ \
-		int c = '*'; \
-		unsigned n; \
-		for ( n = 0; n < max_size && \
-			     (c = getc( smtlibin )) != EOF && c != '\n'; ++n ) \
-			buf[n] = (char) c; \
-		if ( c == '\n' ) \
-			buf[n++] = (char) c; \
-		if ( c == EOF && ferror( smtlibin ) ) \
-			YY_FATAL_ERROR( "input in flex scanner failed" ); \
-		result = n; \
-		} \
-	else \
-		{ \
-		errno=0; \
-		while ( (result = fread(buf, 1, max_size, smtlibin))==0 && ferror(smtlibin)) \
-			{ \
-			if( errno != EINTR) \
-				{ \
-				YY_FATAL_ERROR( "input in flex scanner failed" ); \
-				break; \
-				} \
-			errno=0; \
-			clearerr(smtlibin); \
-			} \
-		}\
-\
-
-#endif
-
-/* No semi-colon after return; correct usage is to write "yyterminate();" -
- * we don't want an extra ';' after the "return" because that will cause
- * some compilers to complain about unreachable statements.
- */
-#ifndef yyterminate
-#define yyterminate() return YY_NULL
-#endif
-
-/* Number of entries by which start-condition stack grows. */
-#ifndef YY_START_STACK_INCR
-#define YY_START_STACK_INCR 25
-#endif
-
-/* Report a fatal error. */
-#ifndef YY_FATAL_ERROR
-#define YY_FATAL_ERROR(msg) yy_fatal_error( msg )
-#endif
-
-/* end tables serialization structures and prototypes */
-
-/* Default declaration of generated scanner - a define so the user can
- * easily add parameters.
- */
-#ifndef YY_DECL
-#define YY_DECL_IS_OURS 1
-
-extern int smtliblex (void);
-
-#define YY_DECL int smtliblex (void)
-#endif /* !YY_DECL */
-
-/* Code executed at the beginning of each rule, after smtlibtext and smtlibleng
- * have been set up.
- */
-#ifndef YY_USER_ACTION
-#define YY_USER_ACTION
-#endif
-
-/* Code executed at the end of each rule. */
-#ifndef YY_BREAK
-#define YY_BREAK break;
-#endif
-
-#define YY_RULE_SETUP \
-	YY_USER_ACTION
-
-/** The main scanner function which does all the work.
- */
-YY_DECL
-{
-	register yy_state_type yy_current_state;
-	register char *yy_cp, *yy_bp;
-	register int yy_act;
-    
-#line 126 "smtlib.lex"
-
-
-#line 939 "smtlib_lexer.cpp"
-
-	if ( !(yy_init) )
-		{
-		(yy_init) = 1;
-
-#ifdef YY_USER_INIT
-		YY_USER_INIT;
-#endif
-
-		if ( ! (yy_start) )
-			(yy_start) = 1;	/* first start state */
-
-		if ( ! smtlibin )
-			smtlibin = stdin;
-
-		if ( ! smtlibout )
-			smtlibout = stdout;
-
-		if ( ! YY_CURRENT_BUFFER ) {
-			smtlibensure_buffer_stack ();
-			YY_CURRENT_BUFFER_LVALUE =
-				smtlib_create_buffer(smtlibin,YY_BUF_SIZE );
-		}
-
-		smtlib_load_buffer_state( );
-		}
-
-	while ( 1 )		/* loops until end-of-file is reached */
-		{
-		yy_cp = (yy_c_buf_p);
-
-		/* Support of smtlibtext. */
-		*yy_cp = (yy_hold_char);
-
-		/* yy_bp points to the position in yy_ch_buf of the start of
-		 * the current run.
-		 */
-		yy_bp = yy_cp;
-
-		yy_current_state = (yy_start);
-yy_match:
-		do
-			{
-			register YY_CHAR yy_c = yy_ec[YY_SC_TO_UI(*yy_cp)];
-			if ( yy_accept[yy_current_state] )
-				{
-				(yy_last_accepting_state) = yy_current_state;
-				(yy_last_accepting_cpos) = yy_cp;
-				}
-			while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state )
-				{
-				yy_current_state = (int) yy_def[yy_current_state];
-				if ( yy_current_state >= 240 )
-					yy_c = yy_meta[(unsigned int) yy_c];
-				}
-			yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c];
-			++yy_cp;
-			}
-		while ( yy_base[yy_current_state] != 265 );
-
-yy_find_action:
-		yy_act = yy_accept[yy_current_state];
-		if ( yy_act == 0 )
-			{ /* have to back up */
-			yy_cp = (yy_last_accepting_cpos);
-			yy_current_state = (yy_last_accepting_state);
-			yy_act = yy_accept[yy_current_state];
-			}
-
-		YY_DO_BEFORE_ACTION;
-
-		if ( yy_act != YY_END_OF_BUFFER && yy_rule_can_match_eol[yy_act] )
-			{
-			int yyl;
-			for ( yyl = 0; yyl < smtlibleng; ++yyl )
-				if ( smtlibtext[yyl] == '\n' )
-					   
-    smtliblineno++;
-;
-			}
-
-do_action:	/* This label is used only to access EOF actions. */
-
-		switch ( yy_act )
-	{ /* beginning of action switch */
-			case 0: /* must back up */
-			/* undo the effects of YY_DO_BEFORE_ACTION */
-			*yy_cp = (yy_hold_char);
-			yy_cp = (yy_last_accepting_cpos);
-			yy_current_state = (yy_last_accepting_state);
-			goto yy_find_action;
-
-case 1:
-/* rule 1 can match eol */
-YY_RULE_SETUP
-#line 128 "smtlib.lex"
-{ CVC3::parserTemp->lineNum++; }
-	YY_BREAK
-case 2:
-YY_RULE_SETUP
-#line 129 "smtlib.lex"
-{ /* skip whitespace */ }
-	YY_BREAK
-case 3:
-YY_RULE_SETUP
-#line 131 "smtlib.lex"
-{ smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK; }
-	YY_BREAK
-case 4:
-YY_RULE_SETUP
-#line 132 "smtlib.lex"
-{ smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK; 
-		}
-	YY_BREAK
-case 5:
-YY_RULE_SETUP
-#line 135 "smtlib.lex"
-{ BEGIN COMMENT; }
-	YY_BREAK
-case 6:
-/* rule 6 can match eol */
-YY_RULE_SETUP
-#line 136 "smtlib.lex"
-{ BEGIN INITIAL; /* return to normal mode */ 
-                  CVC3::parserTemp->lineNum++; }
-	YY_BREAK
-case 7:
-YY_RULE_SETUP
-#line 138 "smtlib.lex"
-{ /* stay in comment mode */ }
-	YY_BREAK
-case 8:
-YY_RULE_SETUP
-#line 140 "smtlib.lex"
-{ BEGIN STRING_LITERAL; 
-                          _string_lit.erase(_string_lit.begin(),
-                                            _string_lit.end()); }
-	YY_BREAK
-case 9:
-YY_RULE_SETUP
-#line 143 "smtlib.lex"
-{ /* escape characters (like \n or \") */
-                          _string_lit.insert(_string_lit.end(),
-                                             escapeChar(smtlibtext[1])); }
-	YY_BREAK
-case 10:
-YY_RULE_SETUP
-#line 146 "smtlib.lex"
-{ BEGIN INITIAL; /* return to normal mode */ 
-			  smtliblval.str = new std::string(_string_lit);
-                          return STRING_TOK; }
-	YY_BREAK
-case 11:
-YY_RULE_SETUP
-#line 149 "smtlib.lex"
-{ _string_lit.insert(_string_lit.end(),*smtlibtext); }
-	YY_BREAK
-case 12:
-YY_RULE_SETUP
-#line 151 "smtlib.lex"
-{ BEGIN PAT_MODE;
-                          return PAT_TOK;}
-	YY_BREAK
-case 13:
-YY_RULE_SETUP
-#line 153 "smtlib.lex"
-{ BEGIN INITIAL; 
-                          return RCURBRACK_TOK; }
-	YY_BREAK
-case 14:
-YY_RULE_SETUP
-#line 155 "smtlib.lex"
-{ BEGIN USER_VALUE;
-                          _string_lit.erase(_string_lit.begin(),
-                                            _string_lit.end()); }
-	YY_BREAK
-case 15:
-YY_RULE_SETUP
-#line 158 "smtlib.lex"
-{ /* escape characters */
-                          _string_lit.insert(_string_lit.end(),smtlibtext[1]); }
-	YY_BREAK
-case 16:
-YY_RULE_SETUP
-#line 161 "smtlib.lex"
-{ BEGIN INITIAL; /* return to normal mode */ 
-			  smtliblval.str = new std::string(_string_lit);
-                          return USER_VAL_TOK; }
-	YY_BREAK
-case 17:
-/* rule 17 can match eol */
-YY_RULE_SETUP
-#line 165 "smtlib.lex"
-{ _string_lit.insert(_string_lit.end(),'\n');
-                          CVC3::parserTemp->lineNum++; }
-	YY_BREAK
-case 18:
-YY_RULE_SETUP
-#line 167 "smtlib.lex"
-{ _string_lit.insert(_string_lit.end(),*smtlibtext); }
-	YY_BREAK
-case 19:
-YY_RULE_SETUP
-#line 169 "smtlib.lex"
-{ return TRUE_TOK; }
-	YY_BREAK
-case 20:
-YY_RULE_SETUP
-#line 170 "smtlib.lex"
-{ return FALSE_TOK; }
-	YY_BREAK
-case 21:
-YY_RULE_SETUP
-#line 171 "smtlib.lex"
-{ return ITE_TOK; }
-	YY_BREAK
-case 22:
-YY_RULE_SETUP
-#line 172 "smtlib.lex"
-{ return NOT_TOK; }
-	YY_BREAK
-case 23:
-YY_RULE_SETUP
-#line 173 "smtlib.lex"
-{ return IMPLIES_TOK; }
-	YY_BREAK
-case 24:
-YY_RULE_SETUP
-#line 174 "smtlib.lex"
-{ return IF_THEN_ELSE_TOK; }
-	YY_BREAK
-case 25:
-YY_RULE_SETUP
-#line 175 "smtlib.lex"
-{ return AND_TOK; }
-	YY_BREAK
-case 26:
-YY_RULE_SETUP
-#line 176 "smtlib.lex"
-{ return OR_TOK; }
-	YY_BREAK
-case 27:
-YY_RULE_SETUP
-#line 177 "smtlib.lex"
-{ return XOR_TOK; }
-	YY_BREAK
-case 28:
-YY_RULE_SETUP
-#line 178 "smtlib.lex"
-{ return IFF_TOK; }
-	YY_BREAK
-case 29:
-YY_RULE_SETUP
-#line 179 "smtlib.lex"
-{ return EXISTS_TOK; }
-	YY_BREAK
-case 30:
-YY_RULE_SETUP
-#line 180 "smtlib.lex"
-{ return FORALL_TOK; }
-	YY_BREAK
-case 31:
-YY_RULE_SETUP
-#line 181 "smtlib.lex"
-{ return LET_TOK; }
-	YY_BREAK
-case 32:
-YY_RULE_SETUP
-#line 182 "smtlib.lex"
-{ return FLET_TOK; }
-	YY_BREAK
-case 33:
-YY_RULE_SETUP
-#line 183 "smtlib.lex"
-{ return NOTES_TOK; }
-	YY_BREAK
-case 34:
-YY_RULE_SETUP
-#line 184 "smtlib.lex"
-{ return CVC_COMMAND_TOK; }
-	YY_BREAK
-case 35:
-YY_RULE_SETUP
-#line 185 "smtlib.lex"
-{ return SORTS_TOK; }
-	YY_BREAK
-case 36:
-YY_RULE_SETUP
-#line 186 "smtlib.lex"
-{ return FUNS_TOK; }
-	YY_BREAK
-case 37:
-YY_RULE_SETUP
-#line 187 "smtlib.lex"
-{ return PREDS_TOK; }
-	YY_BREAK
-case 38:
-YY_RULE_SETUP
-#line 188 "smtlib.lex"
-{ return EXTENSIONS_TOK; }
-	YY_BREAK
-case 39:
-YY_RULE_SETUP
-#line 189 "smtlib.lex"
-{ return DEFINITION_TOK; }
-	YY_BREAK
-case 40:
-YY_RULE_SETUP
-#line 190 "smtlib.lex"
-{ return AXIOMS_TOK; }
-	YY_BREAK
-case 41:
-YY_RULE_SETUP
-#line 191 "smtlib.lex"
-{ return LOGIC_TOK; }
-	YY_BREAK
-case 42:
-YY_RULE_SETUP
-#line 192 "smtlib.lex"
-{ return SAT_TOK; }
-	YY_BREAK
-case 43:
-YY_RULE_SETUP
-#line 193 "smtlib.lex"
-{ return UNSAT_TOK; }
-	YY_BREAK
-case 44:
-YY_RULE_SETUP
-#line 194 "smtlib.lex"
-{ return UNKNOWN_TOK; }
-	YY_BREAK
-case 45:
-YY_RULE_SETUP
-#line 195 "smtlib.lex"
-{ return ASSUMPTION_TOK; }
-	YY_BREAK
-case 46:
-YY_RULE_SETUP
-#line 196 "smtlib.lex"
-{ return FORMULA_TOK; }
-	YY_BREAK
-case 47:
-YY_RULE_SETUP
-#line 197 "smtlib.lex"
-{ return STATUS_TOK; }
-	YY_BREAK
-case 48:
-YY_RULE_SETUP
-#line 198 "smtlib.lex"
-{ return BENCHMARK_TOK; }
-	YY_BREAK
-case 49:
-YY_RULE_SETUP
-#line 199 "smtlib.lex"
-{ return EXTRASORTS_TOK; }
-	YY_BREAK
-case 50:
-YY_RULE_SETUP
-#line 200 "smtlib.lex"
-{ return EXTRAFUNS_TOK; }
-	YY_BREAK
-case 51:
-YY_RULE_SETUP
-#line 201 "smtlib.lex"
-{ return EXTRAPREDS_TOK; }
-	YY_BREAK
-case 52:
-YY_RULE_SETUP
-#line 202 "smtlib.lex"
-{ return LANGUAGE_TOK; }
-	YY_BREAK
-case 53:
-YY_RULE_SETUP
-#line 203 "smtlib.lex"
-{ return DISTINCT_TOK; }
-	YY_BREAK
-case 54:
-YY_RULE_SETUP
-#line 204 "smtlib.lex"
-{ return PAT_TOK; } 
-	YY_BREAK
-case 55:
-YY_RULE_SETUP
-#line 205 "smtlib.lex"
-{ return COLON_TOK; }
-	YY_BREAK
-case 56:
-YY_RULE_SETUP
-#line 206 "smtlib.lex"
-{ return LBRACKET_TOK; }
-	YY_BREAK
-case 57:
-YY_RULE_SETUP
-#line 207 "smtlib.lex"
-{ return RBRACKET_TOK; }
-	YY_BREAK
-case 58:
-YY_RULE_SETUP
-#line 208 "smtlib.lex"
-{ return LCURBRACK_TOK;}
-	YY_BREAK
-case 59:
-YY_RULE_SETUP
-#line 209 "smtlib.lex"
-{ return RCURBRACK_TOK;}
-	YY_BREAK
-case 60:
-YY_RULE_SETUP
-#line 210 "smtlib.lex"
-{ return LPAREN_TOK; }
-	YY_BREAK
-case 61:
-YY_RULE_SETUP
-#line 211 "smtlib.lex"
-{ return RPAREN_TOK; }
-	YY_BREAK
-case 62:
-YY_RULE_SETUP
-#line 212 "smtlib.lex"
-{ return DOLLAR_TOK; }
-	YY_BREAK
-case 63:
-YY_RULE_SETUP
-#line 213 "smtlib.lex"
-{ return QUESTION_TOK; }
-	YY_BREAK
-case 64:
-YY_RULE_SETUP
-#line 215 "smtlib.lex"
-{ smtliblval.str = new std::string(smtlibtext); return AR_SYMB; }
-	YY_BREAK
-case 65:
-YY_RULE_SETUP
-#line 216 "smtlib.lex"
-{smtliblval.str = new std::string(smtlibtext); return SYM_TOK; }
-	YY_BREAK
-case YY_STATE_EOF(INITIAL):
-case YY_STATE_EOF(COMMENT):
-case YY_STATE_EOF(STRING_LITERAL):
-case YY_STATE_EOF(USER_VALUE):
-case YY_STATE_EOF(PAT_MODE):
-#line 218 "smtlib.lex"
-{ return EOF_TOK; }
-	YY_BREAK
-case 66:
-YY_RULE_SETUP
-#line 220 "smtlib.lex"
-{ smtliberror("Illegal input character."); }
-	YY_BREAK
-case 67:
-YY_RULE_SETUP
-#line 221 "smtlib.lex"
-ECHO;
-	YY_BREAK
-#line 1394 "smtlib_lexer.cpp"
-
-	case YY_END_OF_BUFFER:
-		{
-		/* Amount of text matched not including the EOB char. */
-		int yy_amount_of_matched_text = (int) (yy_cp - (yytext_ptr)) - 1;
-
-		/* Undo the effects of YY_DO_BEFORE_ACTION. */
-		*yy_cp = (yy_hold_char);
-		YY_RESTORE_YY_MORE_OFFSET
-
-		if ( YY_CURRENT_BUFFER_LVALUE->yy_buffer_status == YY_BUFFER_NEW )
-			{
-			/* We're scanning a new file or input source.  It's
-			 * possible that this happened because the user
-			 * just pointed smtlibin at a new source and called
-			 * smtliblex().  If so, then we have to assure
-			 * consistency between YY_CURRENT_BUFFER and our
-			 * globals.  Here is the right place to do so, because
-			 * this is the first action (other than possibly a
-			 * back-up) that will match for the new input source.
-			 */
-			(yy_n_chars) = YY_CURRENT_BUFFER_LVALUE->yy_n_chars;
-			YY_CURRENT_BUFFER_LVALUE->yy_input_file = smtlibin;
-			YY_CURRENT_BUFFER_LVALUE->yy_buffer_status = YY_BUFFER_NORMAL;
-			}
-
-		/* Note that here we test for yy_c_buf_p "<=" to the position
-		 * of the first EOB in the buffer, since yy_c_buf_p will
-		 * already have been incremented past the NUL character
-		 * (since all states make transitions on EOB to the
-		 * end-of-buffer state).  Contrast this with the test
-		 * in input().
-		 */
-		if ( (yy_c_buf_p) <= &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)] )
-			{ /* This was really a NUL. */
-			yy_state_type yy_next_state;
-
-			(yy_c_buf_p) = (yytext_ptr) + yy_amount_of_matched_text;
-
-			yy_current_state = yy_get_previous_state(  );
-
-			/* Okay, we're now positioned to make the NUL
-			 * transition.  We couldn't have
-			 * yy_get_previous_state() go ahead and do it
-			 * for us because it doesn't know how to deal
-			 * with the possibility of jamming (and we don't
-			 * want to build jamming into it because then it
-			 * will run more slowly).
-			 */
-
-			yy_next_state = yy_try_NUL_trans( yy_current_state );
-
-			yy_bp = (yytext_ptr) + YY_MORE_ADJ;
-
-			if ( yy_next_state )
-				{
-				/* Consume the NUL. */
-				yy_cp = ++(yy_c_buf_p);
-				yy_current_state = yy_next_state;
-				goto yy_match;
-				}
-
-			else
-				{
-				yy_cp = (yy_c_buf_p);
-				goto yy_find_action;
-				}
-			}
-
-		else switch ( yy_get_next_buffer(  ) )
-			{
-			case EOB_ACT_END_OF_FILE:
-				{
-				(yy_did_buffer_switch_on_eof) = 0;
-
-				if ( smtlibwrap( ) )
-					{
-					/* Note: because we've taken care in
-					 * yy_get_next_buffer() to have set up
-					 * smtlibtext, we can now set up
-					 * yy_c_buf_p so that if some total
-					 * hoser (like flex itself) wants to
-					 * call the scanner after we return the
-					 * YY_NULL, it'll still work - another
-					 * YY_NULL will get returned.
-					 */
-					(yy_c_buf_p) = (yytext_ptr) + YY_MORE_ADJ;
-
-					yy_act = YY_STATE_EOF(YY_START);
-					goto do_action;
-					}
-
-				else
-					{
-					if ( ! (yy_did_buffer_switch_on_eof) )
-						YY_NEW_FILE;
-					}
-				break;
-				}
-
-			case EOB_ACT_CONTINUE_SCAN:
-				(yy_c_buf_p) =
-					(yytext_ptr) + yy_amount_of_matched_text;
-
-				yy_current_state = yy_get_previous_state(  );
-
-				yy_cp = (yy_c_buf_p);
-				yy_bp = (yytext_ptr) + YY_MORE_ADJ;
-				goto yy_match;
-
-			case EOB_ACT_LAST_MATCH:
-				(yy_c_buf_p) =
-				&YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)];
-
-				yy_current_state = yy_get_previous_state(  );
-
-				yy_cp = (yy_c_buf_p);
-				yy_bp = (yytext_ptr) + YY_MORE_ADJ;
-				goto yy_find_action;
-			}
-		break;
-		}
-
-	default:
-		YY_FATAL_ERROR(
-			"fatal flex scanner internal error--no action found" );
-	} /* end of action switch */
-		} /* end of scanning one token */
-} /* end of smtliblex */
-
-/* yy_get_next_buffer - try to read in a new buffer
- *
- * Returns a code representing an action:
- *	EOB_ACT_LAST_MATCH -
- *	EOB_ACT_CONTINUE_SCAN - continue scanning from current position
- *	EOB_ACT_END_OF_FILE - end of file
- */
-static int yy_get_next_buffer (void)
-{
-    	register char *dest = YY_CURRENT_BUFFER_LVALUE->yy_ch_buf;
-	register char *source = (yytext_ptr);
-	register int number_to_move, i;
-	int ret_val;
-
-	if ( (yy_c_buf_p) > &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars) + 1] )
-		YY_FATAL_ERROR(
-		"fatal flex scanner internal error--end of buffer missed" );
-
-	if ( YY_CURRENT_BUFFER_LVALUE->yy_fill_buffer == 0 )
-		{ /* Don't try to fill the buffer, so this is an EOF. */
-		if ( (yy_c_buf_p) - (yytext_ptr) - YY_MORE_ADJ == 1 )
-			{
-			/* We matched a single character, the EOB, so
-			 * treat this as a final EOF.
-			 */
-			return EOB_ACT_END_OF_FILE;
-			}
-
-		else
-			{
-			/* We matched some text prior to the EOB, first
-			 * process it.
-			 */
-			return EOB_ACT_LAST_MATCH;
-			}
-		}
-
-	/* Try to read more data. */
-
-	/* First move last chars to start of buffer. */
-	number_to_move = (int) ((yy_c_buf_p) - (yytext_ptr)) - 1;
-
-	for ( i = 0; i < number_to_move; ++i )
-		*(dest++) = *(source++);
-
-	if ( YY_CURRENT_BUFFER_LVALUE->yy_buffer_status == YY_BUFFER_EOF_PENDING )
-		/* don't do the read, it's not guaranteed to return an EOF,
-		 * just force an EOF
-		 */
-		YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars) = 0;
-
-	else
-		{
-			int num_to_read =
-			YY_CURRENT_BUFFER_LVALUE->yy_buf_size - number_to_move - 1;
-
-		while ( num_to_read <= 0 )
-			{ /* Not enough room in the buffer - grow it. */
-
-			/* just a shorter name for the current buffer */
-			YY_BUFFER_STATE b = YY_CURRENT_BUFFER;
-
-			int yy_c_buf_p_offset =
-				(int) ((yy_c_buf_p) - b->yy_ch_buf);
-
-			if ( b->yy_is_our_buffer )
-				{
-				int new_size = b->yy_buf_size * 2;
-
-				if ( new_size <= 0 )
-					b->yy_buf_size += b->yy_buf_size / 8;
-				else
-					b->yy_buf_size *= 2;
-
-				b->yy_ch_buf = (char *)
-					/* Include room in for 2 EOB chars. */
-					smtlibrealloc((void *) b->yy_ch_buf,b->yy_buf_size + 2  );
-				}
-			else
-				/* Can't grow it, we don't own it. */
-				b->yy_ch_buf = 0;
-
-			if ( ! b->yy_ch_buf )
-				YY_FATAL_ERROR(
-				"fatal error - scanner input buffer overflow" );
-
-			(yy_c_buf_p) = &b->yy_ch_buf[yy_c_buf_p_offset];
-
-			num_to_read = YY_CURRENT_BUFFER_LVALUE->yy_buf_size -
-						number_to_move - 1;
-
-			}
-
-		if ( num_to_read > YY_READ_BUF_SIZE )
-			num_to_read = YY_READ_BUF_SIZE;
-
-		/* Read in more data. */
-		YY_INPUT( (&YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[number_to_move]),
-			(yy_n_chars), (size_t) num_to_read );
-
-		YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars);
-		}
-
-	if ( (yy_n_chars) == 0 )
-		{
-		if ( number_to_move == YY_MORE_ADJ )
-			{
-			ret_val = EOB_ACT_END_OF_FILE;
-			smtlibrestart(smtlibin  );
-			}
-
-		else
-			{
-			ret_val = EOB_ACT_LAST_MATCH;
-			YY_CURRENT_BUFFER_LVALUE->yy_buffer_status =
-				YY_BUFFER_EOF_PENDING;
-			}
-		}
-
-	else
-		ret_val = EOB_ACT_CONTINUE_SCAN;
-
-	if ((yy_size_t) ((yy_n_chars) + number_to_move) > YY_CURRENT_BUFFER_LVALUE->yy_buf_size) {
-		/* Extend the array by 50%, plus the number we really need. */
-		yy_size_t new_size = (yy_n_chars) + number_to_move + ((yy_n_chars) >> 1);
-		YY_CURRENT_BUFFER_LVALUE->yy_ch_buf = (char *) smtlibrealloc((void *) YY_CURRENT_BUFFER_LVALUE->yy_ch_buf,new_size  );
-		if ( ! YY_CURRENT_BUFFER_LVALUE->yy_ch_buf )
-			YY_FATAL_ERROR( "out of dynamic memory in yy_get_next_buffer()" );
-	}
-
-	(yy_n_chars) += number_to_move;
-	YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)] = YY_END_OF_BUFFER_CHAR;
-	YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars) + 1] = YY_END_OF_BUFFER_CHAR;
-
-	(yytext_ptr) = &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[0];
-
-	return ret_val;
-}
-
-/* yy_get_previous_state - get the state just before the EOB char was reached */
-
-    static yy_state_type yy_get_previous_state (void)
-{
-	register yy_state_type yy_current_state;
-	register char *yy_cp;
-    
-	yy_current_state = (yy_start);
-
-	for ( yy_cp = (yytext_ptr) + YY_MORE_ADJ; yy_cp < (yy_c_buf_p); ++yy_cp )
-		{
-		register YY_CHAR yy_c = (*yy_cp ? yy_ec[YY_SC_TO_UI(*yy_cp)] : 1);
-		if ( yy_accept[yy_current_state] )
-			{
-			(yy_last_accepting_state) = yy_current_state;
-			(yy_last_accepting_cpos) = yy_cp;
-			}
-		while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state )
-			{
-			yy_current_state = (int) yy_def[yy_current_state];
-			if ( yy_current_state >= 240 )
-				yy_c = yy_meta[(unsigned int) yy_c];
-			}
-		yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c];
-		}
-
-	return yy_current_state;
-}
-
-/* yy_try_NUL_trans - try to make a transition on the NUL character
- *
- * synopsis
- *	next_state = yy_try_NUL_trans( current_state );
- */
-    static yy_state_type yy_try_NUL_trans  (yy_state_type yy_current_state )
-{
-	register int yy_is_jam;
-    	register char *yy_cp = (yy_c_buf_p);
-
-	register YY_CHAR yy_c = 1;
-	if ( yy_accept[yy_current_state] )
-		{
-		(yy_last_accepting_state) = yy_current_state;
-		(yy_last_accepting_cpos) = yy_cp;
-		}
-	while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state )
-		{
-		yy_current_state = (int) yy_def[yy_current_state];
-		if ( yy_current_state >= 240 )
-			yy_c = yy_meta[(unsigned int) yy_c];
-		}
-	yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c];
-	yy_is_jam = (yy_current_state == 239);
-
-	return yy_is_jam ? 0 : yy_current_state;
-}
-
-#ifndef YY_NO_INPUT
-#ifdef __cplusplus
-    static int yyinput (void)
-#else
-    static int input  (void)
-#endif
-
-{
-	int c;
-    
-	*(yy_c_buf_p) = (yy_hold_char);
-
-	if ( *(yy_c_buf_p) == YY_END_OF_BUFFER_CHAR )
-		{
-		/* yy_c_buf_p now points to the character we want to return.
-		 * If this occurs *before* the EOB characters, then it's a
-		 * valid NUL; if not, then we've hit the end of the buffer.
-		 */
-		if ( (yy_c_buf_p) < &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)] )
-			/* This was really a NUL. */
-			*(yy_c_buf_p) = '\0';
-
-		else
-			{ /* need more input */
-			int offset = (yy_c_buf_p) - (yytext_ptr);
-			++(yy_c_buf_p);
-
-			switch ( yy_get_next_buffer(  ) )
-				{
-				case EOB_ACT_LAST_MATCH:
-					/* This happens because yy_g_n_b()
-					 * sees that we've accumulated a
-					 * token and flags that we need to
-					 * try matching the token before
-					 * proceeding.  But for input(),
-					 * there's no matching to consider.
-					 * So convert the EOB_ACT_LAST_MATCH
-					 * to EOB_ACT_END_OF_FILE.
-					 */
-
-					/* Reset buffer status. */
-					smtlibrestart(smtlibin );
-
-					/*FALLTHROUGH*/
-
-				case EOB_ACT_END_OF_FILE:
-					{
-					if ( smtlibwrap( ) )
-						return EOF;
-
-					if ( ! (yy_did_buffer_switch_on_eof) )
-						YY_NEW_FILE;
-#ifdef __cplusplus
-					return yyinput();
-#else
-					return input();
-#endif
-					}
-
-				case EOB_ACT_CONTINUE_SCAN:
-					(yy_c_buf_p) = (yytext_ptr) + offset;
-					break;
-				}
-			}
-		}
-
-	c = *(unsigned char *) (yy_c_buf_p);	/* cast for 8-bit char's */
-	*(yy_c_buf_p) = '\0';	/* preserve smtlibtext */
-	(yy_hold_char) = *++(yy_c_buf_p);
-
-	if ( c == '\n' )
-		   
-    smtliblineno++;
-;
-
-	return c;
-}
-#endif	/* ifndef YY_NO_INPUT */
-
-/** Immediately switch to a different input stream.
- * @param input_file A readable stream.
- * 
- * @note This function does not reset the start condition to @c INITIAL .
- */
-    void smtlibrestart  (FILE * input_file )
-{
-    
-	if ( ! YY_CURRENT_BUFFER ){
-        smtlibensure_buffer_stack ();
-		YY_CURRENT_BUFFER_LVALUE =
-            smtlib_create_buffer(smtlibin,YY_BUF_SIZE );
-	}
-
-	smtlib_init_buffer(YY_CURRENT_BUFFER,input_file );
-	smtlib_load_buffer_state( );
-}
-
-/** Switch to a different input buffer.
- * @param new_buffer The new input buffer.
- * 
- */
-    void smtlib_switch_to_buffer  (YY_BUFFER_STATE  new_buffer )
-{
-    
-	/* TODO. We should be able to replace this entire function body
-	 * with
-	 *		smtlibpop_buffer_state();
-	 *		smtlibpush_buffer_state(new_buffer);
-     */
-	smtlibensure_buffer_stack ();
-	if ( YY_CURRENT_BUFFER == new_buffer )
-		return;
-
-	if ( YY_CURRENT_BUFFER )
-		{
-		/* Flush out information for old buffer. */
-		*(yy_c_buf_p) = (yy_hold_char);
-		YY_CURRENT_BUFFER_LVALUE->yy_buf_pos = (yy_c_buf_p);
-		YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars);
-		}
-
-	YY_CURRENT_BUFFER_LVALUE = new_buffer;
-	smtlib_load_buffer_state( );
-
-	/* We don't actually know whether we did this switch during
-	 * EOF (smtlibwrap()) processing, but the only time this flag
-	 * is looked at is after smtlibwrap() is called, so it's safe
-	 * to go ahead and always set it.
-	 */
-	(yy_did_buffer_switch_on_eof) = 1;
-}
-
-static void smtlib_load_buffer_state  (void)
-{
-    	(yy_n_chars) = YY_CURRENT_BUFFER_LVALUE->yy_n_chars;
-	(yytext_ptr) = (yy_c_buf_p) = YY_CURRENT_BUFFER_LVALUE->yy_buf_pos;
-	smtlibin = YY_CURRENT_BUFFER_LVALUE->yy_input_file;
-	(yy_hold_char) = *(yy_c_buf_p);
-}
-
-/** Allocate and initialize an input buffer state.
- * @param file A readable stream.
- * @param size The character buffer size in bytes. When in doubt, use @c YY_BUF_SIZE.
- * 
- * @return the allocated buffer state.
- */
-    YY_BUFFER_STATE smtlib_create_buffer  (FILE * file, int  size )
-{
-	YY_BUFFER_STATE b;
-    
-	b = (YY_BUFFER_STATE) smtliballoc(sizeof( struct yy_buffer_state )  );
-	if ( ! b )
-		YY_FATAL_ERROR( "out of dynamic memory in smtlib_create_buffer()" );
-
-	b->yy_buf_size = size;
-
-	/* yy_ch_buf has to be 2 characters longer than the size given because
-	 * we need to put in 2 end-of-buffer characters.
-	 */
-	b->yy_ch_buf = (char *) smtliballoc(b->yy_buf_size + 2  );
-	if ( ! b->yy_ch_buf )
-		YY_FATAL_ERROR( "out of dynamic memory in smtlib_create_buffer()" );
-
-	b->yy_is_our_buffer = 1;
-
-	smtlib_init_buffer(b,file );
-
-	return b;
-}
-
-/** Destroy the buffer.
- * @param b a buffer created with smtlib_create_buffer()
- * 
- */
-    void smtlib_delete_buffer (YY_BUFFER_STATE  b )
-{
-    
-	if ( ! b )
-		return;
-
-	if ( b == YY_CURRENT_BUFFER ) /* Not sure if we should pop here. */
-		YY_CURRENT_BUFFER_LVALUE = (YY_BUFFER_STATE) 0;
-
-	if ( b->yy_is_our_buffer )
-		smtlibfree((void *) b->yy_ch_buf  );
-
-	smtlibfree((void *) b  );
-}
-
-#ifndef __cplusplus
-extern int isatty (int );
-#endif /* __cplusplus */
-    
-/* Initializes or reinitializes a buffer.
- * This function is sometimes called more than once on the same buffer,
- * such as during a smtlibrestart() or at EOF.
- */
-    static void smtlib_init_buffer  (YY_BUFFER_STATE  b, FILE * file )
-
-{
-	int oerrno = errno;
-    
-	smtlib_flush_buffer(b );
-
-	b->yy_input_file = file;
-	b->yy_fill_buffer = 1;
-
-    /* If b is the current buffer, then smtlib_init_buffer was _probably_
-     * called from smtlibrestart() or through yy_get_next_buffer.
-     * In that case, we don't want to reset the lineno or column.
-     */
-    if (b != YY_CURRENT_BUFFER){
-        b->yy_bs_lineno = 1;
-        b->yy_bs_column = 0;
-    }
-
-        b->yy_is_interactive = file ? (isatty( fileno(file) ) > 0) : 0;
-    
-	errno = oerrno;
-}
-
-/** Discard all buffered characters. On the next scan, YY_INPUT will be called.
- * @param b the buffer state to be flushed, usually @c YY_CURRENT_BUFFER.
- * 
- */
-    void smtlib_flush_buffer (YY_BUFFER_STATE  b )
-{
-    	if ( ! b )
-		return;
-
-	b->yy_n_chars = 0;
-
-	/* We always need two end-of-buffer characters.  The first causes
-	 * a transition to the end-of-buffer state.  The second causes
-	 * a jam in that state.
-	 */
-	b->yy_ch_buf[0] = YY_END_OF_BUFFER_CHAR;
-	b->yy_ch_buf[1] = YY_END_OF_BUFFER_CHAR;
-
-	b->yy_buf_pos = &b->yy_ch_buf[0];
-
-	b->yy_at_bol = 1;
-	b->yy_buffer_status = YY_BUFFER_NEW;
-
-	if ( b == YY_CURRENT_BUFFER )
-		smtlib_load_buffer_state( );
-}
-
-/** Pushes the new state onto the stack. The new state becomes
- *  the current state. This function will allocate the stack
- *  if necessary.
- *  @param new_buffer The new state.
- *  
- */
-void smtlibpush_buffer_state (YY_BUFFER_STATE new_buffer )
-{
-    	if (new_buffer == NULL)
-		return;
-
-	smtlibensure_buffer_stack();
-
-	/* This block is copied from smtlib_switch_to_buffer. */
-	if ( YY_CURRENT_BUFFER )
-		{
-		/* Flush out information for old buffer. */
-		*(yy_c_buf_p) = (yy_hold_char);
-		YY_CURRENT_BUFFER_LVALUE->yy_buf_pos = (yy_c_buf_p);
-		YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars);
-		}
-
-	/* Only push if top exists. Otherwise, replace top. */
-	if (YY_CURRENT_BUFFER)
-		(yy_buffer_stack_top)++;
-	YY_CURRENT_BUFFER_LVALUE = new_buffer;
-
-	/* copied from smtlib_switch_to_buffer. */
-	smtlib_load_buffer_state( );
-	(yy_did_buffer_switch_on_eof) = 1;
-}
-
-/** Removes and deletes the top of the stack, if present.
- *  The next element becomes the new top.
- *  
- */
-void smtlibpop_buffer_state (void)
-{
-    	if (!YY_CURRENT_BUFFER)
-		return;
-
-	smtlib_delete_buffer(YY_CURRENT_BUFFER );
-	YY_CURRENT_BUFFER_LVALUE = NULL;
-	if ((yy_buffer_stack_top) > 0)
-		--(yy_buffer_stack_top);
-
-	if (YY_CURRENT_BUFFER) {
-		smtlib_load_buffer_state( );
-		(yy_did_buffer_switch_on_eof) = 1;
-	}
-}
-
-/* Allocates the stack if it does not exist.
- *  Guarantees space for at least one push.
- */
-static void smtlibensure_buffer_stack (void)
-{
-	int num_to_alloc;
-    
-	if (!(yy_buffer_stack)) {
-
-		/* First allocation is just for 2 elements, since we don't know if this
-		 * scanner will even need a stack. We use 2 instead of 1 to avoid an
-		 * immediate realloc on the next call.
-         */
-		num_to_alloc = 1;
-		(yy_buffer_stack) = (struct yy_buffer_state**)smtliballoc
-								(num_to_alloc * sizeof(struct yy_buffer_state*)
-								);
-		if ( ! (yy_buffer_stack) )
-			YY_FATAL_ERROR( "out of dynamic memory in smtlibensure_buffer_stack()" );
-								  
-		memset((yy_buffer_stack), 0, num_to_alloc * sizeof(struct yy_buffer_state*));
-				
-		(yy_buffer_stack_max) = num_to_alloc;
-		(yy_buffer_stack_top) = 0;
-		return;
-	}
-
-	if ((yy_buffer_stack_top) >= ((yy_buffer_stack_max)) - 1){
-
-		/* Increase the buffer to prepare for a possible push. */
-		int grow_size = 8 /* arbitrary grow size */;
-
-		num_to_alloc = (yy_buffer_stack_max) + grow_size;
-		(yy_buffer_stack) = (struct yy_buffer_state**)smtlibrealloc
-								((yy_buffer_stack),
-								num_to_alloc * sizeof(struct yy_buffer_state*)
-								);
-		if ( ! (yy_buffer_stack) )
-			YY_FATAL_ERROR( "out of dynamic memory in smtlibensure_buffer_stack()" );
-
-		/* zero only the new slots.*/
-		memset((yy_buffer_stack) + (yy_buffer_stack_max), 0, grow_size * sizeof(struct yy_buffer_state*));
-		(yy_buffer_stack_max) = num_to_alloc;
-	}
-}
-
-/** Setup the input buffer state to scan directly from a user-specified character buffer.
- * @param base the character buffer
- * @param size the size in bytes of the character buffer
- * 
- * @return the newly allocated buffer state object. 
- */
-YY_BUFFER_STATE smtlib_scan_buffer  (char * base, yy_size_t  size )
-{
-	YY_BUFFER_STATE b;
-    
-	if ( size < 2 ||
-	     base[size-2] != YY_END_OF_BUFFER_CHAR ||
-	     base[size-1] != YY_END_OF_BUFFER_CHAR )
-		/* They forgot to leave room for the EOB's. */
-		return 0;
-
-	b = (YY_BUFFER_STATE) smtliballoc(sizeof( struct yy_buffer_state )  );
-	if ( ! b )
-		YY_FATAL_ERROR( "out of dynamic memory in smtlib_scan_buffer()" );
-
-	b->yy_buf_size = size - 2;	/* "- 2" to take care of EOB's */
-	b->yy_buf_pos = b->yy_ch_buf = base;
-	b->yy_is_our_buffer = 0;
-	b->yy_input_file = 0;
-	b->yy_n_chars = b->yy_buf_size;
-	b->yy_is_interactive = 0;
-	b->yy_at_bol = 1;
-	b->yy_fill_buffer = 0;
-	b->yy_buffer_status = YY_BUFFER_NEW;
-
-	smtlib_switch_to_buffer(b  );
-
-	return b;
-}
-
-/** Setup the input buffer state to scan a string. The next call to smtliblex() will
- * scan from a @e copy of @a str.
- * @param yystr a NUL-terminated string to scan
- * 
- * @return the newly allocated buffer state object.
- * @note If you want to scan bytes that may contain NUL values, then use
- *       smtlib_scan_bytes() instead.
- */
-YY_BUFFER_STATE smtlib_scan_string (yyconst char * yystr )
-{
-    
-	return smtlib_scan_bytes(yystr,strlen(yystr) );
-}
-
-/** Setup the input buffer state to scan the given bytes. The next call to smtliblex() will
- * scan from a @e copy of @a bytes.
- * @param bytes the byte buffer to scan
- * @param len the number of bytes in the buffer pointed to by @a bytes.
- * 
- * @return the newly allocated buffer state object.
- */
-YY_BUFFER_STATE smtlib_scan_bytes  (yyconst char * yybytes, int  _yybytes_len )
-{
-	YY_BUFFER_STATE b;
-	char *buf;
-	yy_size_t n;
-	int i;
-    
-	/* Get memory for full buffer, including space for trailing EOB's. */
-	n = _yybytes_len + 2;
-	buf = (char *) smtliballoc(n  );
-	if ( ! buf )
-		YY_FATAL_ERROR( "out of dynamic memory in smtlib_scan_bytes()" );
-
-	for ( i = 0; i < _yybytes_len; ++i )
-		buf[i] = yybytes[i];
-
-	buf[_yybytes_len] = buf[_yybytes_len+1] = YY_END_OF_BUFFER_CHAR;
-
-	b = smtlib_scan_buffer(buf,n );
-	if ( ! b )
-		YY_FATAL_ERROR( "bad buffer in smtlib_scan_bytes()" );
-
-	/* It's okay to grow etc. this buffer, and we should throw it
-	 * away when we're done.
-	 */
-	b->yy_is_our_buffer = 1;
-
-	return b;
-}
-
-#ifndef YY_EXIT_FAILURE
-#define YY_EXIT_FAILURE 2
-#endif
-
-static void yy_fatal_error (yyconst char* msg )
-{
-    	(void) fprintf( stderr, "%s\n", msg );
-	exit( YY_EXIT_FAILURE );
-}
-
-/* Redefine yyless() so it works in section 3 code. */
-
-#undef yyless
-#define yyless(n) \
-	do \
-		{ \
-		/* Undo effects of setting up smtlibtext. */ \
-        int yyless_macro_arg = (n); \
-        YY_LESS_LINENO(yyless_macro_arg);\
-		smtlibtext[smtlibleng] = (yy_hold_char); \
-		(yy_c_buf_p) = smtlibtext + yyless_macro_arg; \
-		(yy_hold_char) = *(yy_c_buf_p); \
-		*(yy_c_buf_p) = '\0'; \
-		smtlibleng = yyless_macro_arg; \
-		} \
-	while ( 0 )
-
-/* Accessor  methods (get/set functions) to struct members. */
-
-/** Get the current line number.
- * 
- */
-int smtlibget_lineno  (void)
-{
-        
-    return smtliblineno;
-}
-
-/** Get the input stream.
- * 
- */
-FILE *smtlibget_in  (void)
-{
-        return smtlibin;
-}
-
-/** Get the output stream.
- * 
- */
-FILE *smtlibget_out  (void)
-{
-        return smtlibout;
-}
-
-/** Get the length of the current token.
- * 
- */
-int smtlibget_leng  (void)
-{
-        return smtlibleng;
-}
-
-/** Get the current token.
- * 
- */
-
-char *smtlibget_text  (void)
-{
-        return smtlibtext;
-}
-
-/** Set the current line number.
- * @param line_number
- * 
- */
-void smtlibset_lineno (int  line_number )
-{
-    
-    smtliblineno = line_number;
-}
-
-/** Set the input stream. This does not discard the current
- * input buffer.
- * @param in_str A readable stream.
- * 
- * @see smtlib_switch_to_buffer
- */
-void smtlibset_in (FILE *  in_str )
-{
-        smtlibin = in_str ;
-}
-
-void smtlibset_out (FILE *  out_str )
-{
-        smtlibout = out_str ;
-}
-
-int smtlibget_debug  (void)
-{
-        return smtlib_flex_debug;
-}
-
-void smtlibset_debug (int  bdebug )
-{
-        smtlib_flex_debug = bdebug ;
-}
-
-static int yy_init_globals (void)
-{
-        /* Initialization is the same as for the non-reentrant scanner.
-     * This function is called from smtliblex_destroy(), so don't allocate here.
-     */
-
-    /* We do not touch smtliblineno unless the option is enabled. */
-    smtliblineno =  1;
-    
-    (yy_buffer_stack) = 0;
-    (yy_buffer_stack_top) = 0;
-    (yy_buffer_stack_max) = 0;
-    (yy_c_buf_p) = (char *) 0;
-    (yy_init) = 0;
-    (yy_start) = 0;
-
-/* Defined in main.c */
-#ifdef YY_STDINIT
-    smtlibin = stdin;
-    smtlibout = stdout;
-#else
-    smtlibin = (FILE *) 0;
-    smtlibout = (FILE *) 0;
-#endif
-
-    /* For future reference: Set errno on error, since we are called by
-     * smtliblex_init()
-     */
-    return 0;
-}
-
-/* smtliblex_destroy is for both reentrant and non-reentrant scanners. */
-int smtliblex_destroy  (void)
-{
-    
-    /* Pop the buffer stack, destroying each element. */
-	while(YY_CURRENT_BUFFER){
-		smtlib_delete_buffer(YY_CURRENT_BUFFER  );
-		YY_CURRENT_BUFFER_LVALUE = NULL;
-		smtlibpop_buffer_state();
-	}
-
-	/* Destroy the stack itself. */
-	smtlibfree((yy_buffer_stack) );
-	(yy_buffer_stack) = NULL;
-
-    /* Reset the globals. This is important in a non-reentrant scanner so the next time
-     * smtliblex() is called, initialization will occur. */
-    yy_init_globals( );
-
-    return 0;
-}
-
-/*
- * Internal utility routines.
- */
-
-#ifndef yytext_ptr
-static void yy_flex_strncpy (char* s1, yyconst char * s2, int n )
-{
-	register int i;
-	for ( i = 0; i < n; ++i )
-		s1[i] = s2[i];
-}
-#endif
-
-#ifdef YY_NEED_STRLEN
-static int yy_flex_strlen (yyconst char * s )
-{
-	register int n;
-	for ( n = 0; s[n]; ++n )
-		;
-
-	return n;
-}
-#endif
-
-void *smtliballoc (yy_size_t  size )
-{
-	return (void *) malloc( size );
-}
-
-void *smtlibrealloc  (void * ptr, yy_size_t  size )
-{
-	/* The cast to (char *) in the following accommodates both
-	 * implementations that use char* generic pointers, and those
-	 * that use void* generic pointers.  It works with the latter
-	 * because both ANSI C and C++ allow castless assignment from
-	 * any pointer type to void*, and deal with argument conversions
-	 * as though doing an assignment.
-	 */
-	return (void *) realloc( (char *) ptr, size );
-}
-
-void smtlibfree (void * ptr )
-{
-	free( (char *) ptr );	/* see smtlibrealloc() for (char *) cast */
-}
-
-#define YYTABLES_NAME "yytables"
-
-#line 221 "smtlib.lex"
-
-
-
-
diff --git a/lib/SMT/smtlib_parser.cpp b/lib/SMT/smtlib_parser.cpp
deleted file mode 100644
index c97a95ff..00000000
--- a/lib/SMT/smtlib_parser.cpp
+++ /dev/null
@@ -1,1829 +0,0 @@
-/* A Bison parser, made by GNU Bison 2.3.  */
-
-/* Skeleton implementation for Bison's Yacc-like parsers in C
-
-   Copyright (C) 1984, 1989, 1990, 2000, 2001, 2002, 2003, 2004, 2005, 2006
-   Free Software Foundation, Inc.
-
-   This program is free software; you can redistribute it and/or modify
-   it under the terms of the GNU General Public License as published by
-   the Free Software Foundation; either version 2, or (at your option)
-   any later version.
-
-   This program is distributed in the hope that it will be useful,
-   but WITHOUT ANY WARRANTY; without even the implied warranty of
-   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-   GNU General Public License for more details.
-
-   You should have received a copy of the GNU General Public License
-   along with this program; if not, write to the Free Software
-   Foundation, Inc., 51 Franklin Street, Fifth Floor,
-   Boston, MA 02110-1301, USA.  */
-
-/* As a special exception, you may create a larger work that contains
-   part or all of the Bison parser skeleton and distribute that work
-   under terms of your choice, so long as that work isn't itself a
-   parser generator using the skeleton or a modified version thereof
-   as a parser skeleton.  Alternatively, if you modify or redistribute
-   the parser skeleton itself, you may (at your option) remove this
-   special exception, which will cause the skeleton and the resulting
-   Bison output files to be licensed under the GNU General Public
-   License without this special exception.
-
-   This special exception was added by the Free Software Foundation in
-   version 2.2 of Bison.  */
-
-/* C LALR(1) parser skeleton written by Richard Stallman, by
-   simplifying the original so-called "semantic" parser.  */
-
-/* All symbols defined below should begin with yy or YY, to avoid
-   infringing on user name space.  This should be done even for local
-   variables, as they might otherwise be expanded by user macros.
-   There are some unavoidable exceptions within include files to
-   define necessary library symbols; they are noted "INFRINGES ON
-   USER NAME SPACE" below.  */
-
-/* Identify Bison output.  */
-#define YYBISON 1
-
-/* Bison version.  */
-#define YYBISON_VERSION "2.3"
-
-/* Skeleton name.  */
-#define YYSKELETON_NAME "yacc.c"
-
-/* Pure parsers.  */
-#define YYPURE 0
-
-/* Using locations.  */
-#define YYLSP_NEEDED 0
-
-/* Substitute the variable and function names.  */
-#define yyparse smtlibparse
-#define yylex   smtliblex
-#define yyerror smtliberror
-#define yylval  smtliblval
-#define yychar  smtlibchar
-#define yydebug smtlibdebug
-#define yynerrs smtlibnerrs
-
-
-/* Tokens.  */
-#ifndef YYTOKENTYPE
-# define YYTOKENTYPE
-   /* Put the tokens into the symbol table, so that GDB and other debuggers
-      know about them.  */
-   enum yytokentype {
-     NUMERAL_TOK = 258,
-     SYM_TOK = 259,
-     STRING_TOK = 260,
-     AR_SYMB = 261,
-     USER_VAL_TOK = 262,
-     TRUE_TOK = 263,
-     FALSE_TOK = 264,
-     ITE_TOK = 265,
-     NOT_TOK = 266,
-     IMPLIES_TOK = 267,
-     IF_THEN_ELSE_TOK = 268,
-     AND_TOK = 269,
-     OR_TOK = 270,
-     XOR_TOK = 271,
-     IFF_TOK = 272,
-     EXISTS_TOK = 273,
-     FORALL_TOK = 274,
-     LET_TOK = 275,
-     FLET_TOK = 276,
-     NOTES_TOK = 277,
-     CVC_COMMAND_TOK = 278,
-     SORTS_TOK = 279,
-     FUNS_TOK = 280,
-     PREDS_TOK = 281,
-     EXTENSIONS_TOK = 282,
-     DEFINITION_TOK = 283,
-     AXIOMS_TOK = 284,
-     LOGIC_TOK = 285,
-     COLON_TOK = 286,
-     LBRACKET_TOK = 287,
-     RBRACKET_TOK = 288,
-     LCURBRACK_TOK = 289,
-     RCURBRACK_TOK = 290,
-     LPAREN_TOK = 291,
-     RPAREN_TOK = 292,
-     SAT_TOK = 293,
-     UNSAT_TOK = 294,
-     UNKNOWN_TOK = 295,
-     ASSUMPTION_TOK = 296,
-     FORMULA_TOK = 297,
-     STATUS_TOK = 298,
-     BENCHMARK_TOK = 299,
-     EXTRASORTS_TOK = 300,
-     EXTRAFUNS_TOK = 301,
-     EXTRAPREDS_TOK = 302,
-     LANGUAGE_TOK = 303,
-     DOLLAR_TOK = 304,
-     QUESTION_TOK = 305,
-     DISTINCT_TOK = 306,
-     SEMICOLON_TOK = 307,
-     EOF_TOK = 308,
-     PAT_TOK = 309
-   };
-#endif
-/* Tokens.  */
-#define NUMERAL_TOK 258
-#define SYM_TOK 259
-#define STRING_TOK 260
-#define AR_SYMB 261
-#define USER_VAL_TOK 262
-#define TRUE_TOK 263
-#define FALSE_TOK 264
-#define ITE_TOK 265
-#define NOT_TOK 266
-#define IMPLIES_TOK 267
-#define IF_THEN_ELSE_TOK 268
-#define AND_TOK 269
-#define OR_TOK 270
-#define XOR_TOK 271
-#define IFF_TOK 272
-#define EXISTS_TOK 273
-#define FORALL_TOK 274
-#define LET_TOK 275
-#define FLET_TOK 276
-#define NOTES_TOK 277
-#define CVC_COMMAND_TOK 278
-#define SORTS_TOK 279
-#define FUNS_TOK 280
-#define PREDS_TOK 281
-#define EXTENSIONS_TOK 282
-#define DEFINITION_TOK 283
-#define AXIOMS_TOK 284
-#define LOGIC_TOK 285
-#define COLON_TOK 286
-#define LBRACKET_TOK 287
-#define RBRACKET_TOK 288
-#define LCURBRACK_TOK 289
-#define RCURBRACK_TOK 290
-#define LPAREN_TOK 291
-#define RPAREN_TOK 292
-#define SAT_TOK 293
-#define UNSAT_TOK 294
-#define UNKNOWN_TOK 295
-#define ASSUMPTION_TOK 296
-#define FORMULA_TOK 297
-#define STATUS_TOK 298
-#define BENCHMARK_TOK 299
-#define EXTRASORTS_TOK 300
-#define EXTRAFUNS_TOK 301
-#define EXTRAPREDS_TOK 302
-#define LANGUAGE_TOK 303
-#define DOLLAR_TOK 304
-#define QUESTION_TOK 305
-#define DISTINCT_TOK 306
-#define SEMICOLON_TOK 307
-#define EOF_TOK 308
-#define PAT_TOK 309
-
-
-
-
-/* Copy the first part of user declarations.  */
-#line 1 "smtlib.y"
-
-/*****************************************************************************/
-/*!
- * \file smtlib.y
- * 
- * Author: Clark Barrett
- * 
- * Created: Apr 30 2005
- *
- * <hr>
- *
- * License to use, copy, modify, sell and/or distribute this software
- * and its documentation for any purpose is hereby granted without
- * royalty, subject to the terms and conditions defined in the \ref
- * LICENSE file provided with this distribution.
- * 
- * <hr>
- * 
- */
-/*****************************************************************************/
-/* 
-   This file contains the bison code for the parser that reads in CVC
-   commands in SMT-LIB language.
-*/
-
-//#include "vc.h"
-#include "parser_temp.h"
-
-// Exported shared data
-namespace CVC3 {
-  extern ParserTemp* parserTemp;
-}
-// Define shortcuts for various things
-#define TMP CVC3::parserTemp
-#define EXPR CVC3::parserTemp->expr
-//#define VC (CVC3::parserTemp->vc)
-#define ARRAYSENABLED (CVC3::parserTemp->arrFlag)
-#define BVENABLED (CVC3::parserTemp->bvFlag)
-#define BVSIZE (CVC3::parserTemp->bvSize)
-#define RAT(args) CVC3::newRational args
-#define QUERYPARSED CVC3::parserTemp->queryParsed
-
-// Suppress the bogus warning suppression in bison (it generates
-// compile error)
-#undef __GNUC_MINOR__
-
-/* stuff that lives in smtlib.lex */
-extern int smtliblex(void);
-
-int smtliberror(const char *s)
-{
-  std::ostringstream ss;
-  ss << CVC3::parserTemp->fileName << ":" << CVC3::parserTemp->lineNum
-     << ": " << s;
-  return CVC3::parserTemp->error(ss.str());
-}
-
-
-
-#define YYLTYPE_IS_TRIVIAL 1
-#define YYMAXDEPTH 10485760
-
-
-
-/* Enabling traces.  */
-#ifndef YYDEBUG
-# define YYDEBUG 0
-#endif
-
-/* Enabling verbose error messages.  */
-#ifdef YYERROR_VERBOSE
-# undef YYERROR_VERBOSE
-# define YYERROR_VERBOSE 1
-#else
-# define YYERROR_VERBOSE 0
-#endif
-
-/* Enabling the token table.  */
-#ifndef YYTOKEN_TABLE
-# define YYTOKEN_TABLE 0
-#endif
-
-#if ! defined YYSTYPE && ! defined YYSTYPE_IS_DECLARED
-typedef union YYSTYPE
-#line 76 "smtlib.y"
-{
-  std::string *str;
-  std::vector<std::string> *strvec;
-  klee::expr::ExprHandle* node;
-  std::vector<void*> *vec;
-}
-/* Line 187 of yacc.c.  */
-#line 283 "smtlib_parser.cpp"
-	YYSTYPE;
-# define yystype YYSTYPE /* obsolescent; will be withdrawn */
-# define YYSTYPE_IS_DECLARED 1
-# define YYSTYPE_IS_TRIVIAL 1
-#endif
-
-
-
-/* Copy the second part of user declarations.  */
-
-
-/* Line 216 of yacc.c.  */
-#line 296 "smtlib_parser.cpp"
-
-#ifdef short
-# undef short
-#endif
-
-#ifdef YYTYPE_UINT8
-typedef YYTYPE_UINT8 yytype_uint8;
-#else
-typedef unsigned char yytype_uint8;
-#endif
-
-#ifdef YYTYPE_INT8
-typedef YYTYPE_INT8 yytype_int8;
-#elif (defined __STDC__ || defined __C99__FUNC__ \
-     || defined __cplusplus || defined _MSC_VER)
-typedef signed char yytype_int8;
-#else
-typedef short int yytype_int8;
-#endif
-
-#ifdef YYTYPE_UINT16
-typedef YYTYPE_UINT16 yytype_uint16;
-#else
-typedef unsigned short int yytype_uint16;
-#endif
-
-#ifdef YYTYPE_INT16
-typedef YYTYPE_INT16 yytype_int16;
-#else
-typedef short int yytype_int16;
-#endif
-
-#ifndef YYSIZE_T
-# ifdef __SIZE_TYPE__
-#  define YYSIZE_T __SIZE_TYPE__
-# elif defined size_t
-#  define YYSIZE_T size_t
-# elif ! defined YYSIZE_T && (defined __STDC__ || defined __C99__FUNC__ \
-     || defined __cplusplus || defined _MSC_VER)
-#  include <stddef.h> /* INFRINGES ON USER NAME SPACE */
-#  define YYSIZE_T size_t
-# else
-#  define YYSIZE_T unsigned int
-# endif
-#endif
-
-#define YYSIZE_MAXIMUM ((YYSIZE_T) -1)
-
-#ifndef YY_
-# if YYENABLE_NLS
-#  if ENABLE_NLS
-#   include <libintl.h> /* INFRINGES ON USER NAME SPACE */
-#   define YY_(msgid) dgettext ("bison-runtime", msgid)
-#  endif
-# endif
-# ifndef YY_
-#  define YY_(msgid) msgid
-# endif
-#endif
-
-/* Suppress unused-variable warnings by "using" E.  */
-#if ! defined lint || defined __GNUC__
-# define YYUSE(e) ((void) (e))
-#else
-# define YYUSE(e) /* empty */
-#endif
-
-/* Identity function, used to suppress warnings about constant conditions.  */
-#ifndef lint
-# define YYID(n) (n)
-#else
-#if (defined __STDC__ || defined __C99__FUNC__ \
-     || defined __cplusplus || defined _MSC_VER)
-static int
-YYID (int i)
-#else
-static int
-YYID (i)
-    int i;
-#endif
-{
-  return i;
-}
-#endif
-
-#if ! defined yyoverflow || YYERROR_VERBOSE
-
-/* The parser invokes alloca or malloc; define the necessary symbols.  */
-
-# ifdef YYSTACK_USE_ALLOCA
-#  if YYSTACK_USE_ALLOCA
-#   ifdef __GNUC__
-#    define YYSTACK_ALLOC __builtin_alloca
-#   elif defined __BUILTIN_VA_ARG_INCR
-#    include <alloca.h> /* INFRINGES ON USER NAME SPACE */
-#   elif defined _AIX
-#    define YYSTACK_ALLOC __alloca
-#   elif defined _MSC_VER
-#    include <malloc.h> /* INFRINGES ON USER NAME SPACE */
-#    define alloca _alloca
-#   else
-#    define YYSTACK_ALLOC alloca
-#    if ! defined _ALLOCA_H && ! defined _STDLIB_H && (defined __STDC__ || defined __C99__FUNC__ \
-     || defined __cplusplus || defined _MSC_VER)
-#     include <stdlib.h> /* INFRINGES ON USER NAME SPACE */
-#     ifndef _STDLIB_H
-#      define _STDLIB_H 1
-#     endif
-#    endif
-#   endif
-#  endif
-# endif
-
-# ifdef YYSTACK_ALLOC
-   /* Pacify GCC's `empty if-body' warning.  */
-#  define YYSTACK_FREE(Ptr) do { /* empty */; } while (YYID (0))
-#  ifndef YYSTACK_ALLOC_MAXIMUM
-    /* The OS might guarantee only one guard page at the bottom of the stack,
-       and a page size can be as small as 4096 bytes.  So we cannot safely
-       invoke alloca (N) if N exceeds 4096.  Use a slightly smaller number
-       to allow for a few compiler-allocated temporary stack slots.  */
-#   define YYSTACK_ALLOC_MAXIMUM 4032 /* reasonable circa 2006 */
-#  endif
-# else
-#  define YYSTACK_ALLOC YYMALLOC
-#  define YYSTACK_FREE YYFREE
-#  ifndef YYSTACK_ALLOC_MAXIMUM
-#   define YYSTACK_ALLOC_MAXIMUM YYSIZE_MAXIMUM
-#  endif
-#  if (defined __cplusplus && ! defined _STDLIB_H \
-       && ! ((defined YYMALLOC || defined malloc) \
-	     && (defined YYFREE || defined free)))
-#   include <stdlib.h> /* INFRINGES ON USER NAME SPACE */
-#   ifndef _STDLIB_H
-#    define _STDLIB_H 1
-#   endif
-#  endif
-#  ifndef YYMALLOC
-#   define YYMALLOC malloc
-#   if ! defined malloc && ! defined _STDLIB_H && (defined __STDC__ || defined __C99__FUNC__ \
-     || defined __cplusplus || defined _MSC_VER)
-void *malloc (YYSIZE_T); /* INFRINGES ON USER NAME SPACE */
-#   endif
-#  endif
-#  ifndef YYFREE
-#   define YYFREE free
-#   if ! defined free && ! defined _STDLIB_H && (defined __STDC__ || defined __C99__FUNC__ \
-     || defined __cplusplus || defined _MSC_VER)
-void free (void *); /* INFRINGES ON USER NAME SPACE */
-#   endif
-#  endif
-# endif
-#endif /* ! defined yyoverflow || YYERROR_VERBOSE */
-
-
-#if (! defined yyoverflow \
-     && (! defined __cplusplus \
-	 || (defined YYSTYPE_IS_TRIVIAL && YYSTYPE_IS_TRIVIAL)))
-
-/* A type that is properly aligned for any stack member.  */
-union yyalloc
-{
-  yytype_int16 yyss;
-  YYSTYPE yyvs;
-  };
-
-/* The size of the maximum gap between one aligned stack and the next.  */
-# define YYSTACK_GAP_MAXIMUM (sizeof (union yyalloc) - 1)
-
-/* The size of an array large to enough to hold all stacks, each with
-   N elements.  */
-# define YYSTACK_BYTES(N) \
-     ((N) * (sizeof (yytype_int16) + sizeof (YYSTYPE)) \
-      + YYSTACK_GAP_MAXIMUM)
-
-/* Copy COUNT objects from FROM to TO.  The source and destination do
-   not overlap.  */
-# ifndef YYCOPY
-#  if defined __GNUC__ && 1 < __GNUC__
-#   define YYCOPY(To, From, Count) \
-      __builtin_memcpy (To, From, (Count) * sizeof (*(From)))
-#  else
-#   define YYCOPY(To, From, Count)		\
-      do					\
-	{					\
-	  YYSIZE_T yyi;				\
-	  for (yyi = 0; yyi < (Count); yyi++)	\
-	    (To)[yyi] = (From)[yyi];		\
-	}					\
-      while (YYID (0))
-#  endif
-# endif
-
-/* Relocate STACK from its old location to the new one.  The
-   local variables YYSIZE and YYSTACKSIZE give the old and new number of
-   elements in the stack, and YYPTR gives the new location of the
-   stack.  Advance YYPTR to a properly aligned location for the next
-   stack.  */
-# define YYSTACK_RELOCATE(Stack)					\
-    do									\
-      {									\
-	YYSIZE_T yynewbytes;						\
-	YYCOPY (&yyptr->Stack, Stack, yysize);				\
-	Stack = &yyptr->Stack;						\
-	yynewbytes = yystacksize * sizeof (*Stack) + YYSTACK_GAP_MAXIMUM; \
-	yyptr += yynewbytes / sizeof (*yyptr);				\
-      }									\
-    while (YYID (0))
-
-#endif
-
-/* YYFINAL -- State number of the termination state.  */
-#define YYFINAL  6
-/* YYLAST -- Last index in YYTABLE.  */
-#define YYLAST   17
-
-/* YYNTOKENS -- Number of terminals.  */
-#define YYNTOKENS  55
-/* YYNNTS -- Number of nonterminals.  */
-#define YYNNTS  9
-/* YYNRULES -- Number of rules.  */
-#define YYNRULES  12
-/* YYNRULES -- Number of states.  */
-#define YYNSTATES  21
-
-/* YYTRANSLATE(YYLEX) -- Bison symbol number corresponding to YYLEX.  */
-#define YYUNDEFTOK  2
-#define YYMAXUTOK   309
-
-#define YYTRANSLATE(YYX)						\
-  ((unsigned int) (YYX) <= YYMAXUTOK ? yytranslate[YYX] : YYUNDEFTOK)
-
-/* YYTRANSLATE[YYLEX] -- Bison symbol number corresponding to YYLEX.  */
-static const yytype_uint8 yytranslate[] =
-{
-       0,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
-       2,     2,     2,     2,     2,     2,     1,     2,     3,     4,
-       5,     6,     7,     8,     9,    10,    11,    12,    13,    14,
-      15,    16,    17,    18,    19,    20,    21,    22,    23,    24,
-      25,    26,    27,    28,    29,    30,    31,    32,    33,    34,
-      35,    36,    37,    38,    39,    40,    41,    42,    43,    44,
-      45,    46,    47,    48,    49,    50,    51,    52,    53,    54
-};
-
-#if YYDEBUG
-/* YYPRHS[YYN] -- Index of the first RHS symbol of rule number YYN in
-   YYRHS.  */
-static const yytype_uint8 yyprhs[] =
-{
-       0,     0,     3,     5,    11,    13,    15,    17,    21,    25,
-      27,    29,    31
-};
-
-/* YYRHS -- A `-1'-separated list of the rules' RHS.  */
-static const yytype_int8 yyrhs[] =
-{
-      56,     0,    -1,    57,    -1,    36,    44,    58,    59,    37,
-      -1,    53,    -1,     4,    -1,    60,    -1,    31,    41,    61,
-      -1,    31,    42,    61,    -1,    62,    -1,    63,    -1,     8,
-      -1,     9,    -1
-};
-
-/* YYRLINE[YYN] -- source line where rule number YYN was defined.  */
-static const yytype_uint16 yyrline[] =
-{
-       0,   159,   159,   171,   181,   190,   198,   222,   230,   490,
-     691,   761,   766
-};
-#endif
-
-#if YYDEBUG || YYERROR_VERBOSE || YYTOKEN_TABLE
-/* YYTNAME[SYMBOL-NUM] -- String name of the symbol SYMBOL-NUM.
-   First, the terminals, then, starting at YYNTOKENS, nonterminals.  */
-static const char *const yytname[] =
-{
-  "$end", "error", "$undefined", "NUMERAL_TOK", "SYM_TOK", "STRING_TOK",
-  "AR_SYMB", "USER_VAL_TOK", "TRUE_TOK", "FALSE_TOK", "ITE_TOK", "NOT_TOK",
-  "IMPLIES_TOK", "IF_THEN_ELSE_TOK", "AND_TOK", "OR_TOK", "XOR_TOK",
-  "IFF_TOK", "EXISTS_TOK", "FORALL_TOK", "LET_TOK", "FLET_TOK",
-  "NOTES_TOK", "CVC_COMMAND_TOK", "SORTS_TOK", "FUNS_TOK", "PREDS_TOK",
-  "EXTENSIONS_TOK", "DEFINITION_TOK", "AXIOMS_TOK", "LOGIC_TOK",
-  "COLON_TOK", "LBRACKET_TOK", "RBRACKET_TOK", "LCURBRACK_TOK",
-  "RCURBRACK_TOK", "LPAREN_TOK", "RPAREN_TOK", "SAT_TOK", "UNSAT_TOK",
-  "UNKNOWN_TOK", "ASSUMPTION_TOK", "FORMULA_TOK", "STATUS_TOK",
-  "BENCHMARK_TOK", "EXTRASORTS_TOK", "EXTRAFUNS_TOK", "EXTRAPREDS_TOK",
-  "LANGUAGE_TOK", "DOLLAR_TOK", "QUESTION_TOK", "DISTINCT_TOK",
-  "SEMICOLON_TOK", "EOF_TOK", "PAT_TOK", "$accept", "cmd", "benchmark",
-  "bench_name", "bench_attributes", "bench_attribute", "an_formula",
-  "an_atom", "prop_atom", 0
-};
-#endif
-
-# ifdef YYPRINT
-/* YYTOKNUM[YYLEX-NUM] -- Internal token number corresponding to
-   token YYLEX-NUM.  */
-static const yytype_uint16 yytoknum[] =
-{
-       0,   256,   257,   258,   259,   260,   261,   262,   263,   264,
-     265,   266,   267,   268,   269,   270,   271,   272,   273,   274,
-     275,   276,   277,   278,   279,   280,   281,   282,   283,   284,
-     285,   286,   287,   288,   289,   290,   291,   292,   293,   294,
-     295,   296,   297,   298,   299,   300,   301,   302,   303,   304,
-     305,   306,   307,   308,   309
-};
-# endif
-
-/* YYR1[YYN] -- Symbol number of symbol that rule YYN derives.  */
-static const yytype_uint8 yyr1[] =
-{
-       0,    55,    56,    57,    57,    58,    59,    60,    60,    61,
-      62,    63,    63
-};
-
-/* YYR2[YYN] -- Number of symbols composing right hand side of rule YYN.  */
-static const yytype_uint8 yyr2[] =
-{
-       0,     2,     1,     5,     1,     1,     1,     3,     3,     1,
-       1,     1,     1
-};
-
-/* YYDEFACT[STATE-NAME] -- Default rule to reduce with in state
-   STATE-NUM when YYTABLE doesn't specify something else to do.  Zero
-   means the default is an error.  */
-static const yytype_uint8 yydefact[] =
-{
-       0,     0,     4,     0,     2,     0,     1,     5,     0,     0,
-       0,     6,     0,     0,     3,    11,    12,     7,     9,    10,
-       8
-};
-
-/* YYDEFGOTO[NTERM-NUM].  */
-static const yytype_int8 yydefgoto[] =
-{
-      -1,     3,     4,     8,    10,    11,    17,    18,    19
-};
-
-/* YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing
-   STATE-NUM.  */
-#define YYPACT_NINF -41
-static const yytype_int8 yypact[] =
-{
-     -36,   -39,   -41,     6,   -41,     3,   -41,   -41,   -23,   -40,
-     -28,   -41,    -5,    -5,   -41,   -41,   -41,   -41,   -41,   -41,
-     -41
-};
-
-/* YYPGOTO[NTERM-NUM].  */
-static const yytype_int8 yypgoto[] =
-{
-     -41,   -41,   -41,   -41,   -41,   -41,    -3,   -41,   -41
-};
-
-/* YYTABLE[YYPACT[STATE-NUM]].  What to do in state STATE-NUM.  If
-   positive, shift that token.  If negative, reduce the rule which
-   number is the opposite.  If zero, do what YYDEFACT says.
-   If YYTABLE_NINF, syntax error.  */
-#define YYTABLE_NINF -1
-static const yytype_uint8 yytable[] =
-{
-       1,    12,    13,    15,    16,     5,     6,     7,     9,    14,
-      20,     0,     0,     0,     0,     0,     0,     2
-};
-
-static const yytype_int8 yycheck[] =
-{
-      36,    41,    42,     8,     9,    44,     0,     4,    31,    37,
-      13,    -1,    -1,    -1,    -1,    -1,    -1,    53
-};
-
-/* YYSTOS[STATE-NUM] -- The (internal number of the) accessing
-   symbol of state STATE-NUM.  */
-static const yytype_uint8 yystos[] =
-{
-       0,    36,    53,    56,    57,    44,     0,     4,    58,    31,
-      59,    60,    41,    42,    37,     8,     9,    61,    62,    63,
-      61
-};
-
-#define yyerrok		(yyerrstatus = 0)
-#define yyclearin	(yychar = YYEMPTY)
-#define YYEMPTY		(-2)
-#define YYEOF		0
-
-#define YYACCEPT	goto yyacceptlab
-#define YYABORT		goto yyabortlab
-#define YYERROR		goto yyerrorlab
-
-
-/* Like YYERROR except do call yyerror.  This remains here temporarily
-   to ease the transition to the new meaning of YYERROR, for GCC.
-   Once GCC version 2 has supplanted version 1, this can go.  */
-
-#define YYFAIL		goto yyerrlab
-
-#define YYRECOVERING()  (!!yyerrstatus)
-
-#define YYBACKUP(Token, Value)					\
-do								\
-  if (yychar == YYEMPTY && yylen == 1)				\
-    {								\
-      yychar = (Token);						\
-      yylval = (Value);						\
-      yytoken = YYTRANSLATE (yychar);				\
-      YYPOPSTACK (1);						\
-      goto yybackup;						\
-    }								\
-  else								\
-    {								\
-      yyerror (YY_("syntax error: cannot back up")); \
-      YYERROR;							\
-    }								\
-while (YYID (0))
-
-
-#define YYTERROR	1
-#define YYERRCODE	256
-
-
-/* YYLLOC_DEFAULT -- Set CURRENT to span from RHS[1] to RHS[N].
-   If N is 0, then set CURRENT to the empty location which ends
-   the previous symbol: RHS[0] (always defined).  */
-
-#define YYRHSLOC(Rhs, K) ((Rhs)[K])
-#ifndef YYLLOC_DEFAULT
-# define YYLLOC_DEFAULT(Current, Rhs, N)				\
-    do									\
-      if (YYID (N))                                                    \
-	{								\
-	  (Current).first_line   = YYRHSLOC (Rhs, 1).first_line;	\
-	  (Current).first_column = YYRHSLOC (Rhs, 1).first_column;	\
-	  (Current).last_line    = YYRHSLOC (Rhs, N).last_line;		\
-	  (Current).last_column  = YYRHSLOC (Rhs, N).last_column;	\
-	}								\
-      else								\
-	{								\
-	  (Current).first_line   = (Current).last_line   =		\
-	    YYRHSLOC (Rhs, 0).last_line;				\
-	  (Current).first_column = (Current).last_column =		\
-	    YYRHSLOC (Rhs, 0).last_column;				\
-	}								\
-    while (YYID (0))
-#endif
-
-
-/* YY_LOCATION_PRINT -- Print the location on the stream.
-   This macro was not mandated originally: define only if we know
-   we won't break user code: when these are the locations we know.  */
-
-#ifndef YY_LOCATION_PRINT
-# if YYLTYPE_IS_TRIVIAL
-#  define YY_LOCATION_PRINT(File, Loc)			\
-     fprintf (File, "%d.%d-%d.%d",			\
-	      (Loc).first_line, (Loc).first_column,	\
-	      (Loc).last_line,  (Loc).last_column)
-# else
-#  define YY_LOCATION_PRINT(File, Loc) ((void) 0)
-# endif
-#endif
-
-
-/* YYLEX -- calling `yylex' with the right arguments.  */
-
-#ifdef YYLEX_PARAM
-# define YYLEX yylex (YYLEX_PARAM)
-#else
-# define YYLEX yylex ()
-#endif
-
-/* Enable debugging if requested.  */
-#if YYDEBUG
-
-# ifndef YYFPRINTF
-#  include <stdio.h> /* INFRINGES ON USER NAME SPACE */
-#  define YYFPRINTF fprintf
-# endif
-
-# define YYDPRINTF(Args)			\
-do {						\
-  if (yydebug)					\
-    YYFPRINTF Args;				\
-} while (YYID (0))
-
-# define YY_SYMBOL_PRINT(Title, Type, Value, Location)			  \
-do {									  \
-  if (yydebug)								  \
-    {									  \
-      YYFPRINTF (stderr, "%s ", Title);					  \
-      yy_symbol_print (stderr,						  \
-		  Type, Value); \
-      YYFPRINTF (stderr, "\n");						  \
-    }									  \
-} while (YYID (0))
-
-
-/*--------------------------------.
-| Print this symbol on YYOUTPUT.  |
-`--------------------------------*/
-
-/*ARGSUSED*/
-#if (defined __STDC__ || defined __C99__FUNC__ \
-     || defined __cplusplus || defined _MSC_VER)
-static void
-yy_symbol_value_print (FILE *yyoutput, int yytype, YYSTYPE const * const yyvaluep)
-#else
-static void
-yy_symbol_value_print (yyoutput, yytype, yyvaluep)
-    FILE *yyoutput;
-    int yytype;
-    YYSTYPE const * const yyvaluep;
-#endif
-{
-  if (!yyvaluep)
-    return;
-# ifdef YYPRINT
-  if (yytype < YYNTOKENS)
-    YYPRINT (yyoutput, yytoknum[yytype], *yyvaluep);
-# else
-  YYUSE (yyoutput);
-# endif
-  switch (yytype)
-    {
-      default:
-	break;
-    }
-}
-
-
-/*--------------------------------.
-| Print this symbol on YYOUTPUT.  |
-`--------------------------------*/
-
-#if (defined __STDC__ || defined __C99__FUNC__ \
-     || defined __cplusplus || defined _MSC_VER)
-static void
-yy_symbol_print (FILE *yyoutput, int yytype, YYSTYPE const * const yyvaluep)
-#else
-static void
-yy_symbol_print (yyoutput, yytype, yyvaluep)
-    FILE *yyoutput;
-    int yytype;
-    YYSTYPE const * const yyvaluep;
-#endif
-{
-  if (yytype < YYNTOKENS)
-    YYFPRINTF (yyoutput, "token %s (", yytname[yytype]);
-  else
-    YYFPRINTF (yyoutput, "nterm %s (", yytname[yytype]);
-
-  yy_symbol_value_print (yyoutput, yytype, yyvaluep);
-  YYFPRINTF (yyoutput, ")");
-}
-
-/*------------------------------------------------------------------.
-| yy_stack_print -- Print the state stack from its BOTTOM up to its |
-| TOP (included).                                                   |
-`------------------------------------------------------------------*/
-
-#if (defined __STDC__ || defined __C99__FUNC__ \
-     || defined __cplusplus || defined _MSC_VER)
-static void
-yy_stack_print (yytype_int16 *bottom, yytype_int16 *top)
-#else
-static void
-yy_stack_print (bottom, top)
-    yytype_int16 *bottom;
-    yytype_int16 *top;
-#endif
-{
-  YYFPRINTF (stderr, "Stack now");
-  for (; bottom <= top; ++bottom)
-    YYFPRINTF (stderr, " %d", *bottom);
-  YYFPRINTF (stderr, "\n");
-}
-
-# define YY_STACK_PRINT(Bottom, Top)				\
-do {								\
-  if (yydebug)							\
-    yy_stack_print ((Bottom), (Top));				\
-} while (YYID (0))
-
-
-/*------------------------------------------------.
-| Report that the YYRULE is going to be reduced.  |
-`------------------------------------------------*/
-
-#if (defined __STDC__ || defined __C99__FUNC__ \
-     || defined __cplusplus || defined _MSC_VER)
-static void
-yy_reduce_print (YYSTYPE *yyvsp, int yyrule)
-#else
-static void
-yy_reduce_print (yyvsp, yyrule)
-    YYSTYPE *yyvsp;
-    int yyrule;
-#endif
-{
-  int yynrhs = yyr2[yyrule];
-  int yyi;
-  unsigned long int yylno = yyrline[yyrule];
-  YYFPRINTF (stderr, "Reducing stack by rule %d (line %lu):\n",
-	     yyrule - 1, yylno);
-  /* The symbols being reduced.  */
-  for (yyi = 0; yyi < yynrhs; yyi++)
-    {
-      fprintf (stderr, "   $%d = ", yyi + 1);
-      yy_symbol_print (stderr, yyrhs[yyprhs[yyrule] + yyi],
-		       &(yyvsp[(yyi + 1) - (yynrhs)])
-		       		       );
-      fprintf (stderr, "\n");
-    }
-}
-
-# define YY_REDUCE_PRINT(Rule)		\
-do {					\
-  if (yydebug)				\
-    yy_reduce_print (yyvsp, Rule); \
-} while (YYID (0))
-
-/* Nonzero means print parse trace.  It is left uninitialized so that
-   multiple parsers can coexist.  */
-int yydebug;
-#else /* !YYDEBUG */
-# define YYDPRINTF(Args)
-# define YY_SYMBOL_PRINT(Title, Type, Value, Location)
-# define YY_STACK_PRINT(Bottom, Top)
-# define YY_REDUCE_PRINT(Rule)
-#endif /* !YYDEBUG */
-
-
-/* YYINITDEPTH -- initial size of the parser's stacks.  */
-#ifndef	YYINITDEPTH
-# define YYINITDEPTH 200
-#endif
-
-/* YYMAXDEPTH -- maximum size the stacks can grow to (effective only
-   if the built-in stack extension method is used).
-
-   Do not make this value too large; the results are undefined if
-   YYSTACK_ALLOC_MAXIMUM < YYSTACK_BYTES (YYMAXDEPTH)
-   evaluated with infinite-precision integer arithmetic.  */
-
-#ifndef YYMAXDEPTH
-# define YYMAXDEPTH 10000
-#endif
-
-
-
-#if YYERROR_VERBOSE
-
-# ifndef yystrlen
-#  if defined __GLIBC__ && defined _STRING_H
-#   define yystrlen strlen
-#  else
-/* Return the length of YYSTR.  */
-#if (defined __STDC__ || defined __C99__FUNC__ \
-     || defined __cplusplus || defined _MSC_VER)
-static YYSIZE_T
-yystrlen (const char *yystr)
-#else
-static YYSIZE_T
-yystrlen (yystr)
-    const char *yystr;
-#endif
-{
-  YYSIZE_T yylen;
-  for (yylen = 0; yystr[yylen]; yylen++)
-    continue;
-  return yylen;
-}
-#  endif
-# endif
-
-# ifndef yystpcpy
-#  if defined __GLIBC__ && defined _STRING_H && defined _GNU_SOURCE
-#   define yystpcpy stpcpy
-#  else
-/* Copy YYSRC to YYDEST, returning the address of the terminating '\0' in
-   YYDEST.  */
-#if (defined __STDC__ || defined __C99__FUNC__ \
-     || defined __cplusplus || defined _MSC_VER)
-static char *
-yystpcpy (char *yydest, const char *yysrc)
-#else
-static char *
-yystpcpy (yydest, yysrc)
-    char *yydest;
-    const char *yysrc;
-#endif
-{
-  char *yyd = yydest;
-  const char *yys = yysrc;
-
-  while ((*yyd++ = *yys++) != '\0')
-    continue;
-
-  return yyd - 1;
-}
-#  endif
-# endif
-
-# ifndef yytnamerr
-/* Copy to YYRES the contents of YYSTR after stripping away unnecessary
-   quotes and backslashes, so that it's suitable for yyerror.  The
-   heuristic is that double-quoting is unnecessary unless the string
-   contains an apostrophe, a comma, or backslash (other than
-   backslash-backslash).  YYSTR is taken from yytname.  If YYRES is
-   null, do not copy; instead, return the length of what the result
-   would have been.  */
-static YYSIZE_T
-yytnamerr (char *yyres, const char *yystr)
-{
-  if (*yystr == '"')
-    {
-      YYSIZE_T yyn = 0;
-      char const *yyp = yystr;
-
-      for (;;)
-	switch (*++yyp)
-	  {
-	  case '\'':
-	  case ',':
-	    goto do_not_strip_quotes;
-
-	  case '\\':
-	    if (*++yyp != '\\')
-	      goto do_not_strip_quotes;
-	    /* Fall through.  */
-	  default:
-	    if (yyres)
-	      yyres[yyn] = *yyp;
-	    yyn++;
-	    break;
-
-	  case '"':
-	    if (yyres)
-	      yyres[yyn] = '\0';
-	    return yyn;
-	  }
-    do_not_strip_quotes: ;
-    }
-
-  if (! yyres)
-    return yystrlen (yystr);
-
-  return yystpcpy (yyres, yystr) - yyres;
-}
-# endif
-
-/* Copy into YYRESULT an error message about the unexpected token
-   YYCHAR while in state YYSTATE.  Return the number of bytes copied,
-   including the terminating null byte.  If YYRESULT is null, do not
-   copy anything; just return the number of bytes that would be
-   copied.  As a special case, return 0 if an ordinary "syntax error"
-   message will do.  Return YYSIZE_MAXIMUM if overflow occurs during
-   size calculation.  */
-static YYSIZE_T
-yysyntax_error (char *yyresult, int yystate, int yychar)
-{
-  int yyn = yypact[yystate];
-
-  if (! (YYPACT_NINF < yyn && yyn <= YYLAST))
-    return 0;
-  else
-    {
-      int yytype = YYTRANSLATE (yychar);
-      YYSIZE_T yysize0 = yytnamerr (0, yytname[yytype]);
-      YYSIZE_T yysize = yysize0;
-      YYSIZE_T yysize1;
-      int yysize_overflow = 0;
-      enum { YYERROR_VERBOSE_ARGS_MAXIMUM = 5 };
-      char const *yyarg[YYERROR_VERBOSE_ARGS_MAXIMUM];
-      int yyx;
-
-# if 0
-      /* This is so xgettext sees the translatable formats that are
-	 constructed on the fly.  */
-      YY_("syntax error, unexpected %s");
-      YY_("syntax error, unexpected %s, expecting %s");
-      YY_("syntax error, unexpected %s, expecting %s or %s");
-      YY_("syntax error, unexpected %s, expecting %s or %s or %s");
-      YY_("syntax error, unexpected %s, expecting %s or %s or %s or %s");
-# endif
-      char *yyfmt;
-      char const *yyf;
-      static char const yyunexpected[] = "syntax error, unexpected %s";
-      static char const yyexpecting[] = ", expecting %s";
-      static char const yyor[] = " or %s";
-      char yyformat[sizeof yyunexpected
-		    + sizeof yyexpecting - 1
-		    + ((YYERROR_VERBOSE_ARGS_MAXIMUM - 2)
-		       * (sizeof yyor - 1))];
-      char const *yyprefix = yyexpecting;
-
-      /* Start YYX at -YYN if negative to avoid negative indexes in
-	 YYCHECK.  */
-      int yyxbegin = yyn < 0 ? -yyn : 0;
-
-      /* Stay within bounds of both yycheck and yytname.  */
-      int yychecklim = YYLAST - yyn + 1;
-      int yyxend = yychecklim < YYNTOKENS ? yychecklim : YYNTOKENS;
-      int yycount = 1;
-
-      yyarg[0] = yytname[yytype];
-      yyfmt = yystpcpy (yyformat, yyunexpected);
-
-      for (yyx = yyxbegin; yyx < yyxend; ++yyx)
-	if (yycheck[yyx + yyn] == yyx && yyx != YYTERROR)
-	  {
-	    if (yycount == YYERROR_VERBOSE_ARGS_MAXIMUM)
-	      {
-		yycount = 1;
-		yysize = yysize0;
-		yyformat[sizeof yyunexpected - 1] = '\0';
-		break;
-	      }
-	    yyarg[yycount++] = yytname[yyx];
-	    yysize1 = yysize + yytnamerr (0, yytname[yyx]);
-	    yysize_overflow |= (yysize1 < yysize);
-	    yysize = yysize1;
-	    yyfmt = yystpcpy (yyfmt, yyprefix);
-	    yyprefix = yyor;
-	  }
-
-      yyf = YY_(yyformat);
-      yysize1 = yysize + yystrlen (yyf);
-      yysize_overflow |= (yysize1 < yysize);
-      yysize = yysize1;
-
-      if (yysize_overflow)
-	return YYSIZE_MAXIMUM;
-
-      if (yyresult)
-	{
-	  /* Avoid sprintf, as that infringes on the user's name space.
-	     Don't have undefined behavior even if the translation
-	     produced a string with the wrong number of "%s"s.  */
-	  char *yyp = yyresult;
-	  int yyi = 0;
-	  while ((*yyp = *yyf) != '\0')
-	    {
-	      if (*yyp == '%' && yyf[1] == 's' && yyi < yycount)
-		{
-		  yyp += yytnamerr (yyp, yyarg[yyi++]);
-		  yyf += 2;
-		}
-	      else
-		{
-		  yyp++;
-		  yyf++;
-		}
-	    }
-	}
-      return yysize;
-    }
-}
-#endif /* YYERROR_VERBOSE */
-
-
-/*-----------------------------------------------.
-| Release the memory associated to this symbol.  |
-`-----------------------------------------------*/
-
-/*ARGSUSED*/
-#if (defined __STDC__ || defined __C99__FUNC__ \
-     || defined __cplusplus || defined _MSC_VER)
-static void
-yydestruct (const char *yymsg, int yytype, YYSTYPE *yyvaluep)
-#else
-static void
-yydestruct (yymsg, yytype, yyvaluep)
-    const char *yymsg;
-    int yytype;
-    YYSTYPE *yyvaluep;
-#endif
-{
-  YYUSE (yyvaluep);
-
-  if (!yymsg)
-    yymsg = "Deleting";
-  YY_SYMBOL_PRINT (yymsg, yytype, yyvaluep, yylocationp);
-
-  switch (yytype)
-    {
-
-      default:
-	break;
-    }
-}
-
-
-/* Prevent warnings from -Wmissing-prototypes.  */
-
-#ifdef YYPARSE_PARAM
-#if defined __STDC__ || defined __cplusplus
-int yyparse (void *YYPARSE_PARAM);
-#else
-int yyparse ();
-#endif
-#else /* ! YYPARSE_PARAM */
-#if defined __STDC__ || defined __cplusplus
-int yyparse (void);
-#else
-int yyparse ();
-#endif
-#endif /* ! YYPARSE_PARAM */
-
-
-
-/* The look-ahead symbol.  */
-int yychar;
-
-/* The semantic value of the look-ahead symbol.  */
-YYSTYPE yylval;
-
-/* Number of syntax errors so far.  */
-int yynerrs;
-
-
-
-/*----------.
-| yyparse.  |
-`----------*/
-
-#ifdef YYPARSE_PARAM
-#if (defined __STDC__ || defined __C99__FUNC__ \
-     || defined __cplusplus || defined _MSC_VER)
-int
-yyparse (void *YYPARSE_PARAM)
-#else
-int
-yyparse (YYPARSE_PARAM)
-    void *YYPARSE_PARAM;
-#endif
-#else /* ! YYPARSE_PARAM */
-#if (defined __STDC__ || defined __C99__FUNC__ \
-     || defined __cplusplus || defined _MSC_VER)
-int
-yyparse (void)
-#else
-int
-yyparse ()
-
-#endif
-#endif
-{
-  
-  int yystate;
-  int yyn;
-  int yyresult;
-  /* Number of tokens to shift before error messages enabled.  */
-  int yyerrstatus;
-  /* Look-ahead token as an internal (translated) token number.  */
-  int yytoken = 0;
-#if YYERROR_VERBOSE
-  /* Buffer for error messages, and its allocated size.  */
-  char yymsgbuf[128];
-  char *yymsg = yymsgbuf;
-  YYSIZE_T yymsg_alloc = sizeof yymsgbuf;
-#endif
-
-  /* Three stacks and their tools:
-     `yyss': related to states,
-     `yyvs': related to semantic values,
-     `yyls': related to locations.
-
-     Refer to the stacks thru separate pointers, to allow yyoverflow
-     to reallocate them elsewhere.  */
-
-  /* The state stack.  */
-  yytype_int16 yyssa[YYINITDEPTH];
-  yytype_int16 *yyss = yyssa;
-  yytype_int16 *yyssp;
-
-  /* The semantic value stack.  */
-  YYSTYPE yyvsa[YYINITDEPTH];
-  YYSTYPE *yyvs = yyvsa;
-  YYSTYPE *yyvsp;
-
-
-
-#define YYPOPSTACK(N)   (yyvsp -= (N), yyssp -= (N))
-
-  YYSIZE_T yystacksize = YYINITDEPTH;
-
-  /* The variables used to return semantic value and location from the
-     action routines.  */
-  YYSTYPE yyval;
-
-
-  /* The number of symbols on the RHS of the reduced rule.
-     Keep to zero when no symbol should be popped.  */
-  int yylen = 0;
-
-  YYDPRINTF ((stderr, "Starting parse\n"));
-
-  yystate = 0;
-  yyerrstatus = 0;
-  yynerrs = 0;
-  yychar = YYEMPTY;		/* Cause a token to be read.  */
-
-  /* Initialize stack pointers.
-     Waste one element of value and location stack
-     so that they stay on the same level as the state stack.
-     The wasted elements are never initialized.  */
-
-  yyssp = yyss;
-  yyvsp = yyvs;
-
-  goto yysetstate;
-
-/*------------------------------------------------------------.
-| yynewstate -- Push a new state, which is found in yystate.  |
-`------------------------------------------------------------*/
- yynewstate:
-  /* In all cases, when you get here, the value and location stacks
-     have just been pushed.  So pushing a state here evens the stacks.  */
-  yyssp++;
-
- yysetstate:
-  *yyssp = yystate;
-
-  if (yyss + yystacksize - 1 <= yyssp)
-    {
-      /* Get the current used size of the three stacks, in elements.  */
-      YYSIZE_T yysize = yyssp - yyss + 1;
-
-#ifdef yyoverflow
-      {
-	/* Give user a chance to reallocate the stack.  Use copies of
-	   these so that the &'s don't force the real ones into
-	   memory.  */
-	YYSTYPE *yyvs1 = yyvs;
-	yytype_int16 *yyss1 = yyss;
-
-
-	/* Each stack pointer address is followed by the size of the
-	   data in use in that stack, in bytes.  This used to be a
-	   conditional around just the two extra args, but that might
-	   be undefined if yyoverflow is a macro.  */
-	yyoverflow (YY_("memory exhausted"),
-		    &yyss1, yysize * sizeof (*yyssp),
-		    &yyvs1, yysize * sizeof (*yyvsp),
-
-		    &yystacksize);
-
-	yyss = yyss1;
-	yyvs = yyvs1;
-      }
-#else /* no yyoverflow */
-# ifndef YYSTACK_RELOCATE
-      goto yyexhaustedlab;
-# else
-      /* Extend the stack our own way.  */
-      if (YYMAXDEPTH <= yystacksize)
-	goto yyexhaustedlab;
-      yystacksize *= 2;
-      if (YYMAXDEPTH < yystacksize)
-	yystacksize = YYMAXDEPTH;
-
-      {
-	yytype_int16 *yyss1 = yyss;
-	union yyalloc *yyptr =
-	  (union yyalloc *) YYSTACK_ALLOC (YYSTACK_BYTES (yystacksize));
-	if (! yyptr)
-	  goto yyexhaustedlab;
-	YYSTACK_RELOCATE (yyss);
-	YYSTACK_RELOCATE (yyvs);
-
-#  undef YYSTACK_RELOCATE
-	if (yyss1 != yyssa)
-	  YYSTACK_FREE (yyss1);
-      }
-# endif
-#endif /* no yyoverflow */
-
-      yyssp = yyss + yysize - 1;
-      yyvsp = yyvs + yysize - 1;
-
-
-      YYDPRINTF ((stderr, "Stack size increased to %lu\n",
-		  (unsigned long int) yystacksize));
-
-      if (yyss + yystacksize - 1 <= yyssp)
-	YYABORT;
-    }
-
-  YYDPRINTF ((stderr, "Entering state %d\n", yystate));
-
-  goto yybackup;
-
-/*-----------.
-| yybackup.  |
-`-----------*/
-yybackup:
-
-  /* Do appropriate processing given the current state.  Read a
-     look-ahead token if we need one and don't already have one.  */
-
-  /* First try to decide what to do without reference to look-ahead token.  */
-  yyn = yypact[yystate];
-  if (yyn == YYPACT_NINF)
-    goto yydefault;
-
-  /* Not known => get a look-ahead token if don't already have one.  */
-
-  /* YYCHAR is either YYEMPTY or YYEOF or a valid look-ahead symbol.  */
-  if (yychar == YYEMPTY)
-    {
-      YYDPRINTF ((stderr, "Reading a token: "));
-      yychar = YYLEX;
-    }
-
-  if (yychar <= YYEOF)
-    {
-      yychar = yytoken = YYEOF;
-      YYDPRINTF ((stderr, "Now at end of input.\n"));
-    }
-  else
-    {
-      yytoken = YYTRANSLATE (yychar);
-      YY_SYMBOL_PRINT ("Next token is", yytoken, &yylval, &yylloc);
-    }
-
-  /* If the proper action on seeing token YYTOKEN is to reduce or to
-     detect an error, take that action.  */
-  yyn += yytoken;
-  if (yyn < 0 || YYLAST < yyn || yycheck[yyn] != yytoken)
-    goto yydefault;
-  yyn = yytable[yyn];
-  if (yyn <= 0)
-    {
-      if (yyn == 0 || yyn == YYTABLE_NINF)
-	goto yyerrlab;
-      yyn = -yyn;
-      goto yyreduce;
-    }
-
-  if (yyn == YYFINAL)
-    YYACCEPT;
-
-  /* Count tokens shifted since error; after three, turn off error
-     status.  */
-  if (yyerrstatus)
-    yyerrstatus--;
-
-  /* Shift the look-ahead token.  */
-  YY_SYMBOL_PRINT ("Shifting", yytoken, &yylval, &yylloc);
-
-  /* Discard the shifted token unless it is eof.  */
-  if (yychar != YYEOF)
-    yychar = YYEMPTY;
-
-  yystate = yyn;
-  *++yyvsp = yylval;
-
-  goto yynewstate;
-
-
-/*-----------------------------------------------------------.
-| yydefault -- do the default action for the current state.  |
-`-----------------------------------------------------------*/
-yydefault:
-  yyn = yydefact[yystate];
-  if (yyn == 0)
-    goto yyerrlab;
-  goto yyreduce;
-
-
-/*-----------------------------.
-| yyreduce -- Do a reduction.  |
-`-----------------------------*/
-yyreduce:
-  /* yyn is the number of a rule to reduce with.  */
-  yylen = yyr2[yyn];
-
-  /* If YYLEN is nonzero, implement the default value of the action:
-     `$$ = $1'.
-
-     Otherwise, the following line sets YYVAL to garbage.
-     This behavior is undocumented and Bison
-     users should not rely upon it.  Assigning to YYVAL
-     unconditionally makes the parser a bit smaller, and it avoids a
-     GCC warning that YYVAL may be used uninitialized.  */
-  yyval = yyvsp[1-yylen];
-
-
-  YY_REDUCE_PRINT (yyn);
-  switch (yyn)
-    {
-        case 2:
-#line 160 "smtlib.y"
-    {
-      /*
-      EXPR = *$1;
-      delete $1;
-      */
-      EXPR = (yyvsp[(1) - (1)].node);
-      YYACCEPT;
-    ;}
-    break;
-
-  case 3:
-#line 172 "smtlib.y"
-    {
-      /*
-      if (!QUERYPARSED)
-        $4->push_back(CVC3::Expr(VC->listExpr("_CHECKSAT", CVC3::Expr(VC->idExpr("_TRUE_EXPR")))));
-      $$ = new CVC3::Expr(VC->listExpr("_SEQ",*$4));
-      delete $4;
-      */
-      (yyval.node) = NULL;
-    ;}
-    break;
-
-  case 4:
-#line 182 "smtlib.y"
-    { 
-      TMP->done = true;
-      //$$ = new CVC3::Expr();
-      (yyval.node) = NULL;
-    ;}
-    break;
-
-  case 5:
-#line 191 "smtlib.y"
-    {
-      (yyval.node) = NULL;
-      delete (yyvsp[(1) - (1)].str);
-    ;}
-    break;
-
-  case 6:
-#line 199 "smtlib.y"
-    {
-      (yyval.node) = (yyvsp[(1) - (1)].node);
-    ;}
-    break;
-
-  case 7:
-#line 223 "smtlib.y"
-    {
-      /*
-      $$ = new CVC3::Expr(VC->listExpr("_ASSERT", *$3));      
-      delete $3;
-      */
-      (yyval.node) = (yyvsp[(3) - (3)].node);
-    ;}
-    break;
-
-  case 8:
-#line 231 "smtlib.y"
-    {
-      /*
-      $$ = new CVC3::Expr(VC->listExpr("_CHECKSAT", *$3));
-      QUERYPARSED = true;
-      delete $3;
-      */
-      (yyval.node) = (yyvsp[(3) - (3)].node);
-    ;}
-    break;
-
-  case 9:
-#line 491 "smtlib.y"
-    {
-      (yyval.node) = (yyvsp[(1) - (1)].node);
-    ;}
-    break;
-
-  case 10:
-#line 692 "smtlib.y"
-    {
-      (yyval.node) = (yyvsp[(1) - (1)].node);
-    ;}
-    break;
-
-  case 11:
-#line 762 "smtlib.y"
-    {
-      //$$ = new CVC3::Expr(VC->idExpr("_TRUE_EXPR"));
-      (yyval.node) = NULL;
-    ;}
-    break;
-
-  case 12:
-#line 767 "smtlib.y"
-    { 
-      //$$ = new CVC3::Expr(VC->idExpr("_FALSE_EXPR"));
-      (yyval.node) = NULL;
-    ;}
-    break;
-
-
-/* Line 1267 of yacc.c.  */
-#line 1614 "smtlib_parser.cpp"
-      default: break;
-    }
-  YY_SYMBOL_PRINT ("-> $$ =", yyr1[yyn], &yyval, &yyloc);
-
-  YYPOPSTACK (yylen);
-  yylen = 0;
-  YY_STACK_PRINT (yyss, yyssp);
-
-  *++yyvsp = yyval;
-
-
-  /* Now `shift' the result of the reduction.  Determine what state
-     that goes to, based on the state we popped back to and the rule
-     number reduced by.  */
-
-  yyn = yyr1[yyn];
-
-  yystate = yypgoto[yyn - YYNTOKENS] + *yyssp;
-  if (0 <= yystate && yystate <= YYLAST && yycheck[yystate] == *yyssp)
-    yystate = yytable[yystate];
-  else
-    yystate = yydefgoto[yyn - YYNTOKENS];
-
-  goto yynewstate;
-
-
-/*------------------------------------.
-| yyerrlab -- here on detecting error |
-`------------------------------------*/
-yyerrlab:
-  /* If not already recovering from an error, report this error.  */
-  if (!yyerrstatus)
-    {
-      ++yynerrs;
-#if ! YYERROR_VERBOSE
-      yyerror (YY_("syntax error"));
-#else
-      {
-	YYSIZE_T yysize = yysyntax_error (0, yystate, yychar);
-	if (yymsg_alloc < yysize && yymsg_alloc < YYSTACK_ALLOC_MAXIMUM)
-	  {
-	    YYSIZE_T yyalloc = 2 * yysize;
-	    if (! (yysize <= yyalloc && yyalloc <= YYSTACK_ALLOC_MAXIMUM))
-	      yyalloc = YYSTACK_ALLOC_MAXIMUM;
-	    if (yymsg != yymsgbuf)
-	      YYSTACK_FREE (yymsg);
-	    yymsg = (char *) YYSTACK_ALLOC (yyalloc);
-	    if (yymsg)
-	      yymsg_alloc = yyalloc;
-	    else
-	      {
-		yymsg = yymsgbuf;
-		yymsg_alloc = sizeof yymsgbuf;
-	      }
-	  }
-
-	if (0 < yysize && yysize <= yymsg_alloc)
-	  {
-	    (void) yysyntax_error (yymsg, yystate, yychar);
-	    yyerror (yymsg);
-	  }
-	else
-	  {
-	    yyerror (YY_("syntax error"));
-	    if (yysize != 0)
-	      goto yyexhaustedlab;
-	  }
-      }
-#endif
-    }
-
-
-
-  if (yyerrstatus == 3)
-    {
-      /* If just tried and failed to reuse look-ahead token after an
-	 error, discard it.  */
-
-      if (yychar <= YYEOF)
-	{
-	  /* Return failure if at end of input.  */
-	  if (yychar == YYEOF)
-	    YYABORT;
-	}
-      else
-	{
-	  yydestruct ("Error: discarding",
-		      yytoken, &yylval);
-	  yychar = YYEMPTY;
-	}
-    }
-
-  /* Else will try to reuse look-ahead token after shifting the error
-     token.  */
-  goto yyerrlab1;
-
-
-/*---------------------------------------------------.
-| yyerrorlab -- error raised explicitly by YYERROR.  |
-`---------------------------------------------------*/
-yyerrorlab:
-
-  /* Pacify compilers like GCC when the user code never invokes
-     YYERROR and the label yyerrorlab therefore never appears in user
-     code.  */
-  if (/*CONSTCOND*/ 0)
-     goto yyerrorlab;
-
-  /* Do not reclaim the symbols of the rule which action triggered
-     this YYERROR.  */
-  YYPOPSTACK (yylen);
-  yylen = 0;
-  YY_STACK_PRINT (yyss, yyssp);
-  yystate = *yyssp;
-  goto yyerrlab1;
-
-
-/*-------------------------------------------------------------.
-| yyerrlab1 -- common code for both syntax error and YYERROR.  |
-`-------------------------------------------------------------*/
-yyerrlab1:
-  yyerrstatus = 3;	/* Each real token shifted decrements this.  */
-
-  for (;;)
-    {
-      yyn = yypact[yystate];
-      if (yyn != YYPACT_NINF)
-	{
-	  yyn += YYTERROR;
-	  if (0 <= yyn && yyn <= YYLAST && yycheck[yyn] == YYTERROR)
-	    {
-	      yyn = yytable[yyn];
-	      if (0 < yyn)
-		break;
-	    }
-	}
-
-      /* Pop the current state because it cannot handle the error token.  */
-      if (yyssp == yyss)
-	YYABORT;
-
-
-      yydestruct ("Error: popping",
-		  yystos[yystate], yyvsp);
-      YYPOPSTACK (1);
-      yystate = *yyssp;
-      YY_STACK_PRINT (yyss, yyssp);
-    }
-
-  if (yyn == YYFINAL)
-    YYACCEPT;
-
-  *++yyvsp = yylval;
-
-
-  /* Shift the error token.  */
-  YY_SYMBOL_PRINT ("Shifting", yystos[yyn], yyvsp, yylsp);
-
-  yystate = yyn;
-  goto yynewstate;
-
-
-/*-------------------------------------.
-| yyacceptlab -- YYACCEPT comes here.  |
-`-------------------------------------*/
-yyacceptlab:
-  yyresult = 0;
-  goto yyreturn;
-
-/*-----------------------------------.
-| yyabortlab -- YYABORT comes here.  |
-`-----------------------------------*/
-yyabortlab:
-  yyresult = 1;
-  goto yyreturn;
-
-#ifndef yyoverflow
-/*-------------------------------------------------.
-| yyexhaustedlab -- memory exhaustion comes here.  |
-`-------------------------------------------------*/
-yyexhaustedlab:
-  yyerror (YY_("memory exhausted"));
-  yyresult = 2;
-  /* Fall through.  */
-#endif
-
-yyreturn:
-  if (yychar != YYEOF && yychar != YYEMPTY)
-     yydestruct ("Cleanup: discarding lookahead",
-		 yytoken, &yylval);
-  /* Do not reclaim the symbols of the rule which action triggered
-     this YYABORT or YYACCEPT.  */
-  YYPOPSTACK (yylen);
-  YY_STACK_PRINT (yyss, yyssp);
-  while (yyssp != yyss)
-    {
-      yydestruct ("Cleanup: popping",
-		  yystos[*yyssp], yyvsp);
-      YYPOPSTACK (1);
-    }
-#ifndef yyoverflow
-  if (yyss != yyssa)
-    YYSTACK_FREE (yyss);
-#endif
-#if YYERROR_VERBOSE
-  if (yymsg != yymsgbuf)
-    YYSTACK_FREE (yymsg);
-#endif
-  /* Make sure YYID is used.  */
-  return YYID (yyresult);
-}
-
-
-#line 1270 "smtlib.y"
-
-
diff --git a/lib/SMT/smtlib_parser.h b/lib/SMT/smtlib_parser.h
deleted file mode 100644
index 1544c35e..00000000
--- a/lib/SMT/smtlib_parser.h
+++ /dev/null
@@ -1,171 +0,0 @@
-/* A Bison parser, made by GNU Bison 2.3.  */
-
-/* Skeleton interface for Bison's Yacc-like parsers in C
-
-   Copyright (C) 1984, 1989, 1990, 2000, 2001, 2002, 2003, 2004, 2005, 2006
-   Free Software Foundation, Inc.
-
-   This program is free software; you can redistribute it and/or modify
-   it under the terms of the GNU General Public License as published by
-   the Free Software Foundation; either version 2, or (at your option)
-   any later version.
-
-   This program is distributed in the hope that it will be useful,
-   but WITHOUT ANY WARRANTY; without even the implied warranty of
-   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-   GNU General Public License for more details.
-
-   You should have received a copy of the GNU General Public License
-   along with this program; if not, write to the Free Software
-   Foundation, Inc., 51 Franklin Street, Fifth Floor,
-   Boston, MA 02110-1301, USA.  */
-
-/* As a special exception, you may create a larger work that contains
-   part or all of the Bison parser skeleton and distribute that work
-   under terms of your choice, so long as that work isn't itself a
-   parser generator using the skeleton or a modified version thereof
-   as a parser skeleton.  Alternatively, if you modify or redistribute
-   the parser skeleton itself, you may (at your option) remove this
-   special exception, which will cause the skeleton and the resulting
-   Bison output files to be licensed under the GNU General Public
-   License without this special exception.
-
-   This special exception was added by the Free Software Foundation in
-   version 2.2 of Bison.  */
-
-/* Tokens.  */
-#ifndef YYTOKENTYPE
-# define YYTOKENTYPE
-   /* Put the tokens into the symbol table, so that GDB and other debuggers
-      know about them.  */
-   enum yytokentype {
-     NUMERAL_TOK = 258,
-     SYM_TOK = 259,
-     STRING_TOK = 260,
-     AR_SYMB = 261,
-     USER_VAL_TOK = 262,
-     TRUE_TOK = 263,
-     FALSE_TOK = 264,
-     ITE_TOK = 265,
-     NOT_TOK = 266,
-     IMPLIES_TOK = 267,
-     IF_THEN_ELSE_TOK = 268,
-     AND_TOK = 269,
-     OR_TOK = 270,
-     XOR_TOK = 271,
-     IFF_TOK = 272,
-     EXISTS_TOK = 273,
-     FORALL_TOK = 274,
-     LET_TOK = 275,
-     FLET_TOK = 276,
-     NOTES_TOK = 277,
-     CVC_COMMAND_TOK = 278,
-     SORTS_TOK = 279,
-     FUNS_TOK = 280,
-     PREDS_TOK = 281,
-     EXTENSIONS_TOK = 282,
-     DEFINITION_TOK = 283,
-     AXIOMS_TOK = 284,
-     LOGIC_TOK = 285,
-     COLON_TOK = 286,
-     LBRACKET_TOK = 287,
-     RBRACKET_TOK = 288,
-     LCURBRACK_TOK = 289,
-     RCURBRACK_TOK = 290,
-     LPAREN_TOK = 291,
-     RPAREN_TOK = 292,
-     SAT_TOK = 293,
-     UNSAT_TOK = 294,
-     UNKNOWN_TOK = 295,
-     ASSUMPTION_TOK = 296,
-     FORMULA_TOK = 297,
-     STATUS_TOK = 298,
-     BENCHMARK_TOK = 299,
-     EXTRASORTS_TOK = 300,
-     EXTRAFUNS_TOK = 301,
-     EXTRAPREDS_TOK = 302,
-     LANGUAGE_TOK = 303,
-     DOLLAR_TOK = 304,
-     QUESTION_TOK = 305,
-     DISTINCT_TOK = 306,
-     SEMICOLON_TOK = 307,
-     EOF_TOK = 308,
-     PAT_TOK = 309
-   };
-#endif
-/* Tokens.  */
-#define NUMERAL_TOK 258
-#define SYM_TOK 259
-#define STRING_TOK 260
-#define AR_SYMB 261
-#define USER_VAL_TOK 262
-#define TRUE_TOK 263
-#define FALSE_TOK 264
-#define ITE_TOK 265
-#define NOT_TOK 266
-#define IMPLIES_TOK 267
-#define IF_THEN_ELSE_TOK 268
-#define AND_TOK 269
-#define OR_TOK 270
-#define XOR_TOK 271
-#define IFF_TOK 272
-#define EXISTS_TOK 273
-#define FORALL_TOK 274
-#define LET_TOK 275
-#define FLET_TOK 276
-#define NOTES_TOK 277
-#define CVC_COMMAND_TOK 278
-#define SORTS_TOK 279
-#define FUNS_TOK 280
-#define PREDS_TOK 281
-#define EXTENSIONS_TOK 282
-#define DEFINITION_TOK 283
-#define AXIOMS_TOK 284
-#define LOGIC_TOK 285
-#define COLON_TOK 286
-#define LBRACKET_TOK 287
-#define RBRACKET_TOK 288
-#define LCURBRACK_TOK 289
-#define RCURBRACK_TOK 290
-#define LPAREN_TOK 291
-#define RPAREN_TOK 292
-#define SAT_TOK 293
-#define UNSAT_TOK 294
-#define UNKNOWN_TOK 295
-#define ASSUMPTION_TOK 296
-#define FORMULA_TOK 297
-#define STATUS_TOK 298
-#define BENCHMARK_TOK 299
-#define EXTRASORTS_TOK 300
-#define EXTRAFUNS_TOK 301
-#define EXTRAPREDS_TOK 302
-#define LANGUAGE_TOK 303
-#define DOLLAR_TOK 304
-#define QUESTION_TOK 305
-#define DISTINCT_TOK 306
-#define SEMICOLON_TOK 307
-#define EOF_TOK 308
-#define PAT_TOK 309
-
-
-
-
-#if ! defined YYSTYPE && ! defined YYSTYPE_IS_DECLARED
-typedef union YYSTYPE
-#line 76 "smtlib.y"
-{
-  std::string *str;
-  std::vector<std::string> *strvec;
-  klee::expr::ExprHandle* node;
-  std::vector<void*> *vec;
-}
-/* Line 1489 of yacc.c.  */
-#line 164 "smtlib_parser.hpp"
-	YYSTYPE;
-# define yystype YYSTYPE /* obsolescent; will be withdrawn */
-# define YYSTYPE_IS_DECLARED 1
-# define YYSTYPE_IS_TRIVIAL 1
-#endif
-
-extern YYSTYPE smtliblval;
-