First attempt at incorporating LFSC proof checker into CVC4.

27 files changed, 7435 insertions, 0 deletions

diff --git a/proofs/lfsc_checker/.gitignore b/proofs/lfsc_checker/.gitignore
new file mode 100644
index 000000000..1f799d15a
--- /dev/null
+++ b/proofs/lfsc_checker/.gitignore
@@ -0,0 +1,16 @@
+/autom4te.cache
+/stamp-h
+/config.h.in
+/config.log
+/config.status
+/config.cache
+/libtool
+/stamp-h1
+.dep
+Makefile.in
+/configure
+/aclocal.m4
+*~
+\#*\#
+/config/
+*.swp
diff --git a/proofs/lfsc_checker/AUTHORS b/proofs/lfsc_checker/AUTHORS
new file mode 100644
index 000000000..0bd0a37b0
--- /dev/null
+++ b/proofs/lfsc_checker/AUTHORS
@@ -0,0 +1,5 @@
+The core authors and designers of the LFSC proof checker are:
+
+  Andy Reynolds
+  Aaron Stump
+
diff --git a/proofs/lfsc_checker/COPYING b/proofs/lfsc_checker/COPYING
new file mode 100644
index 000000000..b220a3147
--- /dev/null
+++ b/proofs/lfsc_checker/COPYING
@@ -0,0 +1,17 @@
+LFSC is copyright (C) 2012, 2013 The University of Iowa.
+All rights reserved.
+
+LFSC is open-source; distribution is under the terms of the modified
+BSD license.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS
+AS IS AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/proofs/lfsc_checker/INSTALL b/proofs/lfsc_checker/INSTALL
new file mode 100644
index 000000000..a1e89e18a
--- /dev/null
+++ b/proofs/lfsc_checker/INSTALL
@@ -0,0 +1,370 @@
+Installation Instructions
+*************************
+
+Copyright (C) 1994-1996, 1999-2002, 2004-2011 Free Software Foundation,
+Inc.
+
+   Copying and distribution of this file, with or without modification,
+are permitted in any medium without royalty provided the copyright
+notice and this notice are preserved.  This file is offered as-is,
+without warranty of any kind.
+
+Basic Installation
+==================
+
+   Briefly, the shell commands `./configure; make; make install' should
+configure, build, and install this package.  The following
+more-detailed instructions are generic; see the `README' file for
+instructions specific to this package.  Some packages provide this
+`INSTALL' file but do not implement all of the features documented
+below.  The lack of an optional feature in a given package is not
+necessarily a bug.  More recommendations for GNU packages can be found
+in *note Makefile Conventions: (standards)Makefile Conventions.
+
+   The `configure' shell script attempts to guess correct values for
+various system-dependent variables used during compilation.  It uses
+those values to create a `Makefile' in each directory of the package.
+It may also create one or more `.h' files containing system-dependent
+definitions.  Finally, it creates a shell script `config.status' that
+you can run in the future to recreate the current configuration, and a
+file `config.log' containing compiler output (useful mainly for
+debugging `configure').
+
+   It can also use an optional file (typically called `config.cache'
+and enabled with `--cache-file=config.cache' or simply `-C') that saves
+the results of its tests to speed up reconfiguring.  Caching is
+disabled by default to prevent problems with accidental use of stale
+cache files.
+
+   If you need to do unusual things to compile the package, please try
+to figure out how `configure' could check whether to do them, and mail
+diffs or instructions to the address given in the `README' so they can
+be considered for the next release.  If you are using the cache, and at
+some point `config.cache' contains results you don't want to keep, you
+may remove or edit it.
+
+   The file `configure.ac' (or `configure.in') is used to create
+`configure' by a program called `autoconf'.  You need `configure.ac' if
+you want to change it or regenerate `configure' using a newer version
+of `autoconf'.
+
+   The simplest way to compile this package is:
+
+  1. `cd' to the directory containing the package's source code and type
+     `./configure' to configure the package for your system.
+
+     Running `configure' might take a while.  While running, it prints
+     some messages telling which features it is checking for.
+
+  2. Type `make' to compile the package.
+
+  3. Optionally, type `make check' to run any self-tests that come with
+     the package, generally using the just-built uninstalled binaries.
+
+  4. Type `make install' to install the programs and any data files and
+     documentation.  When installing into a prefix owned by root, it is
+     recommended that the package be configured and built as a regular
+     user, and only the `make install' phase executed with root
+     privileges.
+
+  5. Optionally, type `make installcheck' to repeat any self-tests, but
+     this time using the binaries in their final installed location.
+     This target does not install anything.  Running this target as a
+     regular user, particularly if the prior `make install' required
+     root privileges, verifies that the installation completed
+     correctly.
+
+  6. You can remove the program binaries and object files from the
+     source code directory by typing `make clean'.  To also remove the
+     files that `configure' created (so you can compile the package for
+     a different kind of computer), type `make distclean'.  There is
+     also a `make maintainer-clean' target, but that is intended mainly
+     for the package's developers.  If you use it, you may have to get
+     all sorts of other programs in order to regenerate files that came
+     with the distribution.
+
+  7. Often, you can also type `make uninstall' to remove the installed
+     files again.  In practice, not all packages have tested that
+     uninstallation works correctly, even though it is required by the
+     GNU Coding Standards.
+
+  8. Some packages, particularly those that use Automake, provide `make
+     distcheck', which can by used by developers to test that all other
+     targets like `make install' and `make uninstall' work correctly.
+     This target is generally not run by end users.
+
+Compilers and Options
+=====================
+
+   Some systems require unusual options for compilation or linking that
+the `configure' script does not know about.  Run `./configure --help'
+for details on some of the pertinent environment variables.
+
+   You can give `configure' initial values for configuration parameters
+by setting variables in the command line or in the environment.  Here
+is an example:
+
+     ./configure CC=c99 CFLAGS=-g LIBS=-lposix
+
+   *Note Defining Variables::, for more details.
+
+Compiling For Multiple Architectures
+====================================
+
+   You can compile the package for more than one kind of computer at the
+same time, by placing the object files for each architecture in their
+own directory.  To do this, you can use GNU `make'.  `cd' to the
+directory where you want the object files and executables to go and run
+the `configure' script.  `configure' automatically checks for the
+source code in the directory that `configure' is in and in `..'.  This
+is known as a "VPATH" build.
+
+   With a non-GNU `make', it is safer to compile the package for one
+architecture at a time in the source code directory.  After you have
+installed the package for one architecture, use `make distclean' before
+reconfiguring for another architecture.
+
+   On MacOS X 10.5 and later systems, you can create libraries and
+executables that work on multiple system types--known as "fat" or
+"universal" binaries--by specifying multiple `-arch' options to the
+compiler but only a single `-arch' option to the preprocessor.  Like
+this:
+
+     ./configure CC="gcc -arch i386 -arch x86_64 -arch ppc -arch ppc64" \
+                 CXX="g++ -arch i386 -arch x86_64 -arch ppc -arch ppc64" \
+                 CPP="gcc -E" CXXCPP="g++ -E"
+
+   This is not guaranteed to produce working output in all cases, you
+may have to build one architecture at a time and combine the results
+using the `lipo' tool if you have problems.
+
+Installation Names
+==================
+
+   By default, `make install' installs the package's commands under
+`/usr/local/bin', include files under `/usr/local/include', etc.  You
+can specify an installation prefix other than `/usr/local' by giving
+`configure' the option `--prefix=PREFIX', where PREFIX must be an
+absolute file name.
+
+   You can specify separate installation prefixes for
+architecture-specific files and architecture-independent files.  If you
+pass the option `--exec-prefix=PREFIX' to `configure', the package uses
+PREFIX as the prefix for installing programs and libraries.
+Documentation and other data files still use the regular prefix.
+
+   In addition, if you use an unusual directory layout you can give
+options like `--bindir=DIR' to specify different values for particular
+kinds of files.  Run `configure --help' for a list of the directories
+you can set and what kinds of files go in them.  In general, the
+default for these options is expressed in terms of `${prefix}', so that
+specifying just `--prefix' will affect all of the other directory
+specifications that were not explicitly provided.
+
+   The most portable way to affect installation locations is to pass the
+correct locations to `configure'; however, many packages provide one or
+both of the following shortcuts of passing variable assignments to the
+`make install' command line to change installation locations without
+having to reconfigure or recompile.
+
+   The first method involves providing an override variable for each
+affected directory.  For example, `make install
+prefix=/alternate/directory' will choose an alternate location for all
+directory configuration variables that were expressed in terms of
+`${prefix}'.  Any directories that were specified during `configure',
+but not in terms of `${prefix}', must each be overridden at install
+time for the entire installation to be relocated.  The approach of
+makefile variable overrides for each directory variable is required by
+the GNU Coding Standards, and ideally causes no recompilation.
+However, some platforms have known limitations with the semantics of
+shared libraries that end up requiring recompilation when using this
+method, particularly noticeable in packages that use GNU Libtool.
+
+   The second method involves providing the `DESTDIR' variable.  For
+example, `make install DESTDIR=/alternate/directory' will prepend
+`/alternate/directory' before all installation names.  The approach of
+`DESTDIR' overrides is not required by the GNU Coding Standards, and
+does not work on platforms that have drive letters.  On the other hand,
+it does better at avoiding recompilation issues, and works well even
+when some directory options were not specified in terms of `${prefix}'
+at `configure' time.
+
+Optional Features
+=================
+
+   If the package supports it, you can cause programs to be installed
+with an extra prefix or suffix on their names by giving `configure' the
+option `--program-prefix=PREFIX' or `--program-suffix=SUFFIX'.
+
+   Some packages pay attention to `--enable-FEATURE' options to
+`configure', where FEATURE indicates an optional part of the package.
+They may also pay attention to `--with-PACKAGE' options, where PACKAGE
+is something like `gnu-as' or `x' (for the X Window System).  The
+`README' should mention any `--enable-' and `--with-' options that the
+package recognizes.
+
+   For packages that use the X Window System, `configure' can usually
+find the X include and library files automatically, but if it doesn't,
+you can use the `configure' options `--x-includes=DIR' and
+`--x-libraries=DIR' to specify their locations.
+
+   Some packages offer the ability to configure how verbose the
+execution of `make' will be.  For these packages, running `./configure
+--enable-silent-rules' sets the default to minimal output, which can be
+overridden with `make V=1'; while running `./configure
+--disable-silent-rules' sets the default to verbose, which can be
+overridden with `make V=0'.
+
+Particular systems
+==================
+
+   On HP-UX, the default C compiler is not ANSI C compatible.  If GNU
+CC is not installed, it is recommended to use the following options in
+order to use an ANSI C compiler:
+
+     ./configure CC="cc -Ae -D_XOPEN_SOURCE=500"
+
+and if that doesn't work, install pre-built binaries of GCC for HP-UX.
+
+   HP-UX `make' updates targets which have the same time stamps as
+their prerequisites, which makes it generally unusable when shipped
+generated files such as `configure' are involved.  Use GNU `make'
+instead.
+
+   On OSF/1 a.k.a. Tru64, some versions of the default C compiler cannot
+parse its `<wchar.h>' header file.  The option `-nodtk' can be used as
+a workaround.  If GNU CC is not installed, it is therefore recommended
+to try
+
+     ./configure CC="cc"
+
+and if that doesn't work, try
+
+     ./configure CC="cc -nodtk"
+
+   On Solaris, don't put `/usr/ucb' early in your `PATH'.  This
+directory contains several dysfunctional programs; working variants of
+these programs are available in `/usr/bin'.  So, if you need `/usr/ucb'
+in your `PATH', put it _after_ `/usr/bin'.
+
+   On Haiku, software installed for all users goes in `/boot/common',
+not `/usr/local'.  It is recommended to use the following options:
+
+     ./configure --prefix=/boot/common
+
+Specifying the System Type
+==========================
+
+   There may be some features `configure' cannot figure out
+automatically, but needs to determine by the type of machine the package
+will run on.  Usually, assuming the package is built to be run on the
+_same_ architectures, `configure' can figure that out, but if it prints
+a message saying it cannot guess the machine type, give it the
+`--build=TYPE' option.  TYPE can either be a short name for the system
+type, such as `sun4', or a canonical name which has the form:
+
+     CPU-COMPANY-SYSTEM
+
+where SYSTEM can have one of these forms:
+
+     OS
+     KERNEL-OS
+
+   See the file `config.sub' for the possible values of each field.  If
+`config.sub' isn't included in this package, then this package doesn't
+need to know the machine type.
+
+   If you are _building_ compiler tools for cross-compiling, you should
+use the option `--target=TYPE' to select the type of system they will
+produce code for.
+
+   If you want to _use_ a cross compiler, that generates code for a
+platform different from the build platform, you should specify the
+"host" platform (i.e., that on which the generated programs will
+eventually be run) with `--host=TYPE'.
+
+Sharing Defaults
+================
+
+   If you want to set default values for `configure' scripts to share,
+you can create a site shell script called `config.site' that gives
+default values for variables like `CC', `cache_file', and `prefix'.
+`configure' looks for `PREFIX/share/config.site' if it exists, then
+`PREFIX/etc/config.site' if it exists.  Or, you can set the
+`CONFIG_SITE' environment variable to the location of the site script.
+A warning: not all `configure' scripts look for a site script.
+
+Defining Variables
+==================
+
+   Variables not defined in a site shell script can be set in the
+environment passed to `configure'.  However, some packages may run
+configure again during the build, and the customized values of these
+variables may be lost.  In order to avoid this problem, you should set
+them in the `configure' command line, using `VAR=value'.  For example:
+
+     ./configure CC=/usr/local2/bin/gcc
+
+causes the specified `gcc' to be used as the C compiler (unless it is
+overridden in the site shell script).
+
+Unfortunately, this technique does not work for `CONFIG_SHELL' due to
+an Autoconf bug.  Until the bug is fixed you can use this workaround:
+
+     CONFIG_SHELL=/bin/bash /bin/bash ./configure CONFIG_SHELL=/bin/bash
+
+`configure' Invocation
+======================
+
+   `configure' recognizes the following options to control how it
+operates.
+
+`--help'
+`-h'
+     Print a summary of all of the options to `configure', and exit.
+
+`--help=short'
+`--help=recursive'
+     Print a summary of the options unique to this package's
+     `configure', and exit.  The `short' variant lists options used
+     only in the top level, while the `recursive' variant lists options
+     also present in any nested packages.
+
+`--version'
+`-V'
+     Print the version of Autoconf used to generate the `configure'
+     script, and exit.
+
+`--cache-file=FILE'
+     Enable the cache: use and save the results of the tests in FILE,
+     traditionally `config.cache'.  FILE defaults to `/dev/null' to
+     disable caching.
+
+`--config-cache'
+`-C'
+     Alias for `--cache-file=config.cache'.
+
+`--quiet'
+`--silent'
+`-q'
+     Do not print messages saying which checks are being made.  To
+     suppress all normal output, redirect it to `/dev/null' (any error
+     messages will still be shown).
+
+`--srcdir=DIR'
+     Look for the package's source code in directory DIR.  Usually
+     `configure' can determine that directory automatically.
+
+`--prefix=DIR'
+     Use DIR as the installation prefix.  *note Installation Names::
+     for more details, including other options available for fine-tuning
+     the installation locations.
+
+`--no-create'
+`-n'
+     Run the configure checks, but stop before creating any output
+     files.
+
+`configure' also accepts some other, not widely useful, options.  Run
+`configure --help' for more details.
+
diff --git a/proofs/lfsc_checker/Makefile.am b/proofs/lfsc_checker/Makefile.am
new file mode 100644
index 000000000..ff483f5fb
--- /dev/null
+++ b/proofs/lfsc_checker/Makefile.am
@@ -0,0 +1,30 @@
+AM_CXXFLAGS = -Wall -Wno-deprecated
+
+bin_PROGRAMS = lfsc-checker
+
+lfsc_checker_SOURCES = \
+	main.cpp
+lfsc_checker_LDADD = \
+	@builddir@/liblfsc_checker.la
+
+noinst_LTLIBRARIES = liblfsc_checker.la
+
+liblfsc_checker_la_SOURCES = \
+	check.cpp \
+	check.h \
+	chunking_memory_management.h \
+	code.cpp \
+	code.h \
+	expr.cpp \
+	expr.h \
+	libwriter.cpp \
+	libwriter.h \
+	position.h \
+	print_smt2.cpp \
+	print_smt2.h \
+	scccode.cpp \
+	scccode.h \
+	sccwriter.cpp \
+	sccwriter.h \
+	trie.cpp \
+	trie.h
diff --git a/proofs/lfsc_checker/NEWS b/proofs/lfsc_checker/NEWS
new file mode 100644
index 000000000..1a357ab4c
--- /dev/null
+++ b/proofs/lfsc_checker/NEWS
@@ -0,0 +1,9 @@
+This file contains a summary of important user-visible changes to the
+LFSC proof checker.
+
+Changes since pre-1.0 (unversioned) releases
+============================================
+
+* Incorporated the LFSC checker into the CVC4 project.
+
+-- Morgan Deters <mdeters@cs.nyu.edu>  Thu, 12 Dec 2013 18:16:08 -0500
diff --git a/proofs/lfsc_checker/README b/proofs/lfsc_checker/README
new file mode 100644
index 000000000..5073569bc
--- /dev/null
+++ b/proofs/lfsc_checker/README
@@ -0,0 +1,83 @@
+lfsc: a high-performance LFSC proof checker.
+
+Andy Reynolds and Aaron Stump
+
+----------------------------------------------------------------------
+Command line parameters for LFSC:
+
+lfsc [sig_1 .... sig_n] [opts_1...opts_n]
+
+[sig_1 .... sig_n] are signature files, and options [opts_1...opts_n]
+are any of the following:
+
+--compile-scc : Write out all side conditions contained in signatures
+  specified on the command line to files scccode.h, scccode.cpp (see
+  below for example)
+
+--run-scc : Run proof checking with compiled side condition code (see
+  below).
+
+--compile-scc-debug : Write side condition code to scccode.h,
+  scccode.cpp that contains print statements (for debugging running of
+  side condition code).
+
+
+
+
+Typical usage:
+
+./src/opt/lfsc [sig_1 .... sig_n] [proof] [opts_1...opts_n]
+
+A proof is typically specified at the end of the list of input files
+in file [proof].  This will tell LFSC to type check the proof term in
+the file [proof].  The extension (*.plf) is commonly used for both
+user signature files and proof files.
+
+
+
+
+Side condition code compilation:
+
+LFSC may be used with side condition code compilation.  This will take
+all side conditions ("program" constructs) in the user signature and
+produce equivalent C++ code in the output files scccode.h,
+scccode.cpp.
+
+An example for QF_IDL running with side condition code compilation:
+
+(1) In the src/ directory, run LFSC with the command line parameters:
+
+./opt/lfsc ../sat-tests/sat.plf ../sat-tests/smt.plf \
+           ../sat-tests/cnf_conv.plf ../sat-tests/th_base.plf \
+           ../sat-tests/th_idl.plf --compile-scc
+
+This will produce scccode.h and scccode.cpp in the working directory
+where lfsc was run (here, src/).
+
+(2) Recompile the code base for lfsc.  This will produce a copy of the
+LFSC executable that is capable of calling side conditions directly as
+compiled C++.
+
+(3) To check a proof.plf* with side condition code compilation, run
+LFSC with the command line parameters:
+
+./opt/lfsc ../sat-tests/sat.plf ../sat-tests/smt.plf \
+           ../sat-tests/cnf_conv.plf ../sat-tests/th_base.plf \
+           ../sat-tests/th_idl.plf --run-scc   proof.plf
+
+
+
+*Note that this proof must be compatible with the proof checking
+ signature.  The proof generator is responsible for producing a proof
+ in the proper format that can be checked by the proof signature
+ specified when running LFSC.
+
+For example, in the case of CLSAT in the QF_IDL logic, older proofs
+(proofs produced before Feb 2009) may be incompatible with the newest
+version of the resolution checking signature (sat.plf).  The newest
+version of CLSAT -- which can be checked out from the Iowa repository
+with
+
+svn co https://svn.divms.uiowa.edu/repos/clc/clsat/trunk clsat
+
+should produce proofs compatible with the current version of sat.plf.
diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp
new file mode 100644
index 000000000..8ef114115
--- /dev/null
+++ b/proofs/lfsc_checker/check.cpp
@@ -0,0 +1,1383 @@
+#include "position.h"
+#include "check.h"
+#include "code.h"
+#include "expr.h"
+#include "trie.h"
+#include "sccwriter.h"
+#include "libwriter.h"
+#ifndef _MSC_VER
+#include <libgen.h>
+#endif
+#include <stack>
+#include <string.h>
+#include <time.h>
+#include "scccode.h"
+#include "print_smt2.h"
+
+using namespace std;
+#ifndef _MSC_VER
+using namespace __gnu_cxx;
+#endif
+
+int linenum = 1;
+int colnum = 1;
+const char *filename = 0;
+FILE *curfile = 0;
+
+//#define USE_HASH_MAPS
+
+symmap2 progs;
+std::vector< Expr* > ascHoles;
+
+#ifdef USE_HASH_MAPS
+hash_map<string, Expr *> symbols;
+hash_map<string, Expr *> symbol_types;
+#else
+Trie<pair<Expr *, Expr *> > *symbols = new Trie<pair<Expr *, Expr *> >;
+#endif
+
+hash_map<string, bool > imports;
+std::map<SymExpr*, int > mark_map;
+std::vector< std::pair< std::string, std::pair<Expr *, Expr *> > > local_sym_names;
+
+Expr *not_defeq1 = 0;
+Expr *not_defeq2 = 0;
+
+bool tail_calls = true;
+bool big_check = true;
+
+void report_error(const string &msg) {
+  if (filename) {
+    Position p(filename,linenum,colnum);
+    p.print(cout);
+  }
+  cout << "\n";
+  cout << msg;
+  cout << "\n";
+  if (not_defeq1 && not_defeq2) {
+    cout << "The following terms are not definitionally equal:\n1. ";
+    not_defeq1->print(cout);
+    cout << "\n2. ";
+    not_defeq2->print(cout);
+  }
+  cout.flush();
+  _exit(1);
+}
+
+Expr *call_run_code(Expr *code) {
+  if (dbg_prog) {
+    cout << "[Running ";
+    code->print(cout);
+    cout << "\n";
+  }
+  Expr *computed_result = run_code(code);
+  if (dbg_prog) {
+    cout << "] returning ";
+    if (computed_result)
+      computed_result->print(cout);
+    else
+      cout << "fail";
+    cout << "\n";
+  }
+  return computed_result;
+}
+
+char our_getc_c = 0;
+
+int IDBUF_LEN = 2048;
+char idbuf[2048];
+
+Expr *statType = new CExpr(TYPE, 0);
+Expr *statKind = new CExpr(KIND, 0);
+Expr *statMpz = new CExpr(MPZ,0);
+Expr *statMpq = new CExpr(MPQ,0);
+
+int open_parens = 0;
+
+// only call in check()
+void eat_rparen() {
+  eat_char(')');
+  open_parens--;
+}
+
+void eat_excess(int prev) {
+  while(open_parens > prev) 
+    eat_rparen();
+}
+
+/* There are four cases for check():
+
+1. expected=0, create is false: check() sets computed to be the classifier of
+   the checked term.
+
+2. expected=0, create is true: check() returns 
+   the checked expression and sets computed to be its classifier. 
+
+3. expected is non-null, create is false: check returns NULL.
+
+4. expected is non-null, create is true: check returns the term that
+   was checked.
+
+We consume the reference for expected, to enable tail calls in the
+application case. 
+
+If is_hole is NULL, then the expression parsed may not be a hole.
+Otherwise, it may be, and we will set *is_hole to true if it is
+(but leave *is_hole alone if it is not).
+
+*/
+				  
+bool allow_run = false;
+int app_rec_level = 0;
+
+Expr *check(bool create, Expr *expected, Expr **computed = NULL,
+	    bool *is_hole = 0, bool return_pos = false, bool inAsc = false ) {
+ start_check:
+        //std::cout << "check code ";
+        //if( expected )
+        //  expected->print( std::cout );
+        //std::cout << std::endl;
+  char d = non_ws();
+  switch(d) {
+  case '(': {
+
+    open_parens++;
+
+    char c = non_ws(); 
+    switch (c) {
+    case EOF:
+      report_error("Unexpected end of file.");
+      break;
+    case '!': { // the pi case
+      string id(prefix_id());
+#ifdef DEBUG_SYM_NAMES
+      Expr *sym = new SymSExpr(id,SYMS_EXPR);
+#else
+      Expr *sym = new SymExpr(id);
+      //std::cout << "name " << id << " " << sym << std::endl;
+#endif
+      allow_run = true;
+      int prevo = open_parens;
+      Expr *domain = check(true, statType);
+      eat_excess(prevo);
+      allow_run = false;
+#ifdef USE_HASH_MAPS
+      Expr *prev = symbols[id];
+      Expr *prevtp = symbol_types[id];
+      symbols[id] = sym;
+      symbol_types[id] = domain;
+#else
+      pair<Expr *,Expr *>prev =
+	symbols->insert(id.c_str(),pair<Expr *,Expr *>(sym,domain));
+#endif
+      if (expected)
+	      expected->inc();
+      Expr *range = check(create, expected, computed, NULL, return_pos);
+      eat_excess(prevo);
+      eat_rparen();
+
+#ifdef USE_HASH_MAPS
+      symbols[id] = prev;
+      symbol_types[id] = prevtp;
+#else
+      symbols->insert(id.c_str(),prev);
+#endif
+      if (expected) {
+	int o = expected->followDefs()->getop();
+	expected->dec();
+	if (o != TYPE && o != KIND)
+	  report_error(string("The expected classifier for a pi abstraction")
+		       +string("is neither \"type\" nor \"kind\".\n")
+		       +string("1. the expected classifier: ")
+		       +expected->toString());
+   if (create){ 
+	  CExpr* ret = new CExpr(PI, sym, domain, range);
+      ret->calc_free_in();
+      return ret;
+   }
+	return 0;
+      }
+      else {
+         if (create){ 
+	         CExpr* ret = new CExpr(PI, sym, domain, range);
+            ret->calc_free_in();
+            return ret;
+         }
+	int o = (*computed)->followDefs()->getop();
+	if (o != TYPE && o != KIND)
+	  report_error(string("The classifier for the range of a pi")
+		       +string("abstraction is neither \"type\" nor ")
+		       +string("\"kind\".\n1. the computed classifier: ")
+		       +range->toString());
+	return 0;
+      }
+    }
+    case '%': { // the case for big lambda
+      if (expected || create || !return_pos || !big_check)
+	report_error(string("Big lambda abstractions can only be used")
+		     +string("in the return position of a \"bigcheck\"\n")
+		     +string("command."));
+      string id(prefix_id());
+#ifdef DEBUG_SYM_NAMES
+      SymExpr *sym = new SymSExpr(id, SYMS_EXPR);
+#else
+      SymExpr *sym = new SymExpr(id);
+      //std::cout << "name " << id << " " << sym << std::endl;
+#endif
+
+      int prevo = open_parens;
+      Expr *expected_domain = check(true, statType);
+      eat_excess(prevo);
+
+#ifdef USE_HASH_MAPS
+      Expr *prev = symbols[id];
+      Expr *prevtp = symbol_types[id];
+      symbols[id] = sym;
+      symbol_types[id] = expected_domain;
+#else
+      pair<Expr *, Expr *> prevpr = 
+	      symbols->insert(id.c_str(), pair<Expr *, Expr *>(sym,expected_domain));
+      Expr *prev = prevpr.first;
+      Expr *prevtp = prevpr.second;
+#endif
+      expected_domain->inc(); // because we have stored it in the symbol table
+
+      //will clean up local sym name eventually
+      local_sym_names.push_back( std::pair< std::string, std::pair<Expr *, Expr *> >( id, prevpr ) );
+      if (prev) 
+	      prev->dec();
+      if (prevtp)
+	      prevtp->dec();
+      create = false;
+      expected = NULL;
+      // computed unchanged
+      is_hole = NULL;
+      // return_pos unchanged
+
+      // note we will not store the proper return type in computed.
+
+      goto start_check;
+    }
+
+    case '\\': { // the lambda case
+      if (!expected)
+	report_error(string("We are computing a type for a lambda ")
+		     +string("abstraction, but we can only check\n")
+		     +string("such against a type.  Try inserting an ")
+		     +string("ascription (using ':').\n"));
+      Expr *orig_expected = expected;
+      expected = expected->followDefs();
+      if (expected->getop() != PI)
+	report_error(string("We are type-checking a lambda abstraction, but\n")
+		     +string("the expected type is not a pi abstraction.\n")
+		     +string("1. The expected type: ") + expected->toString());
+      string id(prefix_id());
+#ifdef DEBUG_SYM_NAMES
+      SymExpr *sym = new SymSExpr(id, SYMS_EXPR);
+#else
+      SymExpr *sym = new SymExpr(id);
+      //std::cout << "name " << id << " " << sym << std::endl;
+#endif
+
+      CExpr *pitp = (CExpr *)expected;
+      Expr *expected_domain = pitp->kids[1];
+      Expr *expected_range = pitp->kids[2];
+      SymExpr *pivar = (SymExpr *)pitp->kids[0];
+      if (expected_range->followDefs()->getop() == TYPE)
+	report_error(string("The expected classifier for a lambda abstraction")
+		     +string(" a kind, not a type.\n")
+		     +string("1. The expected classifier: ")
+		     +expected->toString());
+      
+      /* we need to map the pivar to the new sym, because in our
+	 higher-order matching we may have (_ x) to unify with t.
+	 The x must be something from an expected type, since only these
+	 can have holes.  We want to map expected vars x to computed vars y,
+	 so that we can set the hole to be \ y t, where t contains ys but
+         not xs. */
+      
+#ifdef USE_HASH_MAPS
+      Expr *prev = symbols[id];
+      Expr *prevtp = symbol_types[id];
+      symbols[id] = sym;
+      symbol_types[id] = expected_domain;
+#else
+      pair<Expr *, Expr *> prevpr = 
+	      symbols->insert(id.c_str(), pair<Expr *, Expr *>(sym,expected_domain));
+      Expr *prev = prevpr.first;
+      Expr *prevtp = prevpr.second;
+#endif
+      Expr *prev_pivar_val = pivar->val;
+      sym->inc();
+      pivar->val = sym;
+
+      expected_domain->inc(); // because we have stored it in the symbol table
+      expected_range->inc(); // because we will pass it to a recursive call
+
+      if (tail_calls && big_check && return_pos && !create) {
+        //will clean up local sym name eventually
+        local_sym_names.push_back( std::pair< std::string, std::pair<Expr *, Expr *> >( id, prevpr ) );
+	      if (prev_pivar_val)
+	        prev_pivar_val->dec();
+	      if (prev) 
+	        prev->dec();
+	      if (prevtp)
+	        prevtp->dec();
+	      orig_expected->dec();
+	      create = false;
+	      expected = expected_range;
+	      computed = NULL;
+	      is_hole = NULL;
+	      // return_pos unchanged
+	      goto start_check;
+      }
+      else {
+
+	      int prev = open_parens;
+	      Expr *range = check(create, expected_range, NULL, NULL, return_pos);
+	      eat_excess(prev);
+	      eat_rparen();
+
+#ifdef USE_HASH_MAPS
+	      symbols[id] = prev;
+	      symbol_types[id] = prevtp;
+#else
+	      symbols->insert(id.c_str(), prevpr);
+#endif
+	      expected_domain->dec(); // because removed from the symbol table now
+
+	      pivar->val = prev_pivar_val;
+
+	      orig_expected->dec();
+
+	      sym->dec(); // the pivar->val reference
+	      if (create) 
+	        return new CExpr(LAM, sym, range);
+	      sym->dec(); // the symbol table reference, otherwise in the new LAM
+	      return 0;
+      }
+    }
+    case '^': { // the run case
+      if (!allow_run || !create || !expected)
+	      report_error(string("A run expression (operator \"^\") appears in")
+		          +string(" a disallowed position."));
+
+      Expr *code = read_code();
+      //string errstr = (string("The first argument in a run expression must be")
+		    //   +string(" a call to a program.\n1. the argument: ") 
+		    //   +code->toString());
+
+      /* determine expected type of the result term, and make sure
+	 the code term is an allowed one. */
+#if 0
+      Expr *progret;
+      if (code->isArithTerm()) 
+	      progret = statMpz;
+      else {
+	      if (code->getop() != APP)
+	        report_error(errstr);
+
+	      CExpr *call = (CExpr *)code;
+      	
+	      // prog is not known to be a SymExpr yet
+	      CExpr *prog = (CExpr *)call->get_head();
+      	
+	      if (prog->getop() != PROG)
+	        report_error(errstr);
+
+	      progret = prog->kids[0]->get_body();
+      }
+#else
+      Expr *progret = NULL;
+      if (code->isArithTerm()) 
+	      progret = statMpz;
+      else {
+	      if (code->getop() == APP)
+        {
+	        CExpr *call = (CExpr *)code;
+        	
+	        // prog is not known to be a SymExpr yet
+	        CExpr *prog = (CExpr *)call->get_head();
+        	
+	        if (prog->getop() == PROG)
+	          progret = prog->kids[0]->get_body();
+        }
+      }
+#endif
+      /* determine expected type of the result term, and make sure
+	      the code term is an allowed one. */
+      //Expr* progret = check_code( code );
+
+      /* the next term cannot be a hole where run expressions are introduced.
+	      When they are checked in applications, it can be. */
+      int prev = open_parens;
+      if( progret )
+        progret->inc();
+      Expr *trm = check(true, progret);
+      eat_excess(prev);
+      eat_rparen();
+
+      if (expected->getop() != TYPE)
+	      report_error(string("The expected type for a run expression is not ")
+		          +string("\"type\".\n")
+		          +string("1. The expected type: ")+expected->toString());
+      expected->dec();
+      return new CExpr(RUN, code, trm);
+    }
+
+    case ':': { // the ascription case
+      statType->inc();
+      int prev = open_parens;
+      Expr *tp = check(true, statType, NULL, NULL, false, true );
+      eat_excess(prev);
+
+      if (!expected)
+	      tp->inc();
+ 
+      Expr *trm = check(create, tp, NULL, NULL, return_pos);
+      eat_excess(prev);
+      eat_rparen();
+      if (expected) {
+	      if (!expected->defeq(tp))
+	        report_error(string("The expected type does not match the ")
+		            +string("ascribed type in an ascription.\n")
+		            +string("1. The expected type: ")+expected->toString()
+		            +string("\n2. The ascribed type: ")+tp->toString());
+
+	      // no need to dec tp, since it was consumed by the call to check
+	      expected->dec();
+	      if (create)
+	        return trm;
+	      trm->dec();
+	      return 0;
+      }
+      else {
+	      *computed = tp;
+	      if (create)
+	        return trm;
+	      return 0;
+      }
+    }
+    case '@': { // the local definition case
+      string id(prefix_id());
+#ifdef DEBUG_SYM_NAMES
+      SymExpr *sym = new SymSExpr(id, SYMS_EXPR);
+#else
+      SymExpr *sym = new SymExpr(id);
+#endif
+      int prev_open = open_parens;
+      Expr *tp_of_trm;
+      Expr *trm = check(true, NULL, &tp_of_trm);
+      eat_excess(prev_open);
+
+      sym->val = trm;
+
+#ifdef USE_HASH_MAPS
+      Expr *prev = symbols[id];
+      Expr *prevtp = symbol_types[id];
+      symbols[id] = sym;
+      symbol_types[id] = tp_of_trm;
+#else
+      pair<Expr *, Expr *> prevpr = 
+	symbols->insert(id.c_str(), pair<Expr *, Expr *>(sym,tp_of_trm));
+      Expr *prev = prevpr.first;
+      Expr *prevtp = prevpr.second;
+#endif
+
+      if (tail_calls && big_check && return_pos && !create) {
+	      if (prev) 
+	        prev->dec();
+	      if (prevtp)
+	        prevtp->dec();
+	      // all parameters to check() unchanged here
+	      goto start_check;
+      }
+      else {
+	      int prev_open = open_parens;
+	      Expr *body = check(create, expected, computed, is_hole, return_pos);
+	      eat_excess(prev_open);
+	      eat_rparen();
+
+#ifdef USE_HASH_MAPS
+	      symbols[id] = prev;
+	      symbol_types[id] = prevtp;
+#else
+	      symbols->insert(id.c_str(), prevpr);
+#endif
+	      tp_of_trm->dec(); // because removed from the symbol table now
+
+	      sym->dec(); 
+	      return body;
+      }
+    }
+    case '~': {
+      int prev = open_parens;
+      Expr *e = check(create, expected, computed, is_hole, return_pos);
+      eat_excess(prev);
+      eat_rparen();
+
+      // this has been only very lightly tested -- ads.
+
+      if (expected) {
+	      if (expected != statMpz && expected != statMpq)
+	        report_error("Negative sign where an numeric expression is expected.");
+      }
+      else {
+	      if ((*computed) != statMpz && (*computed) != statMpq)
+	        report_error("Negative sign where an numeric expression is expected.");
+      }
+
+      if (create) {
+	      if (e->getclass() == INT_EXPR)
+        {
+	        IntExpr *ee = (IntExpr *)e;
+	        mpz_neg(ee->n, ee->n);
+	        return ee;
+        }
+        else if( e->getclass() == RAT_EXPR )
+        {
+	        RatExpr *ee = (RatExpr *)e;
+	        mpq_neg(ee->n, ee->n);
+	        return ee;
+        }
+        else
+        {
+          report_error("Negative sign with expr that is not an int. literal.");
+        }
+      }
+      else 
+	      return 0;
+    }
+    default: { // the application case
+      our_ungetc(c);
+      Expr *head_computed;
+      int prev = open_parens;
+      Expr *headtrm = check(create,0,&head_computed);
+      eat_excess(prev);
+
+      CExpr *headtp = (CExpr *)head_computed->followDefs();
+      headtp->inc();
+      head_computed->dec();
+      if ( headtp->cloned()) {
+	      // we must clone
+	      Expr *orig_headtp = headtp;
+	      headtp = (CExpr *)headtp->clone();
+	      orig_headtp->dec(); 
+      }
+      else
+	      headtp->setcloned();
+#ifdef DEBUG_APPS
+      char tmp[100];
+      sprintf(tmp,"(%d) ", app_rec_level++);
+      cout << tmp << "{ headtp = ";
+      headtp->debug();
+#endif
+      char c;
+      vector<HoleExpr *> holes;
+      vector<bool> free_holes;
+      while ((c = non_ws()) != ')') {
+	our_ungetc(c);
+	if (headtp->getop() != PI)
+	  report_error(string("The type of an applied term is not ") 
+		       + string("a pi-type.\n")
+		       + string("\n1. the type of the term: ")
+		       + headtp->toString()
+		       + (headtrm ? (string("\n2. the term: ") 
+				     + headtrm->toString())
+			  : string("")));
+	SymExpr *headtp_var = (SymExpr *)headtp->kids[0];
+	Expr *headtp_domain = headtp->kids[1];
+	Expr *headtp_range = headtp->kids[2];
+	if (headtp_domain->getop() == RUN) {
+	  CExpr *run = (CExpr *)headtp_domain;
+	  Expr *code = run->kids[0];
+	  Expr *expected_result = run->kids[1];
+	  Expr *computed_result = call_run_code(code);
+	  if (!computed_result)
+	    report_error(string("A side condition failed.\n")
+			 +string("1. the side condition: ")
+			 +code->toString());
+	  if (!expected_result->defeq(computed_result))
+	    report_error(string("The expected result of a side condition ")
+			 +string("does not match the computed result.\n")
+			 +string("1. expected result: ")
+			 +expected_result->toString()
+			 +string("\n2. computed result: ")
+			   +computed_result->toString());
+	  computed_result->dec();
+	}
+	else {
+	  // check an argument
+      bool var_in_range = headtp->get_free_in();//headtp_range->free_in(headtp_var);
+	  bool arg_is_hole = false;
+	  bool consumed_arg = false;
+
+	  bool create_arg = (create || var_in_range);
+
+	  headtp_domain->inc();
+
+	  if (tail_calls && !create_arg && headtp_range->getop() != PI) {
+	    // we can make a tail call to check() here.
+
+	    if (expected) {
+	      if (!expected->defeq(headtp_range))
+		      report_error(string("The type expected for an application ")
+			          + string("does not match the computed type.\n")
+			          + string("1. The expected type: ")
+			          + expected->toString()
+			          + string("\n2. The computed type: ")
+			          + headtp_range->toString()
+			          + (headtrm ? (string("\n3. the application: ") 
+					        + headtrm->toString())
+				    : string("")));
+	      expected->dec();
+	    }
+	    else {
+	      headtp_range->inc();
+	      *computed = headtp_range;
+	    }
+
+	    headtp->dec();
+
+	    // same as below
+	    for (int i = 0, iend = holes.size(); i < iend; i++) {
+	      if (!holes[i]->val)
+		/* if the hole is free in the domain, we will be filling
+		   it in when we make our tail call, since the domain
+		   is the expected type for the argument */
+		if (!headtp_domain->free_in(holes[i]))
+		  report_error(string("A hole was left unfilled after ")
+			       +string("checking an application.\n"));
+	      holes[i]->dec();
+	    }
+
+	    create = false;
+	    expected = headtp_domain;
+	    computed = NULL;
+	    is_hole = NULL; // the argument cannot be a hole
+	    // return_pos is unchanged
+
+#ifdef DEBUG_APPS
+	    cout << "Making tail call.\n";
+#endif
+
+	    goto start_check;
+	  }
+
+	    Expr *arg = check(create_arg, headtp_domain, NULL, &arg_is_hole);
+	    eat_excess(prev);
+	    if (create) {
+#ifndef USE_FLAT_APP
+	      headtrm = new CExpr(APP, headtrm, arg);
+#else
+        headtrm = Expr::make_app( headtrm, arg );
+#endif
+	      consumed_arg = true;
+	    }
+	    if (var_in_range) {
+	      Expr *tmp = arg->followDefs();
+	      tmp->inc();
+	      headtp_var->val = tmp;
+	    }
+	    if (arg_is_hole) {
+	      if (consumed_arg)
+	        arg->inc();
+	      else
+	        consumed_arg = true; // not used currently
+#ifdef DEBUG_HOLES
+	        cout << "An argument is a hole: ";
+	        arg->debug();
+#endif
+	          holes.push_back((HoleExpr *)arg);
+	        }
+	      }
+	      headtp_range->inc();
+	      headtp->dec();
+	      headtp = (CExpr *)headtp_range;
+      }
+      open_parens--;
+
+      // check for remaining RUN in the head's type after all the arguments
+
+      if (headtp->getop() == PI && headtp->kids[1]->getop() == RUN) {
+	      CExpr *run = (CExpr *)headtp->kids[1];
+	      Expr *code = run->kids[0]->followDefs();
+	      Expr *expected_result = run->kids[1];
+	      Expr *computed_result = call_run_code(code);
+	      if (!computed_result)
+	        report_error(string("A side condition failed.\n")
+		            +string("1. the side condition: ")+code->toString());
+	      if (!expected_result->defeq(computed_result))
+	        report_error(string("The expected result of a side condition ")
+		            +string("does not match the computed result.\n")
+		            +string("1. expected result: ")
+		            +expected_result->toString()
+		            +string("\n2. computed result: ")
+		            +computed_result->toString());
+	      Expr *tmp = headtp->kids[2];
+	      tmp->inc();
+	      headtp->dec();
+	      headtp = (CExpr *)tmp;
+	      computed_result->dec();
+      }
+
+#ifdef DEBUG_APPS
+      for (int i = 0, iend = holes.size(); i < iend; i++) {
+	      cout << tmp << "hole ";
+	      holes[i]->debug();
+      }
+      cout << "}";
+      app_rec_level--;
+#endif
+
+      Expr *ret = 0;
+      if (expected) {
+        if (!expected->defeq(headtp)){
+	        report_error(string("The type expected for an application does not")
+		            + string(" match the computed type.(2) \n")
+		            + string("1. The expected type: ")
+		            + expected->toString()
+		            + string("\n2. The computed type: ")
+		            + headtp->toString()
+		            + (headtrm ? (string("\n3. the application: ") 
+				          + headtrm->toString())
+			        : string("")));
+
+        }
+	      expected->dec();
+	      headtp->dec();
+	      if (create)
+	        ret = headtrm;
+      }
+      else {
+	      *computed = headtp;
+	      if (create)
+	        ret = headtrm;
+      }
+
+      /* do this check here to give the defeq() call above a 
+	 chance to fill in some holes */
+      for (int i = 0, iend = holes.size(); i < iend; i++) {
+        if (!holes[i]->val){
+          if( inAsc ){
+#ifdef DEBUG_HOLES
+            std::cout << "Ascription Hole: ";
+            holes[i]->print( std::cout );
+            std::cout << std::endl;
+#endif
+            ascHoles.push_back( holes[i] );
+          }else{
+	          report_error(string("A hole was left unfilled after checking")
+		              +string(" an application (2).\n"));
+          }
+        }
+	      holes[i]->dec();
+      }
+
+      return ret;
+
+    } // end application case
+  }
+  }
+  case EOF:
+    report_error("Unexpected end of file.");
+    break;
+
+  case '_': 
+    if (!is_hole)
+      report_error("A hole is being used in a disallowed position.");
+    *is_hole = true;
+    if (expected)
+      expected->dec();
+    return new HoleExpr();
+  case '0':
+  case '1':
+  case '2':
+  case '3':
+  case '4':
+  case '5':
+  case '6':
+  case '7':
+  case '8':
+  case '9': {
+    our_ungetc(d);
+    string v;
+    char c;
+    while (isdigit(c = our_getc())) 
+      v.push_back(c);
+    bool parseMpq = false;
+    string v2;
+    if( c=='/' )
+    {
+      parseMpq = true;
+      v.push_back( c );
+      while(isdigit(c = our_getc())) 
+        v.push_back(c);
+    }
+    our_ungetc(c);
+
+
+    Expr *i = 0;
+    if (create) {
+      if( parseMpq )
+      {
+        mpq_t num;
+        mpq_init(num);
+        if (mpq_set_str(num,v.c_str(),10) == -1)
+	        report_error("Error reading a numeral.");
+        i = new RatExpr(num);
+      }
+      else
+      {
+        mpz_t num;
+        if (mpz_init_set_str(num,v.c_str(),10) == -1)
+	        report_error("Error reading a numeral.");
+        i = new IntExpr(num);
+      }
+    }
+
+    if (expected) {
+      if( ( !parseMpq && expected != statMpz ) || ( parseMpq && expected != statMpq ) )
+	      report_error(string("We parsed a numeric literal, but were ")
+		          +string("expecting a term of a different type.\n")
+		          +string("1. the expected type: ")+expected->toString());
+      expected->dec();
+      if (create)
+	      return i;
+      return 0;
+    }
+    else {
+      if( parseMpq )
+      {
+        statMpq->inc();
+        *computed = statMpq;
+        if (create)
+	        return i;
+        return statMpq;
+      }
+      else
+      {
+        statMpz->inc();
+        *computed = statMpz;
+        if (create)
+	        return i;
+        return statMpz;
+      }
+    }
+  }
+  default: {
+    our_ungetc(d);
+    string id(prefix_id());
+#ifdef USE_HASH_MAPS
+    Expr *ret = symbols[id];
+    Expr *rettp = symbol_types[id];
+#else
+    pair<Expr *, Expr *> p = symbols->get(id.c_str());
+    Expr *ret = p.first;
+    Expr *rettp = p.second;
+#endif
+    if (!ret)
+      report_error(string("Undeclared identifier: ")+id);
+    if (expected) {
+      if (!expected->defeq(rettp))
+	report_error(string("The type expected for a symbol does not")
+		     + string(" match the symbol's type.\n")
+		     + string("1. The symbol: ")
+		     + id
+		     + string("\n2. The expected type: ")
+		     + expected->toString()
+		     + string("\n3. The symbol's type: ")
+		     + rettp->toString());
+      expected->dec();
+      if (create) {
+	      ret->inc();
+	      return ret;
+      }
+      return 0;
+    }
+    else {
+      if( computed ){
+        *computed = rettp;
+        (*computed)->inc();
+      }
+      if (create) {
+	      ret->inc();
+	      return ret;
+      }
+      return 0;
+    }
+  }
+  }
+
+  report_error("Unexpected operator at the start of a term.");
+  return 0;
+}
+
+#ifdef USE_HASH_MAPS
+void discard_old_symbol(const string &id) {
+  Expr *tmp = symbols[id];
+  if (tmp) 
+    tmp->dec();
+  tmp = symbol_types[id];
+  if (tmp)
+    tmp->dec();
+}
+#endif
+
+int check_time;
+
+void check_file(const char *_filename, args a, sccwriter* scw, libwriter* lw) {
+  int prev_linenum = linenum;
+  int prev_colnum = colnum;
+  const char *prev_filename = filename;
+  FILE * prev_curfile = curfile;
+
+  // from code.h
+  dbg_prog = a.show_runs;
+  run_scc = a.run_scc;
+  tail_calls = !a.no_tail_calls;
+
+
+  char *f;
+  if (strcmp(_filename,"stdin") == 0) {
+    curfile = stdin; 
+    f = strdup(_filename);
+  }
+  else {
+    if (prev_curfile) {
+      f = strdup(prev_filename);
+#ifdef _MSC_VER
+	    std::string str( f );
+	    for( int n=str.length(); n>=0; n-- ){
+		    if( str[n]=='\\' || str[n]=='/' ){
+          str = str.erase( n, str.length()-n );
+          break;
+		    }
+	    }
+	    char *tmp = (char*)str.c_str();
+#else
+      char *tmp = dirname(f);
+#endif
+      delete f;
+      f = new char[strlen(tmp) + 10 + strlen(_filename)];
+      strcpy(f,tmp);
+      strcat(f,"/");
+      strcat(f,_filename);
+    }
+    else
+      f = strdup(_filename);
+    curfile = fopen(f,"r");
+    if (!curfile) 
+      report_error(string("Could not open file \"")
+		   + string(f)
+		   + string("\" for reading.\n"));
+  }
+
+  linenum = 1;
+  colnum = 1;
+  filename = f;
+
+  char c;
+  while ((c = non_ws()) && c!=EOF ) {
+    if( c == '(' )
+    {
+      char d;
+      switch ((d = non_ws())) {
+      case 'd':
+        char b;
+        if ((b = our_getc()) != 'e') 
+	        report_error(string("Unexpected start of command."));
+
+        switch ((b = our_getc())) {
+          case 'f': {// expecting "define"
+	
+	          if (our_getc() != 'i' || our_getc() != 'n' || our_getc() != 'e')
+	            report_error(string("Unexpected start of command."));
+	
+	          string id(prefix_id());
+	          Expr *ttp;
+	          int prevo = open_parens;
+	          Expr *t = check(true, 0, &ttp, NULL, true);
+	          eat_excess(prevo);
+
+	          int o = ttp->followDefs()->getop();
+	          if (o == KIND)
+	            report_error(string("Kind-level definitions are not supported.\n"));
+	          SymSExpr *s = new SymSExpr(id);
+	          s->val = t;
+#ifdef USE_HASH_MAPS
+	          discard_old_symbol(id);
+	          symbols[id] = s;
+	          symbol_types[id] = ttp;
+#else
+	          pair<Expr *, Expr *> prev = 
+	            symbols->insert(id.c_str(), pair<Expr *, Expr *>(s,ttp));
+	          if (prev.first)
+	            prev.first->dec();
+	          if (prev.second)
+	            prev.second->dec();
+#endif
+	        break;
+          }
+          case 'c': {// expecting "declare"
+	          if (our_getc() != 'l' || our_getc() != 'a' || our_getc() != 'r' 
+	              || our_getc() != 'e')
+	            report_error(string("Unexpected start of command."));
+
+	          string id(prefix_id());
+	          Expr *ttp;
+	          int prevo = open_parens;
+	          Expr *t = check(true, 0, &ttp, NULL, true);
+	          eat_excess(prevo);
+
+	          ttp = ttp->followDefs();
+	          if (ttp->getop() != TYPE && ttp->getop() != KIND)
+	            report_error(string("The expression declared for \"")
+		                +id+string("\" is neither\na type nor a kind.\n")
+		                +string("1. The expression: ")
+		                +t->toString()
+		                +string("\n2. Its classifier (should be \"type\" ")
+		                +string("or \"kind\"): ")+ttp->toString());
+	          ttp->dec();
+	          SymSExpr *s = new SymSExpr(id);
+#ifdef USE_HASH_MAPS
+	          discard_old_symbol(id);
+	          symbols[id] = s;
+	          symbol_types[id] = t;
+#else
+	          pair<Expr *, Expr *> prev = 
+	            symbols->insert(id.c_str(), pair<Expr *, Expr *>(s,t));
+            if( lw )
+              lw->add_symbol( s, t );
+	          if (prev.first)
+	            prev.first->dec();
+	          if (prev.second)
+	            prev.second->dec();
+#endif
+	          break;
+            }
+            default: 
+	            report_error(string("Unexpected start of command."));
+            } // switch((b = our_getc())) following "de"
+         break;
+    case 'c': {
+      if (our_getc() != 'h' || our_getc() != 'e' || our_getc() != 'c' || our_getc() != 'k')
+	      report_error(string("Unexpected start of command."));
+      if( run_scc ){
+        init_compiled_scc();
+      }
+      Expr *computed;
+      big_check = true;
+      int prev = open_parens;
+      (void)check(false, 0, &computed, NULL, true);
+
+      //print out ascription holes
+      for( int a=0; a<(int)ascHoles.size(); a++ ){
+#ifdef PRINT_SMT2
+        print_smt2( ascHoles[a], std::cout );
+#else
+        ascHoles[a]->print( std::cout );
+#endif
+        std::cout << std::endl;
+      }
+      if( !ascHoles.empty() )
+        std::cout << std::endl;
+      ascHoles.clear();
+
+      //clean up local symbols
+      for( int a=0; a<(int)local_sym_names.size(); a++ ){
+#ifdef USE_HASH_MAPS
+#else
+        symbols->insert( local_sym_names[a].first.c_str(), local_sym_names[a].second );
+#endif
+      }
+      local_sym_names.clear();
+      mark_map.clear();
+
+      eat_excess(prev);
+
+      computed->dec();
+      //cleanup();
+      //exit(0);
+      break;
+    }
+    case 'o': { // opaque case
+      if (our_getc() != 'p' || our_getc() != 'a' || our_getc() != 'q'
+	        || our_getc() != 'u' || our_getc() != 'e')
+	      report_error(string("Unexpected start of command."));
+	
+      string id(prefix_id());
+      Expr *ttp;
+      int prevo = open_parens;
+      (void)check(false, 0, &ttp, NULL, true);
+      eat_excess(prevo);
+
+      int o = ttp->followDefs()->getop();
+      if (o == KIND)
+	      report_error(string("Kind-level definitions are not supported.\n"));
+      SymSExpr *s = new SymSExpr(id);
+#ifdef USE_HASH_MAPS
+	    discard_old_symbol(id);
+	    symbols[id] = s;
+	    symbol_types[id] = ttp;
+#else
+	    pair<Expr *, Expr *> prev = 
+	      symbols->insert(id.c_str(), pair<Expr *, Expr *>(s,ttp));
+	    if (prev.first)
+	      prev.first->dec();
+	    if (prev.second)
+	      prev.second->dec();
+#endif
+        break;
+      }
+      case 'r': { // run case
+        if (our_getc() != 'u' || our_getc() != 'n')
+	        report_error(string("Unexpected start of command."));
+        Expr *code = read_code();
+        check_code(code);
+        cout << "[Running-sc ";
+        code->print(cout);
+        Expr *tmp = run_code(code);
+        cout << "] = \n";
+        if (tmp) {
+	        tmp->print(cout);
+	        tmp->dec();
+        }
+        else
+	        cout << "fail";
+        cout << "\n";
+        code->dec();
+        break;
+      }
+      case 'p': { // program case
+        if (our_getc() != 'r' || our_getc() != 'o' || our_getc() != 'g' 
+	         || our_getc() != 'r' || our_getc() != 'a' || our_getc() != 'm')
+	        report_error(string("Unexpected start of command."));
+
+        string progstr(prefix_id());
+        SymSExpr *prog = new SymSExpr(progstr);
+        if (progs.find(progstr) != progs.end())
+	        report_error(string("Redeclaring program ")+progstr+string("."));
+        progs[progstr] = prog;
+        eat_char('(');
+        char d;
+        vector<Expr *> vars;
+        vector<Expr *> tps;
+        Expr *tmp;
+        while ((d = non_ws()) != ')') {
+	        our_ungetc(d);
+	        eat_char('(');
+	        string varstr = prefix_id();
+#ifdef USE_HASH_MAPS
+	        if (symbols.find(varstr) != symbols.end())
+#else
+          if (symbols->get(varstr.c_str()).first != NULL)
+#endif
+	          report_error(string("A program variable is already declared")
+		              +string(" (as a constant).\n1. The variable: ")
+		              +varstr);
+	        Expr *var = new SymSExpr(varstr);
+	        vars.push_back(var);
+	        statType->inc();
+	        int prev = open_parens;
+	        Expr *tp = check(true, NULL, &tmp, 0, true);
+          if( tp->getclass()==SYMS_EXPR ){
+#ifdef USE_HASH_MAPS
+            Expr *tptp = symbol_types[((SymSExpr*)tp)->s];
+#else
+            pair<Expr *, Expr *> p = symbols->get(((SymSExpr*)tp)->s.c_str());
+            Expr *tptp = p.second;
+#endif
+            if( !tptp->isType( statType ) ){
+              report_error(string("Bad argument for side condition"));
+            }
+          }else{
+            if (!tp->isDatatype()){
+	            report_error(string("Type for a program variable is not a ")
+		                +string("datatype.\n1. the type: ")+tp->toString());
+            }
+          }
+	        eat_excess(prev);
+
+	        tps.push_back(tp);
+	        eat_char(')');
+
+#ifdef USE_HASH_MAPS
+	        symbols[varstr] = var;
+	        symbol_types[varstr] = tp;
+#else
+	        symbols->insert(varstr.c_str(), pair<Expr *, Expr *>(var,tp));
+#endif
+        }
+      
+        if (!vars.size())
+	        report_error("A program lacks input variables.");
+   
+        statType->inc();
+        int prev = open_parens;
+        Expr *progtp = check(true,statType,&tmp,0, true);
+        eat_excess(prev);
+
+        if (!progtp->isDatatype())
+	        report_error(string("Return type for a program is not a")
+		            +string(" datatype.\n1. the type: ")+progtp->toString());
+        
+        Expr *progcode = read_code();
+
+        for (int i = vars.size() - 1, iend = 0; i >= iend; i--) {
+	        vars[i]->inc(); // used below for the program code (progcode)
+	        progtp = new CExpr(PI, vars[i], tps[i], progtp);
+          progtp->calc_free_in();
+        }
+
+        // just put the type here for type checking.  Make sure progtp is kid 0.
+        prog->val = new CExpr(PROG, progtp); 
+        
+        check_code(progcode);
+     
+        progcode = new CExpr(PROG, progtp, new CExpr(PROGVARS, vars), progcode);
+        //if compiling side condition code, give this code to the side condition code writer
+        if( a.compile_scc ){
+          if( scw ){
+            scw->add_scc( progstr, (CExpr*)progcode );
+          }
+        }
+	
+	// remove the variables from the symbol table.
+        for (int i = 0, iend = vars.size(); i < iend; i++) {
+	        string &s = ((SymSExpr *)vars[i])->s;
+
+#ifdef USE_HASH_MAPS
+	        symbols[s] = NULL;
+	        symbol_types[s] = NULL;
+#else
+	        symbols->insert(s.c_str(), pair<Expr*,Expr*>(NULL,NULL));
+#endif
+        }
+
+        progtp->inc();
+        prog->val->dec();
+
+        prog->val = progcode;
+
+        break;
+      }
+
+      default: 
+	      report_error(string("Unexpected start of command."));
+      } // switch((d = non_ws())
+        
+      eat_char(')');
+    } // while
+    else
+    {
+      if( c != ')' )
+      {
+        char c2[2];
+        c2[1] = 0;
+        c2[0] = c;
+        string syn = string("Bad syntax (mismatched parentheses?): ");
+        syn.append(string(c2));
+        report_error(syn);
+      }
+    }
+  }
+  free(f);
+  if (curfile != stdin)
+    fclose(curfile);
+  linenum = prev_linenum;
+  colnum = prev_colnum;
+  filename = prev_filename;
+  curfile = prev_curfile;
+
+}
+
+class Deref : public Trie<pair<Expr *, Expr *> >::Cleaner {
+public:
+  ~Deref() {}
+  void clean(pair<Expr *, Expr *> p) {
+    Expr *tmp = p.first;
+    if (tmp) {
+#ifdef DEBUG
+      cout << "Cleaning up ";
+      tmp->debug();
+#endif
+      tmp->dec();
+    }
+    tmp = p.second;
+    if (tmp) {
+#ifdef DEBUG
+      cout << " : ";
+      tmp->debug();
+#endif
+      tmp->dec();
+    }
+#ifdef DEBUG
+      cout << "\n";
+#endif
+  }
+};
+
+template <>
+Trie<pair<Expr *, Expr *> >::Cleaner *
+Trie<pair<Expr *, Expr *> >::cleaner = new Deref;
+
+void cleanup() {
+  symmap::iterator i, iend;
+#ifdef USE_HASH_MAPS
+  Expr *tmp;
+  for (i = symbols.begin(), iend = symbols.end(); i != iend; i++) {
+    tmp = i->second;
+    if (tmp) {
+#ifdef DEBUG
+      cout << "Cleaning up " << i->first << " : ";
+      tmp->debug();
+#endif
+      tmp->dec();
+    }
+  }
+  for (i = symbol_types.begin(), iend = symbol_types.end(); i != iend; i++) {
+    tmp = i->second;
+    if (tmp) {
+#ifdef DEBUG
+      cout << "Cleaning up " << i->first << " : ";
+      tmp->debug();
+#endif
+      tmp->dec();
+    }
+  }
+#else
+  delete symbols;
+#endif
+
+  // clean up programs 
+
+  symmap2::iterator j, jend;
+  for (j = progs.begin(), jend = progs.end(); j != jend; j++) {
+    SymExpr *p = j->second;
+    if (p) {
+      Expr *progcode = p->val;
+      p->val = NULL;
+      progcode->dec();
+      p->dec();
+    }
+  }
+}
+
+void init() {
+#ifdef USE_HASH_MAPS
+  string tp("type");
+  symbols[tp] = statType;
+  symbol_types[tp] = statKind;
+  string mpz("mpz");
+  symbols[mpz] = statMpz;
+  symbol_types[mpz] = statType;
+  statType->inc();
+  sym
+#else
+  symbols->insert("type", pair<Expr *, Expr *>(statType, statKind));
+  statType->inc();
+  symbols->insert("mpz", pair<Expr *, Expr *>(statMpz, statType));
+  symbols->insert("mpq", pair<Expr *, Expr *>(statMpq, statType)); 
+#endif
+}
diff --git a/proofs/lfsc_checker/check.h b/proofs/lfsc_checker/check.h
new file mode 100644
index 000000000..a70599b0f
--- /dev/null
+++ b/proofs/lfsc_checker/check.h
@@ -0,0 +1,167 @@
+#ifndef SC2_CHECK_H
+#define SC2_CHECK_H
+
+#include "expr.h"
+#include "trie.h"
+
+#ifdef _MSC_VER
+#include <hash_map>
+#include <stdio.h>
+#else
+#include <ext/hash_map>
+#endif
+
+#include <stack>
+#include <string>
+#include <map>
+
+// see the help message in main.cpp for explanation
+typedef struct args {
+  std::vector<std::string> files;
+  bool show_runs; 
+  bool no_tail_calls; 
+  bool compile_scc;
+  bool compile_scc_debug;
+  bool run_scc;
+  bool use_nested_app;
+  bool compile_lib;
+} args;
+
+extern int check_time;
+
+class sccwriter;
+class libwriter;
+
+void init();
+
+void check_file(const char *_filename, args a, sccwriter* scw = NULL, libwriter* lw = NULL);
+
+void cleanup();
+
+extern char our_getc_c;
+
+void report_error(const std::string &);
+
+extern int linenum;
+extern int colnum;
+extern const char *filename;
+extern FILE *curfile;
+
+inline void our_ungetc(char c) {
+  if (our_getc_c != 0)
+    report_error("Internal error: our_ungetc buffer full");
+  our_getc_c = c;
+  if (c == '\n') {
+    linenum--;
+    colnum=-1;
+  }
+  else
+    colnum--;
+}
+
+inline char our_getc() {
+  char c;
+  if (our_getc_c > 0) {
+    c = our_getc_c;
+    our_getc_c = 0;
+  }
+  else{
+#ifndef __linux__
+	c = fgetc(curfile);
+#else
+    c = fgetc_unlocked(curfile);
+#endif
+  }
+  switch(c) {
+  case '\n':
+    linenum++;
+#ifdef DEBUG_LINES
+    std::cout << "line " << linenum << "." << std::endl;
+#endif
+    colnum = 1;
+    break;
+  case EOF:
+    break;
+  default:
+    colnum++;
+  }
+
+  return c;
+}
+
+// return the next character that is not whitespace
+inline char non_ws() {
+  char c;
+  while(isspace(c = our_getc()));
+  if (c == ';') {
+    // comment to end of line
+    while((c = our_getc()) != '\n' && c != EOF);
+    return non_ws();
+  }
+  return c;
+}
+  
+inline void eat_char(char expected) {
+  if (non_ws() != expected) {
+    char tmp[80];
+    sprintf(tmp,"Expecting a \'%c\'",expected);
+    report_error(tmp);
+  }
+}
+
+extern int IDBUF_LEN;
+extern char idbuf[];
+
+inline const char *prefix_id() {
+  int i = 0;
+  char c = idbuf[i++] = non_ws();
+  while (!isspace(c) && c != '(' && c != ')' && c != EOF) {
+    if (i == IDBUF_LEN)
+      report_error("Identifier is too long");
+    
+    idbuf[i++] = c = our_getc();
+  }
+  our_ungetc(c);
+  idbuf[i-1] = 0;
+  return idbuf;
+}
+
+#ifdef _MSC_VER
+typedef std::hash_map<std::string, Expr *> symmap;
+typedef std::hash_map<std::string, SymExpr *> symmap2;
+#else
+typedef __gnu_cxx::hash_map<std::string, Expr *> symmap;
+typedef __gnu_cxx::hash_map<std::string, SymExpr *> symmap2;
+#endif
+extern symmap2 progs;
+extern std::vector< Expr* > ascHoles;
+
+#ifdef USE_HASH_MAPS
+extern symmap symbols;
+extern symmap symbol_types;
+#else
+extern Trie<std::pair<Expr *, Expr *> > *symbols;
+#endif
+
+extern std::map<SymExpr*, int > mark_map;
+
+extern std::vector< std::pair< std::string, std::pair<Expr *, Expr *> > > local_sym_names;
+
+#ifndef _MSC_VER
+namespace __gnu_cxx
+{
+  template<> struct hash< std::string >
+  {
+    size_t operator()( const std::string& x ) const
+    {
+      return hash< const char* >()( x.c_str() );
+    }
+  };
+}
+#endif
+
+extern Expr *statMpz;
+extern Expr *statMpq;
+extern Expr *statType;
+
+#endif
diff --git a/proofs/lfsc_checker/chunking_memory_management.h b/proofs/lfsc_checker/chunking_memory_management.h
new file mode 100644
index 000000000..bdf938d32
--- /dev/null
+++ b/proofs/lfsc_checker/chunking_memory_management.h
@@ -0,0 +1,157 @@
+///////////////////////////////////////////////////////////////////////////////
+//                                                                           //
+//  Copyright (C) 2002 by the Board of Trustees of Leland Stanford           //
+//  Junior University.  See LICENSE for details.                             //
+//                                                                           //
+///////////////////////////////////////////////////////////////////////////////
+/* chunking_memory_management.h 
+   Aaron Stump, 6/11/99
+
+   This file contains macros that allow you easily to add chunking
+   memory management for classes.
+
+   RCS Version: $Id: chunking_memory_management.h,v 1.1 2004/11/12 16:26:19 stump Exp $
+
+*/
+#ifndef _chunking_memory_management_h_
+#define _chunking_memory_management_h_
+
+#include <assert.h>
+
+/************************************************************************
+ * MACRO: ADD_CHUNKING_MEMORY_MANAGEMENT_H()
+ * Aaron Stump, 6/11/99
+ *
+ * ABSTRACT: This macro should be called exactly once inside the body
+ * of the declaration of the class THE_CLASS to add chunking memory
+ * management for the class.  That class should not itself declare the
+ * operators new and delete.  The macro
+ * C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_CC should be called with
+ * the same value for THE_CLASS in a .cc file for that class.
+ *
+ * NOTE that the access specifier will be public after calling this 
+ * macro.
+ *
+ * THE_FIELD is a field of the class to use for the next pointer in the
+ * free list data structure.  It can be of any type, but must have enough
+ * space to hold a pointer.
+ ************************************************************************/
+#define C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_H(THE_CLASS,THE_FIELD)	\
+private:\
+  static unsigned C_MACROS__CHUNK_SIZE;\
+  static unsigned C_MACROS__BLOCK_SIZE;\
+  static void *C_MACROS__freelist;\
+  static bool C_MACROS__initialized;\
+  static char *C_MACROS__next_free_block;\
+  static char *C_MACROS__end_of_current_chunk;\
+  \
+  static void C_MACROS__allocate_new_chunk();\
+\
+public:\
+  static void C_MACROS__init_chunks() {\
+    if (!C_MACROS__initialized) {\
+      C_MACROS__allocate_new_chunk();\
+      C_MACROS__initialized = true;\
+    }\
+  }\
+\
+  static void *operator new(size_t size, void *h = NULL);\
+  static void operator delete(void *ptr)\
+
+
+/************************************************************************
+ * MACRO: ADD_CHUNKING_MEMORY_MANAGEMENT_CC()
+ * Aaron Stump, 6/11/99
+ *
+ * ABSTRACT: This macro should be called exactly once in a .cc file
+ * for the class THE_CLASS to add chunking memory management for the
+ * class.  This macro should be called with the same value for
+ * THE_CLASS as was used in calling
+ * C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_H in the body of the
+ * declaration of THE_CLASS.  THE_CHUNK_SIZE is the number of blocks
+ * of memory to get at once using malloc().  A block is the portion
+ * of memory needed for one instance of THE_CLASS.
+ *
+ *
+ * IMPLEMENTATION:
+ ************************************************************************
+ * FUNCTION: allocate_new_chunk()
+ * Aaron Stump, 6/8/99
+ *
+ * ABSTRACT: This method allocates a new chunk of memory to use for
+ * allocating instances of THE_CLASS.
+ ************************************************************************
+ * FUNCTION: new()
+ * Aaron Stump, 6/8/99
+ *
+ * ABSTRACT: This allocator uses chunks for more efficient allocation.
+ ************************************************************************
+ * FUNCTION: delete()
+ * Aaron Stump, 6/8/99
+ *
+ * ABSTRACT: This delete() puts the chunk pointed to by ptr on the 
+ * freelist.
+ ************************************************************************
+ * Chunking_Memory_Management_Initializer and its static instance are used
+ * to call the static init_chunks() method for THE_CLASS. 
+ ************************************************************************/
+#define C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_CC(THE_CLASS,THE_FIELD,THE_CHUNK_SIZE) \
+unsigned THE_CLASS::C_MACROS__CHUNK_SIZE = THE_CHUNK_SIZE;\
+\
+unsigned THE_CLASS::C_MACROS__BLOCK_SIZE = sizeof(THE_CLASS);\
+\
+void * THE_CLASS::C_MACROS__freelist = NULL;\
+char * THE_CLASS::C_MACROS__next_free_block = NULL;\
+char * THE_CLASS::C_MACROS__end_of_current_chunk = NULL;\
+bool THE_CLASS::C_MACROS__initialized = false;\
+\
+void \
+THE_CLASS::C_MACROS__allocate_new_chunk() {\
+\
+  unsigned tmp = C_MACROS__CHUNK_SIZE * C_MACROS__BLOCK_SIZE;\
+  char *chunk = (char *)malloc(tmp);\
+  \
+  assert (chunk != NULL);			\
+\
+  C_MACROS__next_free_block = chunk;\
+  C_MACROS__end_of_current_chunk = chunk + tmp;\
+}\
+\
+void * \
+THE_CLASS::operator new(size_t size, void *h) {\
+  (void)size; /* size should always be _BLOCK_SIZE */\
+\
+  if (h != NULL)\
+    /* we're being told what memory we should use */\
+    return h;\
+\
+  char *new_block;\
+\
+  if (C_MACROS__freelist) {\
+    /* we have a block on the freelist that we can use */\
+    new_block = (char *)C_MACROS__freelist;			\
+    C_MACROS__freelist = (void *)((THE_CLASS *)new_block)->THE_FIELD;	\
+  }\
+  else {\
+    /* we have to get a new block from a chunk (which we may */\
+    /* have to allocate*/\
+    \
+    if (C_MACROS__next_free_block == C_MACROS__end_of_current_chunk)\
+      C_MACROS__allocate_new_chunk();\
+    \
+    new_block = C_MACROS__next_free_block;\
+    C_MACROS__next_free_block += C_MACROS__BLOCK_SIZE;\
+  }\
+  \
+  return new_block;\
+}\
+\
+void \
+THE_CLASS::operator delete(void *ptr) {\
+  void **f = (void **)&((THE_CLASS *)ptr)->THE_FIELD;	\
+  *f = C_MACROS__freelist;	\
+  C_MACROS__freelist = ptr;				      \
+}
+
+#endif
+
diff --git a/proofs/lfsc_checker/code.cpp b/proofs/lfsc_checker/code.cpp
new file mode 100644
index 000000000..225700580
--- /dev/null
+++ b/proofs/lfsc_checker/code.cpp
@@ -0,0 +1,1377 @@
+#include "check.h"
+#include "code.h"
+#include <string>
+
+#include "scccode.h"
+
+using namespace std;
+
+string *eat_str(const char *str, bool check_end = true) {
+  string *s = new string();
+  char c, d;
+  while ((c = *str++)) {
+    d = our_getc();
+    if (c != d) {
+      our_ungetc(d);
+      return s;
+    }
+    s->push_back(d);
+  }
+
+  if (check_end &&
+      (d = our_getc()) != ' ' && d != '(' && d != '\n' && d != '\t') {
+    our_ungetc(d);
+    return s;
+  }
+   
+  delete s;
+  return 0;
+}
+
+SymSExpr *read_ctor() {
+  string id(prefix_id());
+#ifdef USE_HASH_TABLES
+  Expr *s = symbols[id];
+  Expr *stp = symbol_types[id];
+#else
+  pair<Expr *, Expr *> p = symbols->get(id.c_str());
+  Expr *s = p.first;
+  Expr *stp = p.second;
+#endif
+
+  if (!stp)
+    report_error("Undeclared identifier parsing a pattern.");
+
+  if (s->getclass() != SYMS_EXPR || ((SymExpr *)s)->val)
+    report_error("The head of a pattern is not a constructor.");
+
+  s->inc();
+
+  return (SymSExpr *)s;
+}
+
+Expr *read_case() {
+  eat_char('(');
+  Expr *pat = NULL;
+  vector<SymSExpr *> vars;
+
+#ifdef USE_HASH_MAPS
+  vector<Expr *>prevs;
+#else
+  vector<pair<Expr *,Expr *> >prevs;
+#endif
+  char d = non_ws();
+  switch(d) {
+  case '(': {
+    // parse application
+    SymSExpr *s = read_ctor();
+    pat = s;
+    char c;
+    while ((c = non_ws()) != ')') {
+	    our_ungetc(c);
+	    string varstr(prefix_id());
+	    SymSExpr *var = new SymSExpr(varstr);
+	    vars.push_back(var);
+#ifdef USE_HASH_MAPS
+	    prevs.push_back(symbols[varstr]);
+	    symbols[varstr] = var;
+#else
+	    prevs.push_back(symbols->insert(varstr.c_str(), 
+					    pair<Expr *, Expr *>(var,NULL)));
+#endif
+#ifndef USE_FLAT_APP
+	    pat = new CExpr(APP,pat,var);
+#else
+      pat = Expr::make_app(pat,var);
+#endif
+    }
+    break;
+  }
+  // default case
+  case 'd': {
+    delete eat_str("efault");
+  }
+    break;
+  case EOF:
+    report_error("Unexpected end of file parsing a pattern.");
+    break;
+  default:
+    // could be an identifier
+    our_ungetc(d);
+    pat = read_ctor();
+    break;
+  }
+  
+  Expr *ret = read_code();
+  if( pat )
+    ret = new CExpr(CASE, pat, ret);
+
+  for (int i = 0, iend = prevs.size(); i < iend; i++) {
+    string &s = vars[i]->s;
+#ifdef USE_HASH_MAPS
+    symbols[s] = prevs[i];
+#else
+    symbols->insert(s.c_str(), prevs[i]);
+#endif
+  }
+
+  eat_char(')');
+
+  return ret;
+}
+
+Expr *read_code() {
+  string *pref = NULL;
+  char d = non_ws();
+  switch(d) {
+    case '(': 
+    {
+      char c = non_ws(); 
+      switch (c) 
+      {
+        case 'd': 
+        {
+          our_ungetc('d');
+          pref = eat_str("do");
+          if (pref) 
+	          break;
+          Expr *ret = read_code();
+          while ((c = non_ws()) != ')') {
+	          our_ungetc(c);
+	          ret = new CExpr(DO,ret,read_code());
+          }
+          return ret;
+        }
+        case 'f': 
+        {
+          our_ungetc('f');
+          pref = eat_str("fail");
+          if (pref) 
+	          break;
+
+          Expr *c = read_code();
+          eat_char(')');
+
+          //do we need to check this???
+          //if (c->getclass() != SYMS_EXPR || ((SymExpr *)c)->val)
+	         // report_error(string("\"fail\" must be used with a (undefined) base ")
+		        //  +string("type.\n1. the expression used: "+c->toString()));
+          
+          return new CExpr(FAIL, c);
+        }
+        case 'l': 
+        {
+          our_ungetc('l');
+          pref = eat_str("let");
+          if (pref) 
+	          break;
+
+          string id(prefix_id());
+          SymSExpr *var = new SymSExpr(id);
+
+          Expr *t1 = read_code();
+
+#ifdef USE_HASH_MAPS
+          Expr *prev = symbols[id];
+          symbols[id] = var;
+#else
+          pair<Expr *, Expr *> prev = 
+	          symbols->insert(id.c_str(), pair<Expr *, Expr *>(var,NULL));
+#endif
+
+          Expr *t2 = read_code();
+      
+#ifdef USE_HASH_MAPS
+          symbols[id] = prev;
+#else
+          symbols->insert(id.c_str(), prev);
+#endif
+          eat_char(')');
+          return new CExpr(LET, var, t1, t2);
+        }
+        case 'i': 
+        {
+          our_ungetc('i');
+          pref = eat_str("ifmarked",false);
+          if (pref) 
+	          break;
+#ifndef MARKVAR_32
+          Expr *e1 = read_code();
+          Expr *e2 = read_code();
+          Expr *e3 = read_code();
+          Expr *ret = new CExpr(IFMARKED, e1, e2, e3);
+#else
+          int index = read_index();
+          Expr *e1 = read_code();
+          Expr *e2 = read_code();
+          Expr *e3 = read_code();
+          Expr *ret = NULL;
+          if( index>=1 && index<=32 )
+          {
+            ret = new CExpr( IFMARKED, new IntExpr( index-1 ), e1, e2, e3 );
+          }
+          else
+          {
+            std::cout << "Can't make IFMARKED with index = " << index << std::endl;
+          }
+          Expr::markedCount++;
+          //Expr *ret = new CExpr(IFMARKED, e1, e2, e3);
+#endif
+          eat_char(')');
+          return ret;
+        }
+        case 'm': 
+        {
+          char c;
+          switch ((c = our_getc())) 
+          {
+            case 'a': 
+            {
+	            char cc;
+	            switch ((cc = our_getc())) {
+	              case 't': 
+                {
+	                our_ungetc('t');
+	                pref = eat_str("tch");
+	                if (pref) {
+	                  pref->insert(0,"ma");
+	                  break;
+	                }
+	                vector<Expr *> cases;
+	                cases.push_back(read_code()); // the scrutinee
+	                while ((c = non_ws()) != ')' && c != 'd') {
+	                  our_ungetc(c);
+	                  cases.push_back(read_case());
+	                }
+	                if (cases.size() == 1) // counting scrutinee
+	                  report_error("A match has no cases.");
+                  if (c == 'd') {
+                    // we have a default case
+                    //delete eat_str("efault");
+                    our_ungetc(c);
+                    cases.push_back(read_case());
+                  }
+	                return new CExpr(MATCH,cases);
+                }
+	              case 'r': 
+                {
+	                our_ungetc('r');
+	                pref = eat_str("rkvar", false);
+	                if (pref) {
+	                  pref->insert(0,"ma");
+	                  break;
+	                }
+    #ifndef MARKVAR_32
+	                Expr *ret = new CExpr(MARKVAR,read_code());
+    #else
+                  int index = read_index();
+                  CExpr* ret = NULL;
+                  if( index>=1 && index<=32 )
+                  {
+                    ret = new CExpr( MARKVAR, new IntExpr( index-1 ), read_code() ); 
+                  }
+                  else
+                  {
+                    std::cout << "Can't make MARKVAR with index = " << index << std::endl;
+                  }
+          Expr::markedCount++;
+	                //Expr *ret = new CExpr(MARKVAR,read_code());
+              #endif
+
+	                eat_char(')');
+	                return ret;
+                }
+	              default:
+                  our_ungetc(c);
+	                pref = new string("ma");
+	                break;
+              }
+            }
+            case 'p': 
+            {
+	            our_ungetc('p');
+	            pref = eat_str("p_",false);
+	            if (pref) {
+	              pref->insert(0,"m");
+	              break;
+              }
+	            char c = our_getc();
+	            switch(c) {
+	            case 'a': 
+              {
+	              our_ungetc('a');
+	              pref = eat_str("add");
+	              if (pref) {
+	                pref->insert(0,"mp_");
+	                break;
+	              }
+                Expr* e1 = read_code();
+                Expr* e2 = read_code();
+	              Expr *ret = new CExpr(ADD, e1, e2);
+	              eat_char(')');
+	              return ret;
+	            }
+	            case 'n': 
+              {
+	              our_ungetc('n');
+	              pref = eat_str("neg");
+	              if (pref) {
+	                pref->insert(0,"mp_");
+	                break;
+	              }
+            	  
+	              Expr *ret = new CExpr(NEG, read_code());
+	              eat_char(')');
+	              return ret;
+	            }
+	            case 'i': 
+              {	// mpz_if_neg
+                char c = our_getc();
+                if( c=='f' )
+                {
+                  c = our_getc();
+                  switch( c )
+                  {
+                  case 'n': {
+                    our_ungetc('n');
+		                pref = eat_str("neg");
+		                if( pref ) {
+			                pref->insert(0,"mp_if");
+			                break;
+		                }
+		                Expr* e1 = read_code();
+                    Expr* e2 = read_code();
+                    Expr* e3 = read_code();
+		                Expr*	ret = new CExpr(IFNEG, e1, e2, e3 );
+		                eat_char(')');
+                    return ret;
+                  }
+                  case 'z': {
+                    our_ungetc('z');
+		                pref = eat_str("zero");
+		                if( pref ) {
+			                pref->insert(0,"mp_if");
+			                break;
+		                }
+		                Expr* e1 = read_code();
+                    Expr* e2 = read_code();
+                    Expr* e3 = read_code();
+		                Expr*	ret = new CExpr(IFZERO, e1, e2, e3 );
+		                eat_char(')');
+                    return ret;
+                  }
+                  default:
+                    our_ungetc(c);
+                    pref = new string("mp_if");
+                    break;
+                  }
+                }
+                else
+                {
+                  our_ungetc(c);
+                  pref = new string("mp_i");
+                  break;
+                }
+              }
+              case 'm':
+              {
+                our_ungetc('m');
+                pref = eat_str("mul");
+                if( pref ){
+                  pref->insert(0,"mp_");
+                  break;
+                }
+		            Expr* e1 = read_code();
+                Expr* e2 = read_code();
+		            Expr*	ret = new CExpr(MUL, e1, e2 );
+		            eat_char(')');
+		            return ret;
+              }
+              case 'd':
+              {
+                our_ungetc('d');
+                pref = eat_str("div");
+                if( pref ){
+                  pref->insert(0,"mp_");
+                  break;
+                }
+		            Expr* e1 = read_code();
+                Expr* e2 = read_code();
+		            Expr*	ret = new CExpr(DIV, e1, e2 );
+		            eat_char(')');
+		            return ret;
+              }
+	            default:
+                our_ungetc(c);
+	              pref = new string("mp_");
+	              break;
+	            }
+            }
+            default:
+              our_ungetc(c);
+	            pref = new string("m");
+	            break;
+            }
+            break;
+        }
+        case '~': {
+          Expr *e = read_code();
+          if( e->getclass()==INT_EXPR )
+          {
+            IntExpr *ee = (IntExpr *)e;
+            mpz_neg(ee->n, ee->n);
+            eat_char(')');
+            return ee;
+          }
+          else if( e->getclass() == RAT_EXPR )
+          {
+            RatExpr *ee = (RatExpr *)e;
+            mpq_neg(ee->n, ee->n);
+            eat_char(')');
+            return ee;
+          }
+          else
+          {
+            report_error("Negative sign with expr that is not an int. literal.");
+          }
+        }
+        case 'c':
+        {
+          our_ungetc('c');
+          pref = eat_str("compare");
+          if (pref) 
+	          break;
+          Expr *e1 = read_code();
+          Expr *e2 = read_code();
+          Expr *e3 = read_code();
+          Expr *e4 = read_code();
+          eat_char(')');
+          return new CExpr(COMPARE, e1, e2, e3, e4);
+        }
+          break;
+        case EOF:
+          report_error("Unexpected end of file.");
+          break;
+        default: 
+        { // the application case
+          our_ungetc(c);
+          break;
+        }
+      }
+      // parse application
+      if (pref) 
+        // we have eaten part of the name of an applied identifier
+        pref->append(prefix_id());
+      else
+        pref = new string(prefix_id());
+
+      Expr *ret = progs[*pref];
+      if (!ret) 
+#ifdef USE_HASH_TABLES
+        ret = symbols[*pref];
+#else
+        ret = symbols->get(pref->c_str()).first;
+#endif
+
+      if (!ret)
+        report_error(string("Undeclared identifier at head of an application: ")
+		    +*pref);
+
+      ret->inc();
+      delete pref;
+
+      while ((c = non_ws()) != ')') {
+        our_ungetc(c);
+#ifndef USE_FLAT_APP
+        ret = new CExpr(APP,ret,read_code());
+#else
+        Expr* ke = read_code();
+        ret = Expr::make_app(ret,ke);
+#endif
+        }
+      return ret;
+    } // end case '('
+    case EOF:
+      report_error("Unexpected end of file.");
+      break;
+    case '_': 
+      report_error("Holes may not be used in code.");
+      return NULL;
+    case '0':
+    case '1':
+    case '2':
+    case '3':
+    case '4':
+    case '5':
+    case '6':
+    case '7':
+    case '8':
+    case '9': 
+    {
+      our_ungetc(d);
+      string v;
+      char c;
+      while (isdigit(c = our_getc())) 
+        v.push_back(c);
+      bool parseMpq = false;
+      if( c=='/' )
+      {
+        parseMpq = true;
+        v.push_back(c);
+        while(isdigit(c = our_getc())) 
+          v.push_back(c);
+      }
+      our_ungetc(c);
+      if( parseMpq )
+      {
+        mpq_t num;
+        mpq_init(num);
+        if (mpq_set_str(num,v.c_str(),10) == -1  )
+	        report_error("Error reading a mpq numeral.");
+
+        Expr* e = new RatExpr( num );
+        return e;
+      }
+      else
+      {
+        mpz_t num;
+        if (mpz_init_set_str(num,v.c_str(),10) == -1)
+          report_error("Error reading a numeral.");
+        return new IntExpr(num);
+      }
+    }
+    default: 
+    {
+      our_ungetc(d);
+      string id(prefix_id());
+#ifdef USE_HASH_MAPS
+      Expr *ret = symbols[id];
+#else
+      pair<Expr *, Expr *> p = symbols->get(id.c_str());
+      Expr *ret = p.first;
+#endif
+      if (!ret) 
+        ret = progs[id];
+      if (!ret)
+        report_error(string("Undeclared identifier: ")+id);
+      ret->inc();
+      return ret;
+    }
+  }
+  report_error("Unexpected operator in a piece of code.");
+  return 0;
+}
+
+// the input is owned by the caller, the output by us (so do not dec it).
+Expr *check_code(Expr *_e) {
+  CExpr *e = (CExpr *)_e;
+  switch (e->getop()) {
+  case NOT_CEXPR:
+    switch (e->getclass()) {
+    case INT_EXPR:
+      return statMpz;
+    case RAT_EXPR:
+      return statMpq;
+    case SYM_EXPR: {
+      report_error("Internal error: an LF variable is encountered in code");
+      break;
+    }
+    case SYMS_EXPR: {
+#ifdef USE_HASH_MAPS
+      Expr *tp = symbol_types[((SymSExpr *)e)->s];
+#else
+      Expr *tp = symbols->get(((SymSExpr *)e)->s.c_str()).second;
+#endif
+      if (!tp)
+	report_error(string("A symbol is missing a type in a piece of code.")
+		     +string("\n1. the symbol: ")+((SymSExpr *)e)->s);
+      return tp;
+    }
+    case HOLE_EXPR:
+      report_error("Encountered a hole unexpectedly in code.");
+    default:
+      report_error("Unrecognized form of expr in code.");
+    }
+  case APP: {
+#ifdef USE_FLAT_APP
+    Expr* h = e->kids[0]->followDefs();
+    vector<Expr *> argtps;
+    int counter = 1;
+    while( e->kids[counter] )
+    {
+       argtps.push_back( check_code( e->kids[counter] ) );
+       counter++;
+    }
+    int iend = counter-1;
+#else
+    vector<Expr *> args;
+    Expr *h = (Expr *)e->collect_args(args);
+
+    int iend = args.size();
+    vector<Expr *> argtps(iend);
+    for (int i = 0; i < iend; i++) 
+      argtps[i] = check_code(args[i]);
+#endif
+
+    Expr *tp = NULL;
+    if (h->getop() == PROG){
+      tp = ((CExpr *)h)->kids[0];
+    }else {
+#ifdef USE_HASH_MAPS
+      tp = symbol_types[((SymSExpr *)h)->s];
+#else
+      tp = symbols->get(((SymSExpr *)h)->s.c_str()).second;
+#endif
+    }
+    
+    if (!tp)
+      report_error(string("The head of an application is missing a type in ")
+		   +string("code.\n1. the application: ")+e->toString());
+    
+    tp = tp->followDefs();
+
+    if (tp->getop() != PI)
+      report_error(string("The head of an application does not have ")
+		   +string("functional type in code.")
+		   +string("\n1. the application: ")+e->toString());
+    
+    CExpr *cur = (CExpr *)tp;
+    int i = 0;
+    while (cur->getop() == PI) {
+      if (i >= iend)
+	      report_error(string("A function is not being fully applied in code.\n")
+		          +string("1. the application: ")+e->toString()
+		          +string("\n2. its (functional) type: ")+cur->toString());
+      if( argtps[i]->getop()==APP )
+        argtps[i] = ((CExpr*)argtps[i])->kids[0];
+      if (argtps[i] != cur->kids[1]) {
+	      char buf[1024];
+	      sprintf(buf,"%d",i);
+	      report_error(string("Type mismatch for argument ")
+		          + string(buf)
+		          + string(" in application in code.\n")
+		          + string("1. the application: ")+e->toString()
+		          + string("\n2. the head's type: ")+tp->toString()
+#ifdef USE_FLAT_APP
+                + string("\n3. the argument: ")+e->kids[i+1]->toString()
+#else
+		          + string("\n3. the argument: ")+args[i]->toString()
+#endif
+		          + string("\n4. computed type: ")+argtps[i]->toString()
+		          + string("\n5. expected type: ")
+		          +cur->kids[1]->toString());
+      }
+      
+      //if (cur->kids[2]->free_in((SymExpr *)cur->kids[0]))
+      if( cur->get_free_in() ){
+        cur->calc_free_in();
+        //are you sure?
+        if( cur->get_free_in() )
+	        report_error(string("A dependently typed function is being applied in")
+		            +string(" code.\n1. the application: ")+e->toString()
+		            +string("\n2. the head's type: ")+tp->toString());
+        //ok, reset the mark
+        cur->setexmark();
+      }
+
+      i++;
+      cur = (CExpr *)cur->kids[2];
+    }
+    if (i < iend)
+      report_error(string("A function is being fully applied to too many ")
+		   +string("arguments in code.\n")
+		   +string("1. the application: ")+e->toString()
+		   +string("\n2. the head's type: ")+tp->toString());
+      
+    
+    return cur;
+  }
+  //is this right?
+  case MPZ:
+    return statType;
+    break;
+  case MPQ:
+    return statType;
+    break;
+  case DO: 
+    check_code(e->kids[0]);
+    return check_code(e->kids[1]);
+
+  case LET: {
+    SymSExpr * var = (SymSExpr *)e->kids[0];
+
+    Expr *tp1 = check_code(e->kids[1]);
+
+#ifdef USE_HASH_MAPS
+    Expr *prevtp = symbol_types[var->s];
+    symbol_types[var->s] = tp1;
+#else
+    pair<Expr *, Expr *> prev = 
+      symbols->insert(var->s.c_str(), pair<Expr *, Expr *>(NULL,tp1));
+#endif
+
+    Expr *tp2 = check_code(e->kids[2]);
+      
+#ifdef USE_HASH_MAPS
+    symbol_types[var->s] = prevtp;
+#else
+    symbols->insert(var->s.c_str(), prev);
+#endif
+    
+    return tp2;
+  }
+
+  case ADD: 
+  case MUL:
+  case DIV:
+  {
+    Expr *tp0 = check_code(e->kids[0]);
+    Expr *tp1 = check_code(e->kids[1]);
+
+    if (tp0 != statMpz && tp0 != statMpq )
+      report_error(string("Argument to mp_[arith] does not have type \"mpz\" or \"mpq\".\n")
+		   +string("1. the argument: ")+e->kids[0]->toString()
+		   +string("\n1. its type: ")+tp0->toString());
+    
+    if (tp0 != tp1)
+      report_error(string("Arguments to mp_[arith] have differing types.\n")
+		   +string("1. argument 1: ")+e->kids[0]->toString()
+		   +string("\n1. its type: ")+tp0->toString()
+		   +string("2. argument 2: ")+e->kids[1]->toString()
+		   +string("\n2. its type: ")+tp1->toString());
+    
+    return tp0;
+  }
+
+  case NEG: {
+    Expr *tp0 = check_code(e->kids[0]);
+    if (tp0 != statMpz && tp0 != statMpq )
+      report_error(string("Argument to mp_neg does not have type \"mpz\" or \"mpq\".\n")
+		   +string("1. the argument: ")+e->kids[0]->toString()
+		   +string("\n1. its type: ")+tp0->toString());
+    
+    return tp0;
+  }
+
+  case IFNEG: 
+  case IFZERO: {
+    Expr *tp0 = check_code(e->kids[0]);
+    if (tp0 != statMpz && tp0 != statMpq)
+      report_error(string("Argument to mp_if does not have type \"mpz\" or \"mpq\".\n")
+		   +string("1. the argument: ")+e->kids[0]->toString()
+		   +string("\n1. its type: ")+tp0->toString());
+    
+    SymSExpr *tp1 = (SymSExpr *)check_code(e->kids[1]);
+    SymSExpr *tp2 = (SymSExpr *)check_code(e->kids[2]);
+    if (tp1->getclass() != SYMS_EXPR || tp1->val || tp1 != tp2)
+      report_error(string("\"mp_if\" used with expressions that do not ")
+       +string("have equal simple datatypes\nfor their types.\n")
+       +string("0. 0'th expression: ")+e->kids[0]->toString()
+		   +string("\n1. first expression: ")+e->kids[1]->toString()
+		   +string("\n2. second expression: ")+e->kids[2]->toString()
+		   +string("\n3. first expression's type: ")+tp1->toString()
+		   +string("\n4. second expression's type: ")+tp2->toString());
+    return tp1;
+  }
+
+  case FAIL: {
+    Expr *tp = check_code(e->kids[0]);
+    if (tp != statType)
+      report_error(string("\"fail\" is used with an expression which is ")
+		   +string("not a type.\n1. the expression :")
+		   +e->kids[0]->toString()
+		   +string("\n2. its type: ")+tp->toString());
+    return e->kids[0];
+  }
+  case MARKVAR: {
+    SymSExpr *tp = (SymSExpr *)check_code(e->kids[1]);
+  
+    Expr* tptp = NULL;
+
+    if (tp->getclass() == SYMS_EXPR && !tp->val){
+#ifdef USE_HASH_MAPS
+      tptp = symbol_types[tp->s];
+#else
+      tptp = symbols->get(tp->s.c_str()).second;
+#endif
+    }
+
+    if (!tptp->isType( statType )){
+      string errstr = (string("\"markvar\" is used with an expression which ")
+		      +string("cannot be a lambda-bound variable.\n")
+		      +string("1. the expression :")
+		      +e->kids[1]->toString()
+		      +string("\n2. its type: ")+tp->toString());
+      report_error(errstr);
+    }
+
+    return tp;
+  }
+
+  case IFMARKED: 
+  {
+    SymSExpr *tp = (SymSExpr *)check_code(e->kids[1]);
+
+    Expr* tptp = NULL;
+   
+    if (tp->getclass() == SYMS_EXPR && !tp->val){
+#ifdef USE_HASH_MAPS
+      tptp = symbol_types[tp->s];
+#else
+      tptp = symbols->get(tp->s.c_str()).second;
+#endif
+    }
+    
+    if (!tptp->isType( statType ) ){
+      string errstr = (string("\"ifmarked\" is used with an expression which ")
+		      +string("cannot be a lambda-bound variable.\n")
+		      +string("1. the expression :")
+		      +e->kids[1]->toString()
+		      +string("\n2. its type: ")+tp->toString());
+      report_error(errstr);
+    }
+
+    SymSExpr *tp1 = (SymSExpr *)check_code(e->kids[2]);
+    SymSExpr *tp2 = (SymSExpr *)check_code(e->kids[3]);
+    if (tp1->getclass() != SYMS_EXPR || tp1->val || tp1 != tp2)
+      report_error(string("\"ifmarked\" used with expressions that do not ")
+       +string("have equal simple datatypes\nfor their types.\n")
+       +string("0. 0'th expression: ")+e->kids[1]->toString()
+		   +string("\n1. first expression: ")+e->kids[2]->toString()
+		   +string("\n2. second expression: ")+e->kids[3]->toString()
+		   +string("\n3. first expression's type: ")+tp1->toString()
+		   +string("\n4. second expression's type: ")+tp2->toString());
+    return tp1;
+  }
+  case COMPARE:
+  {
+    SymSExpr *tp0 = (SymSExpr *)check_code(e->kids[0]);
+    if (tp0->getclass() != SYMS_EXPR || tp0->val){
+      string errstr0 = (string("\"compare\" is used with a first expression which ")
+		      +string("cannot be a lambda-bound variable.\n")
+		      +string("1. the expression :")
+		      +e->kids[0]->toString()
+		      +string("\n2. its type: ")+tp0->toString());
+      report_error(errstr0);
+    }
+
+    SymSExpr *tp1 = (SymSExpr *)check_code(e->kids[1]);
+
+    if (tp1->getclass() != SYMS_EXPR || tp1->val){
+      string errstr1 = (string("\"compare\" is used with a second expression which ")
+		      +string("cannot be a lambda-bound variable.\n")
+		      +string("1. the expression :")
+		      +e->kids[1]->toString()
+		      +string("\n2. its type: ")+tp1->toString());
+      report_error(errstr1);
+    }
+
+    SymSExpr *tp2 = (SymSExpr *)check_code(e->kids[2]);
+    SymSExpr *tp3 = (SymSExpr *)check_code(e->kids[3]);
+    if (tp2->getclass() != SYMS_EXPR || tp2->val || tp2 != tp3)
+      report_error(string("\"compare\" used with expressions that do not ")
+       +string("have equal simple datatypes\nfor their types.\n")
+		   +string("\n1. first expression: ")+e->kids[2]->toString()
+		   +string("\n2. second expression: ")+e->kids[3]->toString()
+		   +string("\n3. first expression's type: ")+tp2->toString()
+		   +string("\n4. second expression's type: ")+tp3->toString());
+    return tp2;
+  }
+  case MATCH: 
+  {
+    SymSExpr *scruttp = (SymSExpr *)check_code(e->kids[0]);
+    Expr *tptp = NULL;
+    if (scruttp->getclass() == SYMS_EXPR && !scruttp->val){
+#ifdef USE_HASH_MAPS
+      tptp = symbol_types[scruttp->s];
+#else
+      tptp = symbols->get(scruttp->s.c_str()).second;
+#endif
+    }
+    if (!tptp->isType( statType )){
+      string errstr = (string("The scrutinee of a match is not ")
+		      +string("a plain piece of data.\n")
+		      +string("1. the scrutinee: ")
+		      +e->kids[0]->toString()
+		      +string("\n2. its type: ")+scruttp->toString());
+      report_error(errstr);
+    }
+
+    int i = 1;
+    Expr **cur = &e->kids[i];
+    Expr *mtp = NULL;
+    Expr *c_or_default;
+    CExpr *c;
+    while ((c_or_default = *cur++)) {
+      Expr *tp = NULL;
+      CExpr *pat = NULL;
+      if (c_or_default->getop() != CASE) 
+        // this is the default of the MATCH
+        tp = check_code(c_or_default);
+      else {
+        // this is a CASE of the MATCH
+        c = (CExpr *)c_or_default;
+        pat = (CExpr *)c->kids[0]; // might be just a SYMS_EXPR
+        if (pat->getclass() == SYMS_EXPR) 
+          tp = check_code(c->kids[1]);
+        else {
+          // extend type context and then check the body of the case
+#ifdef USE_HASH_MAPS
+          vector<Expr *>prevs;
+#else
+          vector<pair<Expr *,Expr *> >prevs;
+#endif
+          vector<Expr *> vars;
+          SymSExpr *ctor = (SymSExpr *)pat->collect_args(vars);
+#ifdef USE_HASH_MAPS
+          CExpr *ctortp = (CExpr *)symbol_types[ctor->s];
+#else
+          CExpr *ctortp = (CExpr *)symbols->get(ctor->s.c_str()).second;
+#endif
+          CExpr *curtp = ctortp;
+          for (int i = 0, iend = vars.size(); i < iend; i++) {
+            if ( curtp->followDefs()->getop() != PI)
+              report_error(string("Too many arguments to a constructor in")
+                           +string(" a pattern.\n1. the pattern: ")
+                           +pat->toString()
+                           +string("\n2. the head's type: "
+                                   +ctortp->toString()));
+#ifdef USE_HASH_MAPS
+            prevs.push_back(symbol_types[((SymSExpr *)vars[i])->s]);
+            symbol_types[((SymSExpr *)vars[i])] = curtp->followDefs()->kids[1];
+#else
+            prevs.push_back
+              (symbols->insert(((SymSExpr *)vars[i])->s.c_str(), 
+                               pair<Expr *, Expr *>(NULL,
+                                                    ((CExpr *)(curtp->followDefs()))->kids[1])));
+#endif
+            curtp = (CExpr *)((CExpr *)(curtp->followDefs()))->kids[2];
+          }
+
+          tp = check_code(c->kids[1]);
+	
+          for (int i = 0, iend = prevs.size(); i < iend; i++) {
+#ifdef USE_HASH_MAPS
+            symbol_types[((SymSExpr *)vars[i])->s] = prevs[i];
+#else
+            symbols->insert(((SymSExpr *)vars[i])->s.c_str(), prevs[i]);
+#endif
+          }
+        }
+      }
+
+      // check that the type for the body of this case -- or the default value --
+      // matches the type for the previous case if we had one.
+
+      if (!mtp)
+        mtp = tp;
+      else
+        if (mtp != tp)
+          report_error(string("Types for bodies of match cases or the default differ.")
+                       +string("\n1. type for first case's body: ")
+                       +mtp->toString()
+                       +(pat == NULL ? string("\n2. type for the default")
+                         : (string("\n2. type for the body of case for ")
+                            +pat->toString()))
+                       +string(": ")+tp->toString());
+      
+    }
+
+    return mtp;
+              }
+  } // end switch
+   
+  report_error("Type checking an unrecognized form of code (internal error).");
+  return NULL;
+}
+
+bool dbg_prog;
+bool run_scc;
+int dbg_prog_indent_lvl = 0;
+
+void dbg_prog_indent(std::ostream &os) {
+  for (int i = 0; i < dbg_prog_indent_lvl; i++)
+    os << " ";
+}
+
+Expr *run_code(Expr *_e) {
+ start_run_code:
+  CExpr *e = (CExpr *)_e;
+  if( e )
+  {
+    //std::cout << ". ";
+    //e->print( std::cout );
+    //std::cout << std::endl;
+    //std::cout << e->getop() << " " << e->getclass() << std::endl;
+  }
+  switch (e->getop()) {
+  case NOT_CEXPR:
+    switch(e->getclass()) {
+    case INT_EXPR:
+    case RAT_EXPR:
+      e->inc();
+      return e;
+    case HOLE_EXPR: {
+      Expr *tmp = e->followDefs();
+      if (tmp == e) 
+	      report_error("Encountered an unfilled hole running code.");
+      tmp->inc();
+      return tmp;
+    }
+    case SYMS_EXPR: 
+    case SYM_EXPR: {
+      Expr *tmp = e->followDefs();
+      //std::cout << "follow def = ";
+      //tmp->print( std::cout );
+      //std::cout << std::endl;
+      if (tmp == e) {
+	      e->inc();
+	      return e;
+      }
+      tmp->inc();
+      return tmp;
+    }
+    }
+  case FAIL:
+    return NULL;
+  case DO: {
+    Expr *tmp = run_code(e->kids[0]);
+    if (!tmp)
+      return NULL;
+    tmp->dec();
+    _e = e->kids[1];
+    goto start_run_code;
+  }
+  case LET: {
+    Expr *r0 = run_code(e->kids[1]);
+    if (!r0)
+      return NULL;
+    SymExpr *var = (SymExpr *)e->kids[0];
+    Expr *prev = var->val;
+    var->val = r0;
+    Expr *r1 = run_code(e->kids[2]);
+    var->val = prev;
+    r0->dec();
+    return r1;
+  }
+  case ADD: 
+  case MUL:
+  case DIV:
+  {
+    Expr *r1 = run_code(e->kids[0]);
+    if (!r1)
+      return NULL;
+    Expr *r2 = run_code(e->kids[1]);
+    if (!r2)
+      return NULL;
+    if( r1->getclass()==INT_EXPR && r2->getclass()==INT_EXPR )
+    {
+      mpz_t r;
+      mpz_init(r);
+      if( e->getop()==ADD )
+        mpz_add(r, ((IntExpr *)r1)->n, ((IntExpr *)r2)->n);
+      else if( e->getop()==MUL )
+        mpz_mul(r, ((IntExpr *)r1)->n, ((IntExpr *)r2)->n);
+      else if( e->getop()==DIV )
+        mpz_cdiv_q(r, ((IntExpr *)r1)->n, ((IntExpr *)r2)->n);
+      r1->dec();
+      r2->dec();
+      return new IntExpr(r);
+    }
+    else if( r1->getclass()==RAT_EXPR && r2->getclass()==RAT_EXPR )
+    {
+      mpq_t q;
+      mpq_init(q);
+      if( e->getop()==ADD )
+        mpq_add(q, ((RatExpr *)r1)->n, ((RatExpr *)r2)->n);
+      else if( e->getop()==MUL )
+        mpq_mul(q, ((RatExpr *)r1)->n, ((RatExpr *)r2)->n);
+      else if( e->getop()==DIV )
+        mpq_div(q, ((RatExpr *)r1)->n, ((RatExpr *)r2)->n);
+      r1->dec();
+      r2->dec();
+      return new RatExpr(q);
+    }
+    else
+    {
+      //std::cout << "An arithmetic operation failed. " << r1->getclass() << " " << r2->getclass() << std::endl;
+      r1->dec();
+      r2->dec();
+      return NULL;
+    }
+  }
+  case NEG: {
+    Expr *r1 = run_code(e->kids[0]);
+    if (!r1)
+      return NULL;
+    if (r1->getclass() == INT_EXPR) {
+      mpz_t r;
+      mpz_init(r);
+      mpz_neg(r, ((IntExpr *)r1)->n);
+      r1->dec();
+      return new IntExpr(r);
+    }
+    else if( r1->getclass() == RAT_EXPR ) {
+      mpq_t q;
+      mpq_init(q);
+      mpq_neg(q, ((RatExpr *)r1)->n);
+      r1->dec();
+      return new RatExpr(q);
+    }
+    else
+    {
+      std::cout << "An arithmetic negation failed. " << r1->getclass() << std::endl;
+      //((SymSExpr*)r1)->val->print( std::cout );
+      std::cout << ((SymSExpr*)r1)->val << std::endl;
+      r1->dec();
+      return NULL;
+    }
+  }
+  case IFNEG: 
+  case IFZERO:{
+    Expr *r1 = run_code(e->kids[0]);
+    if (!r1)
+      return NULL;
+
+    bool cond;
+    if( r1->getclass() == INT_EXPR ){
+      if( e->getop() == IFNEG )
+        cond = mpz_sgn( ((IntExpr *)r1)->n )<0;
+      else if( e->getop() == IFZERO )
+        cond = mpz_sgn( ((IntExpr *)r1)->n )==0;
+    }else if( r1->getclass() == RAT_EXPR ){
+      if( e->getop() == IFNEG )
+        cond = mpq_sgn( ((RatExpr *)r1)->n )<0;
+      else if( e->getop() == IFZERO ) 
+        cond = mpq_sgn( ((RatExpr *)r1)->n )==0;
+    }
+    else
+    {
+      std::cout << "An arithmetic if-expression failed. " << r1->getclass() << std::endl;
+      r1->dec();
+      return NULL;
+    }
+    r1->dec();
+
+
+    if( cond )
+      _e = e->kids[1];
+    else
+      _e = e->kids[2];
+    goto start_run_code;
+  }
+  case IFMARKED: {
+    Expr *r1 = run_code(e->kids[1]);
+    if (!r1)
+      return NULL;
+    if(r1->getclass() != SYM_EXPR && r1->getclass() != SYMS_EXPR ){
+      r1->dec();
+      return NULL;
+    }
+#ifndef MARKVAR_32
+    if (r1->getexmark()) {
+#else
+    if(((SymExpr*)r1)->getmark( ((IntExpr*)e->kids[0])->get_num() ) ){
+#endif
+      r1->dec();
+      _e = e->kids[2];
+      goto start_run_code;
+    }
+    // else
+    r1->dec();
+    _e = e->kids[3];
+    goto start_run_code;
+  }
+  case COMPARE:
+  {
+    Expr *r1 = run_code(e->kids[0]);
+    if (!r1)
+      return NULL;
+    if (r1->getclass() != SYM_EXPR && r1->getclass() != SYMS_EXPR) {
+      r1->dec();
+      return NULL;
+    }
+    Expr *r2 = run_code(e->kids[1]);
+    if (!r2)
+      return NULL;
+    if (r2->getclass() != SYM_EXPR && r2->getclass() != SYMS_EXPR) {
+      r2->dec();
+      return NULL;
+    }
+    if( r1<r2 ){
+      r1->dec();
+      _e = e->kids[2];
+      goto start_run_code;
+    }
+    //else 
+    r2->dec();
+    _e = e->kids[3];
+    goto start_run_code;
+  }
+  case MARKVAR: {
+    Expr *r1 = run_code(e->kids[1]);
+    if (!r1)
+      return NULL;
+    if (r1->getclass() != SYM_EXPR && r1->getclass() != SYMS_EXPR) {
+      r1->dec();
+      return NULL;
+    }
+#ifndef MARKVAR_32
+    if (r1->getexmark())
+      r1->clearexmark();
+    else
+      r1->setexmark();
+#else
+    if(((SymExpr*)r1)->getmark( ((IntExpr*)e->kids[0])->get_num() ) )
+      ((SymExpr*)r1)->clearmark( ((IntExpr*)e->kids[0])->get_num() );
+    else
+      ((SymExpr*)r1)->setmark( ((IntExpr*)e->kids[0])->get_num() );
+#endif
+    return r1;
+  }
+  case MATCH: {
+    Expr *scrut = run_code(e->kids[0]);
+    if (!scrut)
+      return 0;
+    vector<Expr *> args;
+    Expr *hd = scrut->collect_args(args);
+    Expr **cases = &e->kids[1];
+    CExpr *c;
+    Expr *c_or_default;
+    while ((c_or_default = *cases++)) {
+
+      if (c_or_default->getop() != CASE){
+        //std::cout << "run the default " << std::endl;
+        //c_or_default->print( std::cout );
+        // this is the default of the MATCH
+        return run_code(c_or_default);
+      }
+
+      // this is a CASE of the MATCH
+      CExpr *c = (CExpr *)c_or_default;
+      Expr *p = c->kids[0];
+      if (hd == p->get_head()) {
+	      vector<Expr *> vars;
+	      p->collect_args(vars);
+	      int jend = args.size();
+	      vector<Expr *> old_vals(jend);
+	      for (int j = 0; j < jend; j++) {
+	        SymExpr *var = (SymExpr *)vars[j];
+	        old_vals[j] = var->val;
+	        var->val = args[j];
+	        args[j]->inc();
+	      }
+	      scrut->dec();
+	      Expr *ret = run_code(c->kids[1] /* the body of the case */);
+	      for (int j = 0; j < jend; j++) {
+	        ((SymExpr *)vars[j])->val = old_vals[j];
+	        args[j]->dec();
+	      }
+	      return ret;
+      }
+    }
+    break;
+  }
+  case APP: {
+    Expr *tmp = e->whr();
+    if (e != tmp) {
+      _e = tmp;
+      goto start_run_code;
+    }
+
+    // e is in weak head normal form
+
+    vector<Expr *> args;
+    Expr *hd = e->collect_args(args);
+    for (int i = 0, iend = args.size(); i < iend; i++) 
+      if (!(args[i] = run_code(args[i]))) {
+	      for (int j = 0; j < i; j++)
+	         args[j]->dec();
+	      return NULL;
+      }
+    if (hd->getop() != PROG) {
+      hd->inc();
+      Expr *tmp = Expr::build_app(hd,args);
+      return tmp;
+    }
+
+    CExpr *prog = (CExpr *)hd;
+    Expr **cur = ((CExpr *)prog->kids[1])->kids;
+    vector<Expr *> old_vals;
+    SymExpr *var;
+    int i = 0;
+
+    if( run_scc && e->get_head( false )->getclass()==SYMS_EXPR )
+    {
+      //std::cout << "running " << ((SymSExpr*)e->get_head( false ))->s.c_str() << " with " << (int)args.size() << " arguments" << std::endl;
+//#ifndef USE_FLAT_APP
+//      for( int a=0; a<(int)args.size(); a++ )
+//      {
+//        args[a] = CExpr::convert_to_flat_app( args[a] );
+//      }
+//#endif
+      Expr *ret = run_compiled_scc( e->get_head( false ), args );
+      for (int i = 0, iend = args.size(); i < iend; i++) {
+        args[i]->dec();
+      }
+//#ifndef USE_FLAT_APP
+//      ret = CExpr::convert_to_tree_app( ret );
+//#endif
+      //ret->inc();
+      return ret;
+    }
+    else
+    {
+      while((var = (SymExpr *)*cur++)) {
+        old_vals.push_back(var->val);
+        var->val = args[i++];
+      }
+
+      if (dbg_prog) {
+        dbg_prog_indent(cout);
+        cout << "[";
+        e->print(cout);
+        cout << "\n";
+      }
+      dbg_prog_indent_lvl++;
+
+      Expr *ret = run_code(prog->kids[2]);
+
+      dbg_prog_indent_lvl--;
+      if (dbg_prog) {
+        dbg_prog_indent(cout);
+        cout << "= ";
+        if (ret)
+	        ret->print(cout);
+        else
+	        cout << "fail";
+        cout << "]\n";
+      }
+
+      cur = ((CExpr *)prog->kids[1])->kids;
+      i = 0;
+      while((var = (SymExpr *)*cur++)) {
+        args[i]->dec();
+        var->val = old_vals[i++];
+      }
+      return ret;
+    }
+  }
+  } // end switch
+  return NULL;
+}
+
+int read_index()
+{
+  int index = 1;
+  string v;
+  char c;
+  while (isdigit(c = our_getc()))
+    v.push_back(c);
+  our_ungetc(c);
+  if( v.length()>0 )
+  {
+    index = atoi( v.c_str() );
+  }
+  return index;
+}
\ No newline at end of file
diff --git a/proofs/lfsc_checker/code.h b/proofs/lfsc_checker/code.h
new file mode 100644
index 000000000..9d00a6378
--- /dev/null
+++ b/proofs/lfsc_checker/code.h
@@ -0,0 +1,15 @@
+#ifndef SC2_CODE_H
+#define SC2_CODE_H
+
+#include "expr.h"
+
+Expr *read_code();
+Expr *check_code(Expr *); // compute the type for the given code
+Expr *run_code(Expr *); 
+
+int read_index();
+
+extern bool dbg_prog;
+extern bool run_scc;
+
+#endif 
diff --git a/proofs/lfsc_checker/configure.ac b/proofs/lfsc_checker/configure.ac
new file mode 100644
index 000000000..245b0ea65
--- /dev/null
+++ b/proofs/lfsc_checker/configure.ac
@@ -0,0 +1,47 @@
+#                                               -*- Autoconf -*-
+# Process this file with autoconf to produce a configure script.
+
+AC_PREREQ([2.68])
+AC_INIT([lfsc-checker], [1.0], [cvc-bugs@cs.nyu.edu])
+AC_CONFIG_SRCDIR([libwriter.h])
+AC_CONFIG_AUX_DIR([config])
+AC_CONFIG_MACRO_DIR([config])
+AC_CONFIG_HEADERS([config.h])
+AM_INIT_AUTOMAKE([1.11 foreign no-define tar-pax])
+LT_INIT
+
+AC_CANONICAL_BUILD
+AC_CANONICAL_HOST
+AC_CANONICAL_TARGET
+
+m4_ifdef([AM_SILENT_RULES],[AM_SILENT_RULES([yes])])
+
+# on by default
+AM_MAINTAINER_MODE([enable])
+
+# turn off static lib building by default
+AC_ENABLE_SHARED
+AC_DISABLE_STATIC
+
+# Checks for programs.
+AC_PROG_CXX
+AC_PROG_CC
+
+# Checks for libraries.
+# FIXME: Replace `main' with a function in `-lgmp':
+AC_CHECK_LIB([gmp], [__gmpz_init])
+
+# Checks for header files.
+AC_CHECK_HEADERS([stdlib.h string.h])
+
+# Checks for typedefs, structures, and compiler characteristics.
+AC_HEADER_STDBOOL
+AC_C_INLINE
+AC_TYPE_SIZE_T
+
+# Checks for library functions.
+AC_FUNC_MALLOC
+AC_CHECK_FUNCS([strdup])
+
+AC_CONFIG_FILES([Makefile])
+AC_OUTPUT
diff --git a/proofs/lfsc_checker/expr.cpp b/proofs/lfsc_checker/expr.cpp
new file mode 100644
index 000000000..7ffc6469a
--- /dev/null
+++ b/proofs/lfsc_checker/expr.cpp
@@ -0,0 +1,966 @@
+#include "expr.h"
+#include <stdlib.h>
+#include <sstream>
+#ifdef _MSC_VER
+#include <algorithm>
+#endif
+#include "check.h"
+
+using namespace std;
+
+int HoleExpr::next_id = 0;
+int Expr::markedCount = 0;
+
+C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_CC(CExpr,kids,32768);
+
+//C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_CC(IntCExpr,_n,32768);
+
+#define USE_HOLE_PATH_COMPRESSION
+
+void Expr::debug() {
+  print(cout);
+  /*
+  cout << "\nAt " << this << "\n";
+  cout << "marked = " << getmark() << "\n";
+  */
+  cout << "\n";
+  cout.flush();
+}
+
+bool destroy_progs = false;
+
+#define destroydec(rr) \
+  do { \
+    Expr *r = rr;	    \
+    int ref = r->data >> 9; \
+    ref = ref - 1; \
+    r->debugrefcnt(ref,DEC); \
+    if (ref == 0) {  \
+      _e = r;		  \
+      goto start_destroy; \
+    } \
+    else \
+      r->data = (ref << 9) | (r->data & 511); \
+  } while(0)
+
+
+void Expr::destroy(Expr *_e, bool dec_kids) {
+ start_destroy:
+  switch (_e->getclass()) {
+  case INT_EXPR:
+    delete (IntExpr *)_e;
+    break;
+  case SYMS_EXPR:  {
+    SymSExpr *e = (SymSExpr *)_e;
+    if (e->val && e->val->getop() != PROG) {
+      Expr *tmp = e->val;
+      delete e;
+      destroydec(tmp);
+    }
+    else
+      delete e;
+    break;
+  }
+  case SYM_EXPR: {
+    SymExpr *e = (SymExpr *)_e;
+    if (e->val && e->val->getop() != PROG) {
+      Expr *tmp = e->val;
+      delete e;
+      destroydec(tmp);
+    }
+    else
+      delete e;
+    break;
+  }
+  case HOLE_EXPR: {
+    HoleExpr *e = (HoleExpr *)_e;
+    if (e->val) {
+      Expr *tmp = e->val;
+      delete e;
+      destroydec(tmp);
+    }
+    else
+      delete e;
+    break;
+  }
+  case CEXPR: {
+    CExpr *e = (CExpr *)_e;
+    if (dec_kids) {
+      Expr **cur = e->kids;
+      Expr *tmp;
+      while((tmp = *cur++)) {
+	if (*cur)
+	  tmp->dec();
+	else {
+	  delete e;
+	  destroydec(tmp);
+	  break;
+	}
+      }
+    }
+    else
+      delete e;
+    break;
+  }
+  }
+}
+
+Expr *Expr::clone() {
+  switch (getclass()) {
+  case INT_EXPR:
+  case RAT_EXPR:
+    inc();
+    return this;
+  case SYMS_EXPR: 
+  case SYM_EXPR: {
+    SymExpr *e = (SymExpr *)this;
+    if (e->val)
+      if (e->val->getop() != PROG)
+	return e->val->clone();
+    e->inc();
+    return e;
+  }
+  case HOLE_EXPR: {
+    HoleExpr *e = (HoleExpr *)this;
+    if (e->val)
+      return e->val->clone();
+    e->inc();
+    return e;
+  }
+  case CEXPR: {
+    CExpr *e = (CExpr *)this;
+    int op = e->getop();
+    switch(op) {
+    case LAM: {
+#ifdef DEBUG_SYM_NAMES
+      SymSExpr *var = (SymSExpr *)e->kids[0];
+      SymSExpr *newvar = new SymSExpr(*var,SYMS_EXPR);
+#else
+      SymExpr *var = (SymExpr *)e->kids[0];
+      SymExpr *newvar = new SymExpr(*var);
+#endif
+      Expr *prev = var->val;
+      var->val = newvar;
+      Expr *bod = e->kids[1]->clone();
+      var->val = prev;
+      return new CExpr(LAM,newvar,bod);
+    }
+    case PI: {
+#ifdef DEBUG_SYM_NAMES
+      SymSExpr *var = (SymSExpr *)e->kids[0];
+      SymSExpr *newvar = new SymSExpr(*var,SYMS_EXPR);
+#else
+      SymExpr *var = (SymExpr *)e->kids[0];
+      SymExpr *newvar = new SymExpr(*var);
+#endif
+      Expr *tp = e->kids[1]->clone();
+      Expr *prev = var->val;
+      var->val = newvar;
+      Expr *bod = e->kids[2]->clone();
+      var->val = prev;
+      Expr* ret = new CExpr(PI,newvar,tp,bod);
+      if( data&256 )
+         ret->data |=256;
+      return ret;
+    }
+    default: {
+      Expr **cur = e->kids;
+      Expr *tmp;
+      int size = 0;
+      while((*cur++))
+	      size++;
+      Expr **kids = new Expr*[size+1];
+      kids[size]=0;
+      cur = e->kids;
+      bool diff_kid = false;
+      int i = 0;
+      while((tmp = *cur++)) {
+	      Expr *c = tmp->clone();
+	      diff_kid |= (c != tmp);
+	      kids[i++] = c;
+      }
+      if (diff_kid)
+	      return new CExpr(op, true /* dummy */, kids);
+      for (int i = 0, iend = size; i != iend; i++)
+	kids[i]->dec();
+      delete[] kids;
+      e->inc();
+      return e;
+    }
+    }
+  }
+  }
+  return 0; // should never be reached
+}
+
+
+Expr* Expr::build_app(Expr *hd, const std::vector<Expr *> &args, int start) {
+#ifndef USE_FLAT_APP
+  Expr *ret = hd;
+  for (int i = start, iend = args.size(); i < iend; i++)
+    ret = new CExpr(APP,ret,args[i]);
+  return ret;
+#else
+  if( start>=(int)args.size() )
+    return hd;
+  else
+  {
+    CExpr *ret = new CExpr( APP );
+    ret->kids = new Expr* [args.size()-start+2];
+    ret->kids[0] = hd;
+    for (int i = start, iend = args.size(); i < iend; i++)
+        ret->kids[i-start+1] = args[i];
+    ret->kids[args.size()-start+1] = NULL;
+    return ret;
+  }
+#endif
+}
+
+Expr* Expr::make_app(Expr* e1, Expr* e2 )
+{
+   //std::cout << "make app from ";
+   //e1->print( std::cout );
+   //std::cout << " ";
+   //e2->print( std::cout );
+   //std::cout << std::endl;
+   CExpr *ret;
+   if( e1->getclass()==CEXPR ){
+      int counter = 0;
+      while( ((CExpr*)e1)->kids[counter] ){
+         counter++;
+      }
+      ret = new CExpr( APP );
+      ret->kids = new Expr* [counter+2];
+      counter = 0;
+      while( ((CExpr*)e1)->kids[counter] ){
+         ret->kids[counter] = ((CExpr*)e1)->kids[counter];
+         counter++;
+      }
+      ret->kids[counter] = e2;
+      ret->kids[counter+1] = NULL;
+   }else{
+      ret = new CExpr( APP, e1, e2 );
+   }
+   //ret->print( std::cout );
+   //std::cout << std::endl;
+   return ret;
+}
+
+int Expr::cargCount = 0;
+
+Expr *Expr::collect_args(std::vector<Expr *> &args, bool follow_defs) {
+   //cargCount++;
+   //if( cargCount%1000==0)
+   //std::cout << cargCount << std::endl;
+#ifndef USE_FLAT_APP
+  CExpr *e = (CExpr *)this;
+  args.reserve(16);
+  while( e->getop() == APP ) {
+    args.push_back(e->kids[1]);
+    e = (CExpr *)e->kids[0];
+    if (follow_defs)
+      e = (CExpr *)e->followDefs();
+  }
+  std::reverse(args.begin(),args.end());
+  return e;
+#else
+  CExpr *e = (CExpr *)this;
+  args.reserve(16);
+  if( e->getop()==APP ){
+      int counter = 1;
+      while( e->kids[counter] ) {
+         args.push_back(e->kids[counter]);
+         counter++;
+      }
+      e = (CExpr*)e->kids[0];
+  }
+  if (follow_defs)
+      return e->followDefs();
+  else
+      return e;
+#endif
+}
+
+Expr *Expr::get_head(bool follow_defs) {
+  CExpr *e = (CExpr *)this;
+  while( e->getop() == APP ) {
+    e = (CExpr *)e->kids[0];
+    if (follow_defs)
+      e = (CExpr *)e->followDefs();
+  }
+  return e;
+}
+
+Expr *Expr::get_body(int op, bool follow_defs) {
+  CExpr *e = (CExpr *)this;
+  while( e->getop() == op ) {
+    e = (CExpr *)e->kids[2];
+    if (follow_defs)
+      e = (CExpr *)e->followDefs();
+  }
+  return e;
+}
+
+// if the return value is different from this, then it is a new reference
+Expr *CExpr::whr() {
+  vector<Expr *> args;
+  if (get_head()->getop() == LAM) {
+    CExpr *head = (CExpr *)collect_args(args, true);
+    Expr *cloned_head;
+    if (head->cloned()) {
+      // we must clone
+      head = (CExpr *)head->clone();
+      cloned_head = head;
+    }
+    else {
+      head->setcloned();
+      cloned_head = 0;
+    }
+    int i = 0;
+    int iend = args.size();
+
+    /* we will end up incrementing the ref count for all the args,
+       since each is either pointed to by a var (following a
+       beta-reduction), or else just an argument in the new
+       application we build below. */
+
+    do {
+      Expr *tmp = args[i++]->followDefs();
+      ((SymExpr *)head->kids[0])->val = tmp;
+      tmp->inc();
+      head = (CExpr *)head->kids[1];
+    } while(head->getop() == LAM && i < iend);
+    for (; i < iend; i++)
+      args[i]->inc();
+    head->inc();
+    if (cloned_head)
+      cloned_head->dec();
+    return build_app(head,args,i);
+  }
+  else 
+    return this;
+}
+
+Expr* CExpr::convert_to_tree_app( Expr* e )
+{
+  if( e->getop()==APP )
+  {
+    std::vector< Expr* > kds;
+    int counter = 1;

+    while( ((CExpr*)e)->kids[counter] )

+    {
+      kds.push_back( convert_to_tree_app( ((CExpr*)e)->kids[counter] ) );
+      counter++;
+    }
+    Expr* app = Expr::build_app( e->get_head(), kds );
+    //app->inc();
+    return app;
+  }
+  else
+  {
+    return e;
+  }
+}
+
+Expr* CExpr::convert_to_flat_app( Expr* e )
+{
+  if( e->getop()==APP )
+  {
+    std::vector< Expr* > args;
+    Expr* hd = ((CExpr*)e)->collect_args( args );
+    CExpr* nce = new CExpr( APP );
+    nce->kids = new Expr *[(int)args.size()+2];
+    nce->kids[0] = hd;
+    for( int a=0; a<(int)args.size(); a++ )
+    {
+      nce->kids[a+1] = convert_to_flat_app( args[a] );
+    }
+    nce->kids[(int)args.size()+1] = 0;
+    nce->inc();
+    return nce;
+  }
+  else
+  {
+    return e;
+  }
+}
+
+bool Expr::defeq(Expr *e) {
+
+  /* we handle a few special cases up front, where this Expr might
+     equal e, even though they have different opclass (i.e., different
+     structure). */
+
+  if (this == e)
+    return true;
+  int op1 = getop();
+  int op2 = e->getop();
+  switch (op1) {
+  case ASCRIBE:
+    return ((CExpr *)this)->kids[0]->defeq(e);
+  case APP: {
+    Expr *tmp = ((CExpr *)this)->whr();
+    if (tmp != this) {
+      bool b = tmp->defeq(e);
+      tmp->dec();
+      return b;
+    }
+    if (get_head()->getclass() == HOLE_EXPR) {
+      vector<Expr *> args;
+      Expr *head = collect_args(args, true);
+      Expr *t = e;
+      t->inc();
+      for (int i = 0, iend = args.size(); i < iend; i++) {
+	      // don't worry about SYMS_EXPR's, since we should not be in code here.
+	      if (args[i]->getclass() != SYM_EXPR || args[i]->getexmark())
+	        /* we cannot fill the hole in this case.  Either this is not
+	          a variable or we are using a variable again. */
+	        return false;
+	      SymExpr *v = (SymExpr *)args[i];
+
+	      // we may have been mapping from expected var v to a computed var
+	      Expr *tmp = (v->val ? v->val : v);
+
+	      tmp->inc();
+	      t = new CExpr(LAM, tmp, t);
+	      args[i]->setexmark();
+      }
+      for (int i = 0, iend = args.size(); i < iend; i++) 
+	      args[i]->clearexmark();
+#ifdef DEBUG_HOLES
+      cout << "Filling hole ";
+      head->debug();
+      cout << "with ";
+      t->debug();
+#endif
+      ((HoleExpr *)head)->val = t;
+      return true;
+    }
+    break;
+  }
+  case NOT_CEXPR:
+    switch (getclass()) {
+    case HOLE_EXPR: {
+      HoleExpr *h = (HoleExpr *)this;
+      if (h->val)
+	      return h->val->defeq(e);
+#ifdef DEBUG_HOLES
+      cout << "Filling hole ";
+      h->debug();
+      cout << "with ";
+      e->debug();
+#endif
+#ifdef USE_HOLE_PATH_COMPRESSION
+      Expr *tmp = e->followDefs();
+#else
+      Expr *tmp = e;
+#endif
+      h->val = tmp;
+      tmp->inc();
+      return true;
+    }
+    case SYMS_EXPR: 
+    case SYM_EXPR: {
+      SymExpr *s = (SymExpr *)this;
+      if (s->val)
+	return s->val->defeq(e);
+      break;
+    }
+    }
+    break;
+  }
+  
+  switch (op2) {
+  case ASCRIBE:
+    return defeq(((CExpr *)e)->kids[0]);
+  case APP: {
+    Expr *tmp = ((CExpr *)e)->whr();
+    if (tmp != e) {
+      bool b = defeq(tmp);
+      tmp->dec();
+      return b;
+    }
+    break;
+  }
+  case NOT_CEXPR:
+    switch (e->getclass()) {
+    case HOLE_EXPR: {
+      HoleExpr *h = (HoleExpr *)e;
+      if (h->val)
+	return defeq(h->val);
+
+#ifdef DEBUG_HOLES
+      cout << "Filling hole ";
+      h->debug();
+      cout << "with ";
+      debug();
+#endif
+#ifdef USE_HOLE_PATH_COMPRESSION
+      Expr *tmp = followDefs();
+#else
+      Expr *tmp = this;
+#endif
+      h->val = tmp;
+      tmp->inc();
+      return true;
+    }
+    case SYMS_EXPR: 
+    case SYM_EXPR: {
+      SymExpr *s = (SymExpr *)e;
+      if (s->val)
+	return defeq(s->val);
+      break;
+    }
+    }
+    break;
+  }
+
+  /* at this point, e1 and e2 must have the same opclass if they are 
+     to be equal. */
+
+  if (op1 != op2)
+    return false;
+  
+  if (op1 == NOT_CEXPR) {
+    switch(getclass()) {
+    case INT_EXPR: {
+      IntExpr *i1 = (IntExpr *)this;
+      IntExpr *i2 = (IntExpr *)e;
+      return (mpz_cmp(i1->n,i2->n) == 0);
+    }
+    case RAT_EXPR: {
+      RatExpr *r1 = (RatExpr *)this;
+      RatExpr *r2 = (RatExpr *)e;
+      return (mpq_cmp(r1->n,r2->n) == 0);
+    }
+    case SYMS_EXPR: 
+    case SYM_EXPR: 
+      return (this == e);
+    }
+  }
+
+  /* Now op1 and op2 must both be CExprs, and must have the same op to be
+     equal. */
+
+  CExpr *e1 = (CExpr *)this;
+  CExpr *e2 = (CExpr *)e;
+
+  int last = 1;
+  switch (op1) {
+  case PI:
+    if (!e1->kids[1]->defeq(e2->kids[1]))
+      return false;
+    last++;
+    // fall through to LAM case
+  case LAM: {
+
+    /* It is critical that we point e1's var. (v1) back to e2's (call
+       it v2).  The reason this is critical is that we assume any
+       holes are in e1.  So we could end up with (_ v1) = t. We wish
+       to fill _ in this case with (\ v2 t).  If v2 pointed to v1, we
+       could not return (\ v1 t), because the fact that v2 points to
+       v1 would then be lost.
+    */
+    SymExpr *v1 = (SymExpr *)e1->kids[0];
+    Expr *prev_v1_val = v1->val;
+    v1->val = e2->kids[0]->followDefs();
+    bool bodies_equal = e1->kids[last]->defeq(e2->kids[last]);
+    v1->val = prev_v1_val;
+    return bodies_equal;
+  }
+  case APP: 
+#ifndef USE_FLAT_APP
+    return (e1->kids[0]->defeq(e2->kids[0]) &&
+	    e1->kids[1]->defeq(e2->kids[1]));
+#else
+    {
+      int counter = 0;
+      while( e1->kids[counter] ){
+         if( !e2->kids[counter] || !e1->kids[counter]->defeq( e2->kids[counter] ) )
+            return false;
+         counter++;
+      }
+      return e2->kids[counter]==NULL;
+    }
+#endif
+  case TYPE:
+  case KIND:
+  case MPZ:
+    // already checked that both exprs have the same opclass.
+    return true;
+  } // switch(op1)
+  
+  return false; // never reached.
+}
+
+int Expr::fiCounter = 0;
+
+bool Expr::free_in(Expr *x) {
+   //fiCounter++;
+   //if( fiCounter%1==0 )
+   //   std::cout << fiCounter << std::endl;
+   switch(getop()) {
+   case NOT_CEXPR:
+      switch (getclass()) {
+      case HOLE_EXPR: {
+         HoleExpr *h = (HoleExpr *)this;
+         if (h->val)
+	         return h->val->free_in(x);
+         return (h == x);
+      }
+      case SYMS_EXPR: 
+      case SYM_EXPR: {
+         SymExpr *s = (SymExpr *)this;
+         if (s->val && s->val->getclass() == HOLE_EXPR)
+	   /* we do not need to follow the "val" pointer except in this
+	      one case, when x is a hole (which we do not bother to check
+	      here) */
+	         return s->val->free_in(x);
+         return (s == x);
+      }
+      case INT_EXPR:
+         return false;
+      }
+      break;
+   case LAM:
+   case PI:
+      if (x == ((CExpr *)this)->kids[0])
+         return false;
+      // fall through
+   default: {
+      // must be a CExpr
+      CExpr *e = (CExpr *)this;
+      Expr *tmp;
+      Expr **cur = e->kids;
+      while ((tmp = *cur++))
+         if (tmp->free_in(x))
+	         return true;
+      return false;
+   }
+   }
+   return false; // should not be reached
+}
+
+void Expr::calc_free_in(){
+   data &= ~256;
+   data |= 256*((CExpr *)this)->kids[2]->free_in( ((CExpr *)this)->kids[0] );
+}
+
+string Expr::toString() {
+  ostringstream oss;
+  print(oss);
+  return oss.str();
+}
+
+static void print_kids(ostream &os, Expr **kids) {
+  Expr *tmp;
+  while ((tmp = *kids++)) {
+    os << " ";
+    tmp->print(os);
+  }
+}
+
+static void print_vector(ostream &os, const vector<Expr *> &v) {
+  for(int i = 0, iend = v.size(); i < iend; i++) {
+    os << " ";
+    v[i]->print(os);
+  }
+}
+
+void Expr::print(ostream &os) {
+  CExpr *e = (CExpr *)this; // for CEXPR cases
+
+  //std::cout << e->getop() << " ";
+  /*
+#ifdef DEBUG_REFCNT
+  os << "<";
+  char tmp[10];
+  sprintf(tmp,"%d",getrefcnt());
+  os << tmp << "> ";
+#endif
+*/
+
+  switch(getop()) {
+  case NOT_CEXPR: {
+    switch(getclass()) {
+    case INT_EXPR: 
+    {
+      IntExpr *e = (IntExpr *)this;
+      if (mpz_sgn(e->n) < 0) {
+	      os << "(~ ";
+	      mpz_t tmp;
+	      mpz_init(tmp);
+	      mpz_neg(tmp,e->n);
+	      char *s = mpz_get_str(0,10,tmp);
+	      os << s;
+	      free(s);
+	      mpz_clear(tmp);
+	      os << ")";
+        //os << "mpz";
+      }
+      else {
+	      char *s = mpz_get_str(0,10,e->n);
+	      os << s;
+	      free(s);
+        //os << "mpz";
+      }
+      break;
+    }
+    case RAT_EXPR: 
+    {
+      RatExpr *e = (RatExpr *)this;
+      char *s = mpq_get_str(0,10,e->n);
+      os << s;
+      if (mpq_sgn(e->n) < 0) {
+	      os << "(~ ";
+	      mpq_t tmp;
+	      mpq_init(tmp);
+	      mpq_neg(tmp,e->n);
+	      char *s = mpq_get_str(0,10,tmp);
+	      os << s;
+	      free(s);
+	      mpq_clear(tmp);
+	      os << ")";
+      }
+      else {
+	      char *s = mpq_get_str(0,10,e->n);
+	      os << s;
+	      free(s);
+      }
+      break;
+    }
+#ifndef DEBUG_SYM_NAMES
+    case SYM_EXPR: 
+    {
+      SymExpr *e = (SymExpr *)this;
+      if (e->val) {
+	      if (e->val->getop() == PROG) {
+	        os << e;
+#ifdef DEBUG_SYMS
+	        os << "[PROG]";
+#endif
+	      }else{
+#ifdef DEBUG_SYMS
+	        os << e;
+	        os << "[SYM ";
+#endif
+	        e->val->print(os);
+#ifdef DEBUG_SYMS
+	        os << "]";
+#endif
+        }
+      }
+      else
+	      os << e;
+      break;
+    }
+#else
+    case SYM_EXPR: /* if we are debugging sym names, then
+		      SYM_EXPRs are really SymSExprs. */
+#endif
+    case SYMS_EXPR: {
+      SymSExpr *e = (SymSExpr *)this;
+      if (e->val) {
+	      if (e->val->getop() == PROG) {
+	        os << e->s;
+#ifdef DEBUG_SYMS
+	        os << "[PROG]";
+#endif
+	      }else{
+#ifdef DEBUG_SYMS
+	        os << e->s;
+	        os << "[SYM ";
+#endif
+	        e->val->print(os);
+#ifdef DEBUG_SYMS
+	        os << "]";
+#endif
+	      }
+      }
+      else
+	      os << e->s;
+      break;
+    }
+    case HOLE_EXPR: 
+    {
+      HoleExpr *e = (HoleExpr *)this;
+      if (e->val) {
+#ifdef DEBUG_SYMS
+	      os << "_" << "[HOLE ";
+#endif
+	      e->val->print(os);
+#ifdef DEBUG_SYMS
+	      os << "]";
+#endif
+      }else {
+	      os << "_";
+#ifdef DEBUG_HOLE_NAMES
+	      char tmp[100];
+	      sprintf(tmp,"%d",e->id);
+	      os << "[ " << tmp << "]";
+#else
+	      os << "[ " << e << "]";
+#endif
+      }
+      break;
+    }
+    default:
+      os << "; unrecognized form of expr";
+      break;
+    }
+    break;
+  } // case NOT_CEXPR
+  case APP: {
+    os << "(";
+    vector<Expr *> args;
+    Expr *head = collect_args(args, false /* follow_defs */);
+    head->print(os);
+    print_vector(os, args);
+    os << ")";
+    break;
+  }
+  case LAM: 
+    os << "(\\";
+    print_kids(os, e->kids);
+    os << ")";
+    break;
+  case PI: 
+    os << "(!";
+    print_kids(os, e->kids);
+    os << ")";
+    break;
+  case TYPE: 
+    os << "type";
+    break;
+  case KIND: 
+    os << "kind";
+    break;
+  case MPZ: 
+    os << "mpz";
+    break;
+  case MPQ:
+    os << "mpq";
+    break;
+  case ADD: 
+    os << "(mp_add";  
+    print_kids(os,e->kids);
+    os << ")";
+    break;
+  case MUL:
+    os << "(mp_mul";  
+    print_kids(os,e->kids);
+    os << ")";
+    break;
+  case DIV:
+    os << "(mp_div";  
+    print_kids(os,e->kids);
+    os << ")";
+    break;
+  case NEG: 
+    os << "(mp_neg";
+    print_kids(os,e->kids);
+    os << ")";
+    break;
+  case IFNEG:
+    os << "(ifneg";
+    print_kids(os,e->kids);
+    os << ")";
+    break;
+  case IFZERO:
+    os << "(ifzero";
+    print_kids(os,e->kids);
+    os << ")";
+    break;
+  case RUN: 
+    os << "(run";
+    print_kids(os,e->kids);
+    os << ")";
+    break;
+  case PROG: 
+    os << "(prog";
+    print_kids(os,e->kids);
+    os << ")";
+    break;
+  case PROGVARS: 
+    os << "(";
+    print_kids(os,e->kids);
+    os << ")";
+    break;
+  case MATCH: 
+    os << "(match";
+    print_kids(os,e->kids);
+    os << ")";
+    break;
+  case CASE: 
+    os << "(";
+    print_kids(os,e->kids);
+    os << ")";
+    break;
+  case LET: 
+    os << "(let";
+    print_kids(os,e->kids);
+    os << ")";
+    break;
+  case DO: 
+    os << "(do";
+    print_kids(os,e->kids);
+    os << ")";
+    break;
+  case IFMARKED: 
+    os << "(ifmarked";
+    print_kids(os,e->kids);
+    os << ")";
+    break;
+  case COMPARE:
+    os << "(compare";
+    print_kids(os,e->kids);
+    os << ")";
+    break;
+  case MARKVAR: 
+    os << "(markvar";
+    print_kids(os,e->kids);
+    os << ")";
+    break;
+  case FAIL: 
+    os << "(fail ";
+    print_kids(os, e->kids);
+    os << ")";
+    break;
+  case ASCRIBE: 
+    os << "(:";
+    print_kids(os, e->kids);
+    os << ")";
+    break;
+  default:
+    os << "; unrecognized form of expr(2) " << getop() << " " << getclass();
+  } // switch(getop())
+}
+
+bool Expr::isType( Expr* statType ){
+  Expr* typ = this;
+  while( typ!=statType ){
+    if( typ->getop()==PI ){
+      typ = ((CExpr*)typ)->kids[2];
+    }else{
+      return false;
+    }
+  }
+  return true;
+}
+
+int SymExpr::symmCount = 0;
+#ifdef MARKVAR_32
+int SymExpr::mark()
+{
+  if( mark_map.find( this )== mark_map.end() )
+  {
+    symmCount++;
+    mark_map[this] = 0;
+  }
+  return mark_map[this];
+}
+void SymExpr::smark( int m )
+{
+  mark_map[this] = m;
+}
+#endif
\ No newline at end of file
diff --git a/proofs/lfsc_checker/expr.h b/proofs/lfsc_checker/expr.h
new file mode 100644
index 000000000..32a62ab33
--- /dev/null
+++ b/proofs/lfsc_checker/expr.h
@@ -0,0 +1,367 @@
+#ifndef sc2__expr_h
+#define sc2__expr_h
+
+#include "gmp.h"
+#include <string>
+#include <vector>
+#include <iostream>
+#include <map>
+#include "chunking_memory_management.h"
+
+#define USE_FLAT_APP
+#define MARKVAR_32
+#define DEBUG_SYM_NAMES
+//#define DEBUG_SYMS
+
+// Expr class
+enum { CEXPR = 0,
+       INT_EXPR,
+       RAT_EXPR,
+       HOLE_EXPR,
+       SYM_EXPR,
+       SYMS_EXPR };
+
+// operators for CExprs
+enum { NOT_CEXPR = 0, // for INT_EXPR, HOLE_EXPR, SYM_EXPR, SYMS_EXPR
+       APP,
+       PI,
+       LAM,
+       TYPE,
+       KIND,
+       ASCRIBE,
+       MPZ,
+       MPQ,
+
+       PROG,
+       PROGVARS,
+       MATCH,
+       CASE,
+       PAT,
+       DO,
+       ADD,
+       MUL,
+       DIV,
+       NEG,
+       IFNEG,
+       IFZERO,
+       LET,
+       RUN,
+       FAIL,
+       MARKVAR,
+       IFMARKED,
+       COMPARE
+};
+
+class SymExpr;
+
+class Expr {
+protected:
+  /* bits 0-2: Expr class
+     bits 3-7: operator 
+     bit 8: a flag for already cloned, free_in calculation
+     bits 9-31: ref count*/
+  int data;
+
+  void destroy(bool dec_kids);
+
+  enum { INC, DEC, CREATE };
+  void debugrefcnt(int ref, int what) {
+#ifdef DEBUG_REFCNT
+    std::cout << "[";
+    debug();
+    switch(what) {
+    case INC:
+      std::cout << " inc to ";
+      break;
+    case DEC:
+      std::cout << " dec to ";
+      break;
+    case CREATE:
+      std::cout << " creating]\n";
+      return;
+    }
+    char tmp[10];
+    sprintf(tmp,"%d",ref);
+    std::cout << tmp << "]\n";
+#else
+    (void)ref;
+    (void)what;
+#endif
+  }
+
+  Expr(int _class, int _op)
+    : data(1 << 9 /* refcount 1, not cloned */| (_op << 3) | _class)
+  { }
+
+public:
+  static int markedCount;
+  inline Expr* followDefs();
+  inline int getclass() const { return data & 7; }
+  int getexmark() const { return data & 256; }
+  void setexmark() { data |= 256; }
+  void clearexmark() { data &= ~256; }
+  inline int getop() const { return (data >> 3) & 31; }
+  int cloned() const { return data & 256; }
+  void setcloned() { data |= 256; }
+
+  inline int getrefcnt() { return data >> 9; }
+  inline void inc() {
+    int ref = getrefcnt();
+    //static int iCounter = 0;
+    //iCounter++;
+    //if( iCounter%10000==0 ){
+    //   //print( std::cout );
+    //   std::cout << " " << ref << std::endl;
+    //}
+    ref = ref<4194303 ? ref + 1 : ref;
+    debugrefcnt(ref,INC);
+    data = (ref << 9) | (data & 511);
+  }
+  static void destroy(Expr *, bool);
+  inline void dec(bool dec_kids = true) {
+    int ref = getrefcnt();
+    ref = ref - 1;
+    debugrefcnt(ref,DEC);
+    if (ref == 0)
+      destroy(this,dec_kids);
+    else
+      data = (ref << 9) | (data & 511);
+  }
+
+  //must pass statType (the expr representing "type") to this function
+  bool isType( Expr* statType );
+
+  inline bool isDatatype() {
+    return getclass() == SYMS_EXPR || getop() == MPZ || getop() == MPQ;
+  }
+  inline bool isArithTerm() {
+    return getop() == ADD || getop() == NEG;
+  }
+
+  static Expr *build_app(Expr *hd, const std::vector<Expr *> &args, 
+			 int start = 0);
+
+  static Expr *make_app(Expr* e1, Expr* e2 );
+
+  /* if this is an APP, return the head, and store the args in args.
+     If follow_defs is true, we proceed through defined heads;
+     otherwise not. */
+  Expr *collect_args(std::vector<Expr *> &args, bool follow_defs = true);
+
+  Expr *get_head(bool follow_defs = true);
+
+  Expr *get_body(int op = PI, bool follow_defs = true);
+
+  std::string toString();
+
+  void print(std::ostream &);
+  void debug();
+
+  /* check whether or not this expr is alpha equivalent to e.  If this
+     expr contains unfilled holes, fill them as we go. We do not fill
+     holes in e.  We do not take responsibility for the reference to
+     this nor the reference to e. */
+  bool defeq(Expr *e);
+
+  /* return a clone of this expr.  All abstractions are really duplicated
+     in memory.  Other expressions may not actually be duplicated in
+     memory, but their refcounts will be incremented. */
+  Expr *clone(); 
+
+  // x can be a SymExpr or a HoleExpr.
+  bool free_in(Expr *x);
+  bool get_free_in() { return data & 256; }
+  void calc_free_in();
+
+  static int cargCount;
+  static int fiCounter;
+};
+
+class CExpr : public Expr {
+public:
+  C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_H(CExpr,kids);
+
+  Expr **kids;
+  ~CExpr() {
+    delete[] kids;
+  }
+  CExpr(int _op) : Expr(CEXPR, _op), kids() {
+    kids = new Expr *[1];
+    kids[0] = 0;
+    debugrefcnt(1,CREATE);
+  }
+  CExpr(int _op, Expr *e1) : Expr(CEXPR, _op), kids() {
+    kids = new Expr *[2];
+    kids[0] = e1;
+    kids[1] = 0;
+    debugrefcnt(1,CREATE);
+  }
+  CExpr(int _op, Expr *e1, Expr *e2)
+    : Expr(CEXPR, _op), kids() {
+    kids = new Expr *[3];
+    kids[0] = e1;
+    kids[1] = e2;
+    kids[2] = 0;
+    debugrefcnt(1,CREATE);
+  }
+  CExpr(int _op, Expr *e1, Expr *e2, Expr *e3)
+    : Expr(CEXPR, _op), kids() {
+    kids = new Expr *[4];
+    kids[0] = e1;
+    kids[1] = e2;
+    kids[2] = e3;
+    kids[3] = 0;
+    debugrefcnt(1,CREATE);
+  }
+  CExpr(int _op, Expr *e1, Expr *e2, Expr *e3, Expr *e4)
+    : Expr(CEXPR, _op), kids() {
+    kids = new Expr *[5];
+    kids[0] = e1;
+    kids[1] = e2;
+    kids[2] = e3;
+    kids[3] = e4;
+    kids[4] = 0;
+    debugrefcnt(1,CREATE);
+  }
+  CExpr(int _op, const std::vector<Expr *> &_kids) 
+    : Expr(CEXPR, _op), kids() {
+    int i, iend = _kids.size();
+    kids = new Expr *[iend + 1];
+    for (i = 0; i < iend; i++)
+      kids[i] = _kids[i];
+    kids[i] = 0;
+    debugrefcnt(1,CREATE);
+  }
+
+  // _kids must be null-terminated.
+  CExpr(int _op, bool dummy, Expr **_kids) : Expr(CEXPR, _op), kids(_kids) {
+    (void)dummy;
+    debugrefcnt(1,CREATE);
+  }
+
+  Expr *whr();
+
+  static Expr* convert_to_tree_app( Expr* ce );
+  static Expr* convert_to_flat_app( Expr* ce );
+};
+
+class IntExpr : public Expr {
+ public:
+  mpz_t n;
+  ~IntExpr() {
+    mpz_clear(n);
+  }
+  IntExpr(mpz_t _n) : Expr(INT_EXPR, 0), n() {
+    mpz_init_set(n,_n);
+    debugrefcnt(1,CREATE);
+  }
+  IntExpr(signed long int _n ) : Expr(INT_EXPR, 0), n() {
+    mpz_init_set_si( n, _n );
+  }
+
+  unsigned long int get_num() { return mpz_get_ui( n ); }
+};
+
+class RatExpr : public Expr {
+ public:
+  mpq_t n;
+  ~RatExpr() {
+    mpq_clear(n);
+  }
+  RatExpr(mpq_t _n) : Expr(RAT_EXPR, 0), n() {
+    mpq_init( n );
+    mpq_set(n,_n);
+    debugrefcnt(1,CREATE);
+    mpq_canonicalize( n );
+  }
+  RatExpr(signed long int _n1, unsigned long int _n2 ) : Expr(RAT_EXPR, 0), n() {
+    mpq_init( n );
+    mpq_set_si( n, _n1, _n2 );
+    mpq_canonicalize( n );
+  }
+};
+
+class SymExpr : public Expr {
+ public:
+  Expr *val; // may be set by beta-reduction and clone().
+  static int symmCount;
+
+  SymExpr(std::string _s, int theclass = SYM_EXPR) 
+    : Expr(theclass, 0), val(0)
+  {   
+    (void)_s;
+    if (theclass == SYM_EXPR)
+      debugrefcnt(1,CREATE);
+  }
+  SymExpr(const SymExpr &e, int theclass = SYM_EXPR) 
+    : Expr(theclass, 0), val(0)
+  {
+    (void)e;
+    if (theclass == SYM_EXPR)
+      debugrefcnt(1,CREATE);
+  }
+#ifdef MARKVAR_32
+private:
+  int mark();
+  void smark( int m );
+public:
+  int getmark( int i = 0 ) { return (mark() >> i)&1; }
+  void setmark( int i = 0 ) { smark( mark() | (1 << i) ); }
+  void clearmark( int i = 0 ) { smark( mark() & ~(1 << i) ); }
+#endif
+};
+
+class SymSExpr : public SymExpr {
+ public:
+  std::string s;
+  SymSExpr(std::string _s, int theclass = SYMS_EXPR) 
+    : SymExpr(_s, theclass), s(_s)
+  {
+    debugrefcnt(1,CREATE);
+  }
+  SymSExpr(const SymSExpr &e, int theclass = SYMS_EXPR) 
+    : SymExpr(e, theclass), s(e.s)
+  { 
+    debugrefcnt(1,CREATE);
+  }
+};
+
+class HoleExpr : public Expr {
+  static int next_id;
+public:
+#ifdef DEBUG_HOLE_NAMES
+  int id;
+#endif
+  HoleExpr() 
+    : Expr(HOLE_EXPR, 0), val(0) 
+  {
+#ifdef DEBUG_HOLE_NAMES
+    id = next_id++;
+#endif
+    debugrefcnt(1,CREATE);
+  }
+  Expr *val; // may be set during subst(), defeq(), and clone().
+};
+
+inline Expr * Expr::followDefs() {
+  switch(getclass()) {
+  case HOLE_EXPR: {
+    HoleExpr *h = (HoleExpr *)this;
+    if (h->val)
+      return h->val->followDefs();
+    break;
+  }
+  case SYMS_EXPR: 
+  case SYM_EXPR: {
+    SymExpr *h = (SymExpr *)this;
+    if (h->val)
+      return h->val->followDefs();
+    break;
+  }
+  }
+
+  return this;
+}
+
+#endif
+
diff --git a/proofs/lfsc_checker/libwriter.cpp b/proofs/lfsc_checker/libwriter.cpp
new file mode 100644
index 000000000..49e9bbaad
--- /dev/null
+++ b/proofs/lfsc_checker/libwriter.cpp
@@ -0,0 +1,238 @@
+#include "libwriter.h"

+#include <sstream>

+#include <algorithm>

+#include <fstream>

+

+void libwriter::get_var_name( const std::string& n, std::string& nn ) {

+  nn = std::string( n.c_str() );

+  for( int i = 0; i <(int)n.length(); i++ ){

+    char c = n[i];

+    if (c <= 47)

+        c += 65;

+    else if (c >= 58 && c <= 64)

+        c += 97-58;

+    if ((c >= 91 && c <= 94) || c == 96)

+        c += 104-91;

+    else if (c >= 123)

+        c -= 4;

+    nn[i] = c;

+  }  

+}

+

+void libwriter::write_file()

+{

+  //std::cout << "write lib" << std::endl;

+  std::ostringstream os_enum;

+  std::ostringstream os_print;

+  std::ostringstream os_constructor_h;

+  std::ostringstream os_constructor_c;

+

+  for ( int a=0; a<(int)syms.size(); a++ ) {

+    //std::cout << "sym #" << (a+1) << ": ";

+    //std::cout << ((SymSExpr*)syms[a])->s.c_str() << std::endl;

+    //defs[a]->print( std::cout );

+    //std::cout << std::endl;

+    

+    if( defs[a]->getclass()==CEXPR ){

+      //calculate which arguments are required for input

+      std::vector< Expr* > args;

+      std::vector< bool > argsNeed;

+      std::vector< Expr* > argTypes;

+      CExpr* c = ((CExpr*)defs[a]);

+      while( c->getop()==PI ){

+        //std::cout << c->kids[0] << std::endl;

+        if( ((CExpr*)c->kids[1])->getop()!=RUN ){

+          args.push_back( c->kids[0] );

+          argsNeed.push_back( true );

+          argTypes.push_back( c->kids[1] );

+        }

+        for( int b=0; b<(int)args.size(); b++ ){

+          if( argsNeed[b] ){

+            if( ((CExpr*)c->kids[1])->getop()==RUN ){

+              if( ((CExpr*)c->kids[1])->kids[1]->free_in( args[b] ) ){

+                argsNeed[b] = false;

+              }

+            }else{

+              if( c->kids[1]->free_in( args[b] ) ){

+                argsNeed[b] = false;

+              }

+            }

+          }

+        }

+        c = (CExpr*)(c->kids[2]);

+      }

+

+      //record if this declares a judgement

+      if( ((CExpr*)defs[a])->getop()==PI && c->getop()==TYPE ){

+        //std::cout << "This is a judgement" << std::endl;

+        judgements.push_back( syms[a] );

+      //record if this declares a proof rule

+      }else if( c->getclass()==CEXPR && std::find( judgements.begin(), judgements.end(), c->kids[0] )!=judgements.end() ){

+        std::cout << "Handle rule: " << ((SymSExpr*)syms[a])->s.c_str() << std::endl;

+        //std::cout << "These are required to input:" << std::endl;

+        //for( int b=0; b<(int)args.size(); b++ ){

+        //  if( argsNeed[b] ){

+        //    std::cout << ((SymSExpr*)args[b])->s.c_str() << std::endl;

+        //  }

+        //}

+        os_enum << "    rule_" << ((SymSExpr*)syms[a])->s.c_str() << "," << std::endl;

+

+        os_print << "  case rule_" << ((SymSExpr*)syms[a])->s.c_str() << ": os << \"";

+        os_print << ((SymSExpr*)syms[a])->s.c_str() << "\";break;" << std::endl;

+

+        std::ostringstream os_args;

+        os_args << "(";

+        bool firstTime = true;

+        for( int b=0; b<(int)args.size(); b++ ){

+          if( argsNeed[b] ){

+            if( !firstTime )

+              os_args << ",";

+            std::string str;

+            get_var_name( ((SymSExpr*)args[b])->s, str );

+            os_args << " LFSCProof* " << str.c_str();

+            firstTime = false;

+          }

+        }

+        if( !firstTime ){

+          os_args << " ";

+        }

+        os_args << ")";

+

+        os_constructor_h << "  static LFSCProof* make_" << ((SymSExpr*)syms[a])->s.c_str();

+        os_constructor_h << os_args.str().c_str() << ";" << std::endl;

+

+        os_constructor_c << "LFSCProof* LFSCProof::make_" << ((SymSExpr*)syms[a])->s.c_str();

+        os_constructor_c << os_args.str().c_str() << "{" << std::endl;

+        os_constructor_c << "  LFSCProof **kids = new LFSCProof *[" << (int)args.size()+1 << "];" << std::endl;

+        for( int b=0; b<(int)args.size(); b++ ){

+          os_constructor_c << "  kids[" << b << "] = ";

+          if( argsNeed[b] ){

+            std::string str;

+            get_var_name( ((SymSExpr*)args[b])->s, str );

+            os_constructor_c << str.c_str();

+          }else{

+            os_constructor_c << "hole";

+          }

+          os_constructor_c << ";" << std::endl;

+        }

+        os_constructor_c << "  kids[" << (int)args.size() << "] = 0;" << std::endl;

+        os_constructor_c << "  return new LFSCProofC( rule_" << ((SymSExpr*)syms[a])->s.c_str() << ", kids );" << std::endl;

+        os_constructor_c << "}" << std::endl << std::endl;

+      }

+    }

+

+    //write the header

+    static std::string filename( "lfsc_proof" );

+    std::fstream fsh;

+    std::string fnameh( filename );

+    fnameh.append(".h");

+    fsh.open( fnameh.c_str(), std::ios::out );

+

+    fsh << "#ifndef LFSC_PROOF_LIB_H" << std::endl;

+    fsh << "#define LFSC_PROOF_LIB_H" << std::endl;

+    fsh << std::endl;

+    fsh << "#include <string>" << std::endl;

+    fsh << std::endl;

+    fsh << "class LFSCProof{" << std::endl;

+    fsh << "protected:" << std::endl;

+    fsh << "  enum{" << std::endl;

+    fsh << os_enum.str().c_str();

+    fsh << "  };" << std::endl;

+    fsh << "  static LFSCProof* hole;" << std::endl;

+    fsh << "  LFSCProof(){}" << std::endl;

+    fsh << "public:" << std::endl;

+    fsh << "  virtual ~LFSCProof(){}" << std::endl;

+    fsh << "  static void init();" << std::endl;

+    fsh << std::endl;

+    fsh << "  //functions to build LFSC proofs" << std::endl;

+    fsh << os_constructor_h.str().c_str();

+    fsh << std::endl;

+    fsh << "  virtual void set_child( int i, LFSCProof* e ) {}" << std::endl;

+    fsh << "  virtual void print( std::ostream& os ){}" << std::endl;

+    fsh << "};" << std::endl;

+    fsh << std::endl;

+    fsh << "class LFSCProofC : public LFSCProof{" << std::endl;

+    fsh << "  short id;" << std::endl;

+    fsh << "  LFSCProof **kids;" << std::endl;

+    fsh << "public:" << std::endl;

+    fsh << "  LFSCProofC( short d_id, LFSCProof **d_kids ) : id( d_id ), kids( d_kids ){}" << std::endl;

+    fsh << "  void set_child( int i, LFSCProof* e ) { kids[i] = e; }" << std::endl;

+    fsh << "  void print( std::ostream& os );" << std::endl;

+    fsh << "};" << std::endl;

+    fsh << std::endl;

+    fsh << "class LFSCProofSym : public LFSCProof{" << std::endl;

+    fsh << "private:" << std::endl;

+    fsh << "  std::string s;" << std::endl;

+    fsh << "  LFSCProofSym( std::string ss ) : s( ss ){}" << std::endl;

+    fsh << "public:" << std::endl;

+    fsh << "  static LFSCProofSym* make( std::string ss ) { return new LFSCProofSym( ss ); }" << std::endl;

+    fsh << "  static LFSCProofSym* make( const char* ss ) { return new LFSCProofSym( std::string( ss ) ); }" << std::endl;

+    fsh << "  ~LFSCProofSym(){}" << std::endl;

+    fsh << "  void print( std::ostream& os ) { os << s.c_str(); }" << std::endl;

+    fsh << "};" << std::endl;

+    fsh << std::endl;

+    fsh << "class LFSCProofLam : public LFSCProof{" << std::endl;

+    fsh << "  LFSCProofSym* var;" << std::endl;

+    fsh << "  LFSCProof* body;" << std::endl;

+    fsh << "  LFSCProof* typ;" << std::endl;

+    fsh << "  LFSCProofLam( LFSCProofSym* d_var, LFSCProof* d_body, LFSCProof* d_typ ) : var( d_var ), body( d_body ), typ( d_typ ){}" << std::endl;

+    fsh << "public:" << std::endl;

+    fsh << "  static LFSCProof* make( LFSCProofSym* d_var, LFSCProof* d_body, LFSCProof* d_typ = NULL ) {" << std::endl;

+    fsh << "    return new LFSCProofLam( d_var, d_body, d_typ );" << std::endl;

+    fsh << "  }" << std::endl;

+    fsh << "  ~LFSCProofLam(){}" << std::endl;

+    fsh << std::endl;

+    fsh << "  void print( std::ostream& os );" << std::endl;

+    fsh << "};" << std::endl;

+    fsh << std::endl;

+    fsh << "#endif" << std::endl;

+

+    //write the cpp

+    std::fstream fsc;

+    std::string fnamec( filename );

+    fnamec.append(".cpp");

+    fsc.open( fnamec.c_str(), std::ios::out );

+

+    fsc << "#include \"lfsc_proof.h\"" << std::endl;

+    fsc << std::endl;

+    fsc << "LFSCProof* LFSCProof::hole = NULL;" << std::endl;

+    fsc << std::endl;

+    fsc << "void LFSCProof::init(){" << std::endl;

+    fsc << "  hole = LFSCProofSym::make( \"_\" );" << std::endl;

+    fsc << "}" << std::endl;

+    fsc << std::endl;

+    fsc << "void LFSCProofC::print( std::ostream& os ){" << std::endl;

+    fsc << "  os << \"(\";" << std::endl;

+    fsc << "  switch( id ){" << std::endl;

+    fsc << os_print.str().c_str();

+    fsc << "  }" << std::endl;

+    fsc << "  int counter = 0;" << std::endl;

+    fsc << "  while( kids[counter] ){" << std::endl;

+    fsc << "    os << \" \";" << std::endl;

+    fsc << "    kids[counter]->print( os );" << std::endl;

+    fsc << "    counter++;" << std::endl;

+    fsc << "  }" << std::endl;

+    fsc << "  os << \")\";" << std::endl;

+    fsc << "}" << std::endl;

+    fsc << std::endl;

+    fsc << "void LFSCProofLam::print( std::ostream& os ){" << std::endl;

+    fsc << "  os << \"(\";" << std::endl;

+    fsc << "  if( typ ){" << std::endl;

+    fsc << "    os << \"% \";" << std::endl;

+    fsc << "  }else{" << std::endl;

+    fsc << "    os << \"\\\\ \";" << std::endl;

+    fsc << "  }" << std::endl;

+    fsc << "  var->print( os );" << std::endl;

+    fsc << "  if( typ ){" << std::endl;

+    fsc << "    os << \" \";" << std::endl;

+    fsc << "    typ->print( os );" << std::endl;

+    fsc << "  }" << std::endl;

+    fsc << "  os << std::endl;" << std::endl;

+    fsc << "  body->print( os );" << std::endl;

+    fsc << "  os << \")\";" << std::endl;

+    fsc << "}" << std::endl;

+    fsc << std::endl;

+    fsc << os_constructor_c.str().c_str();

+    fsc << std::endl;

+  }

+}

diff --git a/proofs/lfsc_checker/libwriter.h b/proofs/lfsc_checker/libwriter.h
new file mode 100644
index 000000000..093cf541b
--- /dev/null
+++ b/proofs/lfsc_checker/libwriter.h
@@ -0,0 +1,28 @@
+#ifndef LIB_WRITER_H

+#define LIB_WRITER_H

+

+#include "expr.h"

+#include <map>

+

+class libwriter

+{

+private:

+  std::vector< Expr* > syms;

+  std::vector< Expr* > defs;

+

+  std::vector< Expr* > judgements;

+  //get the variable name

+  void get_var_name( const std::string& n, std::string& nn );

+public:

+  libwriter(){}

+  virtual ~libwriter(){}

+

+  void add_symbol( Expr* s, Expr* t ) { 

+    syms.push_back( s );

+    defs.push_back( t ); 

+  }

+

+  void write_file();

+};

+

+#endif

diff --git a/proofs/lfsc_checker/main.cpp b/proofs/lfsc_checker/main.cpp
new file mode 100644
index 000000000..80f36e69f
--- /dev/null
+++ b/proofs/lfsc_checker/main.cpp
@@ -0,0 +1,139 @@
+#include "expr.h"
+#include "check.h"
+#include <signal.h>
+#include "sccwriter.h"
+#include "libwriter.h"
+#include <time.h>
+
+using namespace std;
+
+args a;
+
+static void parse_args(int argc, char **argv, args &a)
+{
+  char *arg0 = *argv;
+
+  /* skip 0'th argument */
+  argv++;
+  argc--;
+
+  while (argc) {
+
+    if ((strncmp("-h", *argv, 2) == 0) || 
+	(strncmp("--h", *argv, 3) == 0)) {
+      cout << "Usage: " << arg0 << " [options] infile1 ...infile_n\n";
+      cout << "If no infiles are named on the command line, input is read\n"
+	   << "from stdin.  Specifying the infile \"stdin\" will also read\n"
+	   << "from stdin.  Options are:\n\n";
+      cout << "--show-runs: print debugging information for runs of side condition code\n"; 
+      cout << "--compile-scc: compile side condition code\n"; 
+      cout << "--compile-scc-debug: compile debug versions of side condition code\n"; 
+      cout << "--run-scc: use compiled side condition code\n"; 
+      exit(0);
+    }	  
+    else if(strcmp("--show-runs", *argv) == 0) {
+      argc--; argv++;
+      a.show_runs = true;
+    }
+    else if(strcmp("--no-tail-calls", *argv) == 0) {
+      // this is just for debugging.
+      argc--; argv++;
+      a.no_tail_calls = true;
+    }
+    else if( strcmp("--compile-scc", *argv) == 0 ){
+      argc--; argv++;
+      a.compile_scc = true;
+      a.compile_scc_debug = false;
+    }
+    else if( strcmp("--compile-scc-debug", *argv) == 0 )
+    {
+       argc--; argv++;
+       a.compile_scc = true;
+       a.compile_scc_debug = true;
+    }
+    else if( strcmp("--compile-lib", *argv) == 0 )
+    {
+       argc--; argv++;
+       a.compile_lib = true;
+    }
+    else if( strcmp("--run-scc", *argv) == 0 ){
+      argc--; argv++;
+      a.run_scc = true;
+    }
+    else if( strcmp("--use-nested-app", *argv) == 0 ){
+      argc--; argv++;
+      a.use_nested_app = true;    //not implemented yet
+    }else {
+      a.files.push_back(*argv);
+      argc--; argv++;
+    }
+  }
+}
+
+void sighandler(int /* signum */) {
+  cerr << "\nInterrupted.  sc is aborting.\n";
+  exit(1);
+}
+
+int main(int argc, char **argv) {
+
+  a.show_runs = false;
+  a.no_tail_calls = false;
+  a.compile_scc = false;
+  a.run_scc = false;
+  a.use_nested_app = false;
+
+  signal(SIGINT, sighandler);
+
+  parse_args(argc, argv, a);
+
+  init();
+
+  check_time = (int)clock();
+
+  if (a.files.size()) {
+    sccwriter* scw = NULL;
+    libwriter* lw = NULL;
+    if( a.compile_scc ){
+       scw = new sccwriter( a.compile_scc_debug ? opt_write_call_debug : 0 );
+    }
+    if( a.compile_lib ){
+       lw = new libwriter;
+    }
+    /* process the files named */
+    int i = 0, iend = a.files.size();
+    for (; i < iend; i++) {
+      const char *filename = a.files[i].c_str();
+      check_file(filename, a, scw, lw);
+    }
+    if( scw ){
+      scw->write_file();
+      delete scw;
+    }
+    if( lw ){
+#ifdef DEBUG_SYM_NAMES
+      lw->write_file();
+      delete lw;
+#else
+      std::cout << "ERROR libwriter: Must compile LFSC with DEBUG_SYM_NAMES flag (see Expr.h)" << std::endl;
+#endif
+    }
+  }
+  else 
+    check_file("stdin", a);
+
+  //std::cout << "time = " << (int)clock() - t << std::endl;
+  //while(1){}
+
+#ifdef DEBUG
+  cout << "Clearing globals.\n";
+  cout.flush(); 
+
+  cleanup();
+  a.files.clear();
+#endif
+
+  std::cout << "time = " << (int)clock() - check_time << std::endl;
+  std::cout << "sym count = " << SymExpr::symmCount << std::endl;
+  std::cout << "marked count = " << Expr::markedCount << std::endl;
+}
diff --git a/proofs/lfsc_checker/position.h b/proofs/lfsc_checker/position.h
new file mode 100644
index 000000000..a5c51ffc6
--- /dev/null
+++ b/proofs/lfsc_checker/position.h
@@ -0,0 +1,30 @@
+#ifndef sc2__position_h
+#define sc2__position_h
+
+#include <iostream>
+#include <stdio.h>
+
+class Position {
+public:
+  const char *filename;
+  int linenum; 
+  int colnum;
+
+  Position(const char *_f, int l, int c) : filename(_f), linenum(l), colnum(c)
+  {}
+  void print(std::ostream &os) {
+    os << filename;
+    if (colnum == -1) {
+      char tmp[1024];
+      sprintf(tmp, ", line %d, end of column: ", linenum);
+      os << tmp;
+    }
+    else {
+      char tmp[1024];
+      sprintf(tmp, ", line %d, column %d: ", linenum, colnum);
+      os << tmp;
+    }
+  }
+};
+
+#endif
diff --git a/proofs/lfsc_checker/print_smt2.cpp b/proofs/lfsc_checker/print_smt2.cpp
new file mode 100644
index 000000000..bf068c248
--- /dev/null
+++ b/proofs/lfsc_checker/print_smt2.cpp
@@ -0,0 +1,122 @@
+#include "print_smt2.h"

+

+#ifdef PRINT_SMT2

+

+void print_smt2( Expr* p, std::ostream& s, short mode )

+{

+  switch( p->getclass() )

+  {

+  case CEXPR:

+    {

+      switch( p->getop() )

+      {

+      case APP:

+        {

+          std::vector<Expr *> args;
+          Expr *head = p->collect_args(args, false);

+          short newMode = get_mode( head );

+          if( is_smt2_poly_formula( head ) )

+          {

+            s << "(";

+            head->print( s );

+            s << " ";

+            print_smt2( args[1], s, newMode );

+            s << " ";

+            print_smt2( args[2], s, newMode );

+            s << ")";

+          }

+          else if( ( mode==2 || mode==3 ) && mode==newMode )

+          {

+            print_smt2( args[0], s, newMode );

+            s << " ";

+            print_smt2( args[1], s, newMode );

+          }

+          else if( newMode==1 )

+          {

+            if( mode!=1 || newMode!=mode ){

+              s << "(";

+            }

+            print_smt2( args[2], s, newMode );

+            s << " ";

+            print_smt2( args[3], s, 0 );

+            if( mode!=1 || newMode!=mode ){

+              s << ")";

+            }

+          }

+          else

+          {

+            s << "(";

+            switch( newMode )

+            {

+            case 4: s << "=>";break;

+            default: head->print( s );break;

+            }

+            s << " ";

+            for( int a=0; a<(int)args.size(); a++ ){

+              print_smt2( args[a], s, newMode );

+              if( a!=args.size()-1 )

+                s << " ";

+            }

+            s << ")";

+          }

+        }

+        break;

+      default:

+        std::cout << "Unhandled op " << p->getop() << std::endl;

+        break;

+      }

+    }

+    break;

+  case HOLE_EXPR:

+    {

+      HoleExpr *e = (HoleExpr *)p;

+      if( e->val ){

+        print_smt2( e->val, s, mode );

+      }else{

+        s << "_";

+      }

+    }

+    break;

+  case SYMS_EXPR:

+  case SYM_EXPR:

+    if( ((SymExpr*)p)->val )

+      print_smt2( ((SymExpr*)p)->val, s, mode );

+    else

+      p->print( s );

+    break;

+  default:

+    std::cout << "Unhandled class " << p->getclass() << std::endl;

+    break;

+  }

+}

+

+bool is_smt2_poly_formula( Expr* e )

+{

+  if( e->getclass()==SYMS_EXPR )

+  {

+    SymSExpr* s = (SymSExpr*)e;

+    static std::string eq("=");

+    static std::string distinct("distinct");

+    return s->s==eq || s->s==distinct;

+  }else{

+    return false;

+  }

+}

+

+short get_mode( Expr* e )

+{

+  if( e->getclass()==SYMS_EXPR ){

+    SymSExpr* s = (SymSExpr*)e;

+    static std::string applys("apply");

+    if ( s->s==applys ) return 1;

+    static std::string ands("and");

+    if ( s->s==ands ) return 2;

+    static std::string ors("or");

+    if ( s->s==ors ) return 3;

+    static std::string impls("impl");

+    if ( s->s==impls ) return 4;

+  }

+  return 0;

+}

+

+#endif

diff --git a/proofs/lfsc_checker/print_smt2.h b/proofs/lfsc_checker/print_smt2.h
new file mode 100644
index 000000000..c70b1dfa4
--- /dev/null
+++ b/proofs/lfsc_checker/print_smt2.h
@@ -0,0 +1,17 @@
+#ifndef PRINT_SMT2_H

+#define PRINT_SMT2_H

+

+#define PRINT_SMT2

+

+#include "expr.h"

+

+#ifdef PRINT_SMT2

+void print_smt2( Expr* p, std::ostream& s, short mode = 0 );

+

+bool is_smt2_poly_formula( Expr* p );

+short get_mode( Expr* p );

+

+#endif

+

+

+#endif

diff --git a/proofs/lfsc_checker/scccode.cpp b/proofs/lfsc_checker/scccode.cpp
new file mode 100644
index 000000000..cff762a08
--- /dev/null
+++ b/proofs/lfsc_checker/scccode.cpp
@@ -0,0 +1,609 @@
+#include "scccode.h"
+
+Expr* e_pos;
+Expr* e_neg;
+Expr* e_tt;
+Expr* e_ff;
+Expr* e_cln;
+Expr* e_clc;
+Expr* e_concat;
+Expr* e_clr;
+Expr* e_litvar;
+Expr* e_litpol;
+Expr* e_notb;
+Expr* e_iffb;
+Expr* e_clear_mark;
+Expr* e_append;
+Expr* e_simplify_clause_h;
+Expr* e_simplify_clause;
+
+void init_compiled_scc(){
+   e_pos = symbols->get("pos").first;
+   e_neg = symbols->get("neg").first;
+   e_tt = symbols->get("tt").first;
+   e_ff = symbols->get("ff").first;
+   e_cln = symbols->get("cln").first;
+   e_clc = symbols->get("clc").first;
+   e_concat = symbols->get("concat").first;
+   e_clr = symbols->get("clr").first;
+   e_litvar = progs["litvar"];
+   e_litpol = progs["litpol"];
+   e_notb = progs["notb"];
+   e_iffb = progs["iffb"];
+   e_clear_mark = progs["clear_mark"];
+   e_append = progs["append"];
+   e_simplify_clause_h = progs["simplify_clause_h"];
+   e_simplify_clause = progs["simplify_clause"];
+}
+
+Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args ){
+   if( p==e_litvar ){
+      return f_litvar( args[0] );
+   }else if( p==e_litpol ){
+      return f_litpol( args[0] );
+   }else if( p==e_notb ){
+      return f_notb( args[0] );
+   }else if( p==e_iffb ){
+      return f_iffb( args[0], args[1] );
+   }else if( p==e_clear_mark ){
+      return f_clear_mark( args[0] );
+   }else if( p==e_append ){
+      return f_append( args[0], args[1] );
+   }else if( p==e_simplify_clause_h ){
+      return f_simplify_clause_h( args[0], args[1] );
+   }else if( p==e_simplify_clause ){
+      return f_simplify_clause( args[0] );
+   }else{
+      return NULL;
+   }
+}
+
+Expr* f_litvar( Expr* l ){
+   Expr* e0;
+   l->inc();
+   Expr* e1 = l->followDefs()->get_head();
+   Expr* e2;
+   e2 = e_pos;
+   e2->inc();
+   Expr* e3;
+   e3 = e_neg;
+   e3->inc();
+   if( e1==e2 ){
+      Expr* x = ((CExpr*)l->followDefs())->kids[1];
+      e0 = x;
+      e0->inc();
+   }else if( e1==e3 ){
+      Expr* x = ((CExpr*)l->followDefs())->kids[1];
+      e0 = x;
+      e0->inc();
+   }else{
+      std::cout << "Could not find match for expression in function f_litvar ";
+      e1->print( std::cout );
+      std::cout << std::endl;
+      exit( 1 );
+   }
+   l->dec();
+   e2->dec();
+   e3->dec();
+   return e0;
+}
+
+Expr* f_litpol( Expr* l ){
+   Expr* e0;
+   l->inc();
+   Expr* e1 = l->followDefs()->get_head();
+   Expr* e2;
+   e2 = e_pos;
+   e2->inc();
+   Expr* e3;
+   e3 = e_neg;
+   e3->inc();
+   if( e1==e2 ){
+      Expr* x = ((CExpr*)l->followDefs())->kids[1];
+      e0 = e_tt;
+      e0->inc();
+   }else if( e1==e3 ){
+      Expr* x = ((CExpr*)l->followDefs())->kids[1];
+      e0 = e_ff;
+      e0->inc();
+   }else{
+      std::cout << "Could not find match for expression in function f_litpol ";
+      e1->print( std::cout );
+      std::cout << std::endl;
+      exit( 1 );
+   }
+   l->dec();
+   e2->dec();
+   e3->dec();
+   return e0;
+}
+
+Expr* f_notb( Expr* b ){
+   Expr* e0;
+   b->inc();
+   Expr* e1 = b->followDefs()->get_head();
+   Expr* e2;
+   e2 = e_ff;
+   e2->inc();
+   Expr* e3;
+   e3 = e_tt;
+   e3->inc();
+   if( e1==e2 ){
+      e0 = e_tt;
+      e0->inc();
+   }else if( e1==e3 ){
+      e0 = e_ff;
+      e0->inc();
+   }else{
+      std::cout << "Could not find match for expression in function f_notb ";
+      e1->print( std::cout );
+      std::cout << std::endl;
+      exit( 1 );
+   }
+   b->dec();
+   e2->dec();
+   e3->dec();
+   return e0;
+}
+
+Expr* f_iffb( Expr* b1, Expr* b2 ){
+   Expr* e0;
+   b1->inc();
+   Expr* e1 = b1->followDefs()->get_head();
+   Expr* e2;
+   e2 = e_tt;
+   e2->inc();
+   Expr* e3;
+   e3 = e_ff;
+   e3->inc();
+   if( e1==e2 ){
+      e0 = b2;
+      e0->inc();
+   }else if( e1==e3 ){
+      b2->inc();
+      e0 = f_notb( b2 );
+      b2->dec();
+   }else{
+      std::cout << "Could not find match for expression in function f_iffb ";
+      e1->print( std::cout );
+      std::cout << std::endl;
+      exit( 1 );
+   }
+   b1->dec();
+   e2->dec();
+   e3->dec();
+   return e0;
+}
+
+Expr* f_clear_mark( Expr* v ){
+   Expr* e0;
+   v->inc();
+   if ( ((SymExpr*)v->followDefs())->getmark(0)){
+      v->inc();
+      if ( ((SymExpr*)v->followDefs())->getmark(0))
+         ((SymExpr*)v->followDefs())->clearmark(0);
+      else
+         ((SymExpr*)v->followDefs())->setmark(0);
+      e0 = v;
+      e0->inc();
+      v->dec();
+   }else{
+      e0 = v;
+      e0->inc();
+   }
+   v->dec();
+   return e0;
+}
+
+Expr* f_append( Expr* c1, Expr* c2 ){
+   Expr* e0;
+   c1->inc();
+   Expr* e1 = c1->followDefs()->get_head();
+   Expr* e2;
+   e2 = e_cln;
+   e2->inc();
+   Expr* e3;
+   e3 = e_clc;
+   e3->inc();
+   if( e1==e2 ){
+      e0 = c2;
+      e0->inc();
+   }else if( e1==e3 ){
+      Expr* l = ((CExpr*)c1->followDefs())->kids[1];
+      Expr* c1h = ((CExpr*)c1->followDefs())->kids[2];
+      l->inc();
+      Expr* e4;
+      c1h->inc();
+      c2->inc();
+      e4 = f_append( c1h, c2 );
+      c1h->dec();
+      c2->dec();
+      static Expr* e5;
+      e5 = e_clc;
+      e5->inc();
+      e0 = new CExpr( APP, e5, l, e4 );
+   }else{
+      std::cout << "Could not find match for expression in function f_append ";
+      e1->print( std::cout );
+      std::cout << std::endl;
+      exit( 1 );
+   }
+   c1->dec();
+   e2->dec();
+   e3->dec();
+   return e0;
+}
+
+Expr* f_simplify_clause_h( Expr* pol, Expr* c ){
+   Expr* e0;
+   c->inc();
+   Expr* e1 = c->followDefs()->get_head();
+   Expr* e2;
+   e2 = e_cln;
+   e2->inc();
+   Expr* e3;
+   e3 = e_clc;
+   e3->inc();
+   Expr* e4;
+   e4 = e_concat;
+   e4->inc();
+   Expr* e5;
+   e5 = e_clr;
+   e5->inc();
+   if( e1==e2 ){
+      e0 = e_cln;
+      e0->inc();
+   }else if( e1==e3 ){
+      Expr* l = ((CExpr*)c->followDefs())->kids[1];
+      Expr* c1 = ((CExpr*)c->followDefs())->kids[2];
+      Expr* v;
+      l->inc();
+      v = f_litvar( l );
+      l->dec();
+      Expr* e6;
+      Expr* e7;
+      l->inc();
+      e7 = f_litpol( l );
+      l->dec();
+      pol->inc();
+      e6 = f_iffb( e7, pol );
+      e7->dec();
+      pol->dec();
+      Expr* e8 = e6->followDefs()->get_head();
+      Expr* e9;
+      e9 = e_tt;
+      e9->inc();
+      Expr* e10;
+      e10 = e_ff;
+      e10->inc();
+      if( e8==e9 ){
+         Expr* m;
+         v->inc();
+         if ( ((SymExpr*)v->followDefs())->getmark(0)){
+            m = e_tt;
+            m->inc();
+         }else{
+            Expr* e11;
+            v->inc();
+            if ( ((SymExpr*)v->followDefs())->getmark(0))
+               ((SymExpr*)v->followDefs())->clearmark(0);
+            else
+               ((SymExpr*)v->followDefs())->setmark(0);
+            e11 = v;
+            e11->inc();
+            v->dec();
+            e11->dec();
+            m = e_ff;
+            m->inc();
+         }
+         v->dec();
+         Expr* ch;
+         pol->inc();
+         c1->inc();
+         ch = f_simplify_clause_h( pol, c1 );
+         pol->dec();
+         c1->dec();
+         m->inc();
+         Expr* e12 = m->followDefs()->get_head();
+         Expr* e13;
+         e13 = e_tt;
+         e13->inc();
+         Expr* e14;
+         e14 = e_ff;
+         e14->inc();
+         if( e12==e13 ){
+            Expr* e15;
+            v->inc();
+            if ( ((SymExpr*)v->followDefs())->getmark(1)){
+               e15 = v;
+               e15->inc();
+            }else{
+               v->inc();
+               if ( ((SymExpr*)v->followDefs())->getmark(1))
+                  ((SymExpr*)v->followDefs())->clearmark(1);
+               else
+                  ((SymExpr*)v->followDefs())->setmark(1);
+               e15 = v;
+               e15->inc();
+               v->dec();
+            }
+            v->dec();
+            e15->dec();
+            e0 = ch;
+            e0->inc();
+         }else if( e12==e14 ){
+            Expr* e16;
+            Expr* e17;
+            v->inc();
+            if ( ((SymExpr*)v->followDefs())->getmark(1)){
+               v->inc();
+               if ( ((SymExpr*)v->followDefs())->getmark(1))
+                  ((SymExpr*)v->followDefs())->clearmark(1);
+               else
+                  ((SymExpr*)v->followDefs())->setmark(1);
+               e17 = v;
+               e17->inc();
+               v->dec();
+            }else{
+               e17 = v;
+               e17->inc();
+            }
+            v->dec();
+            e17->dec();
+            v->inc();
+            if ( ((SymExpr*)v->followDefs())->getmark(0))
+               ((SymExpr*)v->followDefs())->clearmark(0);
+            else
+               ((SymExpr*)v->followDefs())->setmark(0);
+            e16 = v;
+            e16->inc();
+            v->dec();
+            e16->dec();
+            l->inc();
+            ch->inc();
+            static Expr* e18;
+            e18 = e_clc;
+            e18->inc();
+            e0 = new CExpr( APP, e18, l, ch );
+         }else{
+            std::cout << "Could not find match for expression in function f_simplify_clause_h ";
+            e12->print( std::cout );
+            std::cout << std::endl;
+            exit( 1 );
+         }
+         m->dec();
+         e13->dec();
+         e14->dec();
+         ch->dec();
+         m->dec();
+      }else if( e8==e10 ){
+         l->inc();
+         Expr* e19;
+         pol->inc();
+         c1->inc();
+         e19 = f_simplify_clause_h( pol, c1 );
+         pol->dec();
+         c1->dec();
+         static Expr* e20;
+         e20 = e_clc;
+         e20->inc();
+         e0 = new CExpr( APP, e20, l, e19 );
+      }else{
+         std::cout << "Could not find match for expression in function f_simplify_clause_h ";
+         e8->print( std::cout );
+         std::cout << std::endl;
+         exit( 1 );
+      }
+      e6->dec();
+      e9->dec();
+      e10->dec();
+      v->dec();
+   }else if( e1==e4 ){
+      Expr* c1 = ((CExpr*)c->followDefs())->kids[1];
+      Expr* c2 = ((CExpr*)c->followDefs())->kids[2];
+      pol->inc();
+      Expr* e21 = pol->followDefs()->get_head();
+      Expr* e22;
+      e22 = e_ff;
+      e22->inc();
+      Expr* e23;
+      e23 = e_tt;
+      e23->inc();
+      if( e21==e22 ){
+         Expr* e24;
+         pol->inc();
+         c1->inc();
+         e24 = f_simplify_clause_h( pol, c1 );
+         pol->dec();
+         c1->dec();
+         Expr* e25;
+         pol->inc();
+         c2->inc();
+         e25 = f_simplify_clause_h( pol, c2 );
+         pol->dec();
+         c2->dec();
+         static Expr* e26;
+         e26 = e_concat;
+         e26->inc();
+         e0 = new CExpr( APP, e26, e24, e25 );
+      }else if( e21==e23 ){
+         Expr* e27;
+         pol->inc();
+         c1->inc();
+         e27 = f_simplify_clause_h( pol, c1 );
+         pol->dec();
+         c1->dec();
+         Expr* e28;
+         pol->inc();
+         c2->inc();
+         e28 = f_simplify_clause_h( pol, c2 );
+         pol->dec();
+         c2->dec();
+         e0 = f_append( e27, e28 );
+         e27->dec();
+         e28->dec();
+      }else{
+         std::cout << "Could not find match for expression in function f_simplify_clause_h ";
+         e21->print( std::cout );
+         std::cout << std::endl;
+         exit( 1 );
+      }
+      pol->dec();
+      e22->dec();
+      e23->dec();
+   }else if( e1==e5 ){
+      Expr* l = ((CExpr*)c->followDefs())->kids[1];
+      Expr* c1 = ((CExpr*)c->followDefs())->kids[2];
+      Expr* e29;
+      Expr* e30;
+      l->inc();
+      e30 = f_litpol( l );
+      l->dec();
+      pol->inc();
+      e29 = f_iffb( e30, pol );
+      e30->dec();
+      pol->dec();
+      Expr* e31 = e29->followDefs()->get_head();
+      Expr* e32;
+      e32 = e_ff;
+      e32->inc();
+      Expr* e33;
+      e33 = e_tt;
+      e33->inc();
+      if( e31==e32 ){
+         l->inc();
+         Expr* e34;
+         pol->inc();
+         c1->inc();
+         e34 = f_simplify_clause_h( pol, c1 );
+         pol->dec();
+         c1->dec();
+         static Expr* e35;
+         e35 = e_clr;
+         e35->inc();
+         e0 = new CExpr( APP, e35, l, e34 );
+      }else if( e31==e33 ){
+         Expr* v;
+         l->inc();
+         v = f_litvar( l );
+         l->dec();
+         Expr* m;
+         v->inc();
+         if ( ((SymExpr*)v->followDefs())->getmark(0)){
+            m = e_tt;
+            m->inc();
+         }else{
+            Expr* e36;
+            v->inc();
+            if ( ((SymExpr*)v->followDefs())->getmark(0))
+               ((SymExpr*)v->followDefs())->clearmark(0);
+            else
+               ((SymExpr*)v->followDefs())->setmark(0);
+            e36 = v;
+            e36->inc();
+            v->dec();
+            e36->dec();
+            m = e_ff;
+            m->inc();
+         }
+         v->dec();
+         Expr* ch;
+         pol->inc();
+         c1->inc();
+         ch = f_simplify_clause_h( pol, c1 );
+         pol->dec();
+         c1->dec();
+         v->inc();
+         if ( ((SymExpr*)v->followDefs())->getmark(1)){
+            m->inc();
+            Expr* e37 = m->followDefs()->get_head();
+            Expr* e38;
+            e38 = e_tt;
+            e38->inc();
+            Expr* e39;
+            e39 = e_ff;
+            e39->inc();
+            if( e37==e38 ){
+               e0 = ch;
+               e0->inc();
+            }else if( e37==e39 ){
+               Expr* e40;
+               Expr* e41;
+               v->inc();
+               if ( ((SymExpr*)v->followDefs())->getmark(1))
+                  ((SymExpr*)v->followDefs())->clearmark(1);
+               else
+                  ((SymExpr*)v->followDefs())->setmark(1);
+               e41 = v;
+               e41->inc();
+               v->dec();
+               e41->dec();
+               v->inc();
+               if ( ((SymExpr*)v->followDefs())->getmark(0))
+                  ((SymExpr*)v->followDefs())->clearmark(0);
+               else
+                  ((SymExpr*)v->followDefs())->setmark(0);
+               e40 = v;
+               e40->inc();
+               v->dec();
+               e40->dec();
+               e0 = ch;
+               e0->inc();
+            }else{
+               std::cout << "Could not find match for expression in function f_simplify_clause_h ";
+               e37->print( std::cout );
+               std::cout << std::endl;
+               exit( 1 );
+            }
+            m->dec();
+            e38->dec();
+            e39->dec();
+         }else{
+            e0 = NULL;
+         }
+         v->dec();
+         ch->dec();
+         m->dec();
+         v->dec();
+      }else{
+         std::cout << "Could not find match for expression in function f_simplify_clause_h ";
+         e31->print( std::cout );
+         std::cout << std::endl;
+         exit( 1 );
+      }
+      e29->dec();
+      e32->dec();
+      e33->dec();
+   }else{
+      std::cout << "Could not find match for expression in function f_simplify_clause_h ";
+      e1->print( std::cout );
+      std::cout << std::endl;
+      exit( 1 );
+   }
+   c->dec();
+   e2->dec();
+   e3->dec();
+   e4->dec();
+   e5->dec();
+   return e0;
+}
+
+Expr* f_simplify_clause( Expr* c ){
+   Expr* e0;
+   static Expr* e1;
+   e1 = e_tt;
+   e1->inc();
+   Expr* e2;
+   static Expr* e3;
+   e3 = e_ff;
+   e3->inc();
+   c->inc();
+   e2 = f_simplify_clause_h( e3, c );
+   e3->dec();
+   c->dec();
+   e0 = f_simplify_clause_h( e1, e2 );
+   e1->dec();
+   e2->dec();
+   return e0;
+}
+
diff --git a/proofs/lfsc_checker/scccode.h b/proofs/lfsc_checker/scccode.h
new file mode 100644
index 000000000..6f5efc8b5
--- /dev/null
+++ b/proofs/lfsc_checker/scccode.h
@@ -0,0 +1,27 @@
+#ifndef SCC_CODE_H
+#define SCC_CODE_H
+
+#include "check.h"
+
+void init_compiled_scc();
+
+Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args );
+
+inline Expr* f_litvar( Expr* l );
+
+inline Expr* f_litpol( Expr* l );
+
+inline Expr* f_notb( Expr* b );
+
+inline Expr* f_iffb( Expr* b1, Expr* b2 );
+
+inline Expr* f_clear_mark( Expr* v );
+
+inline Expr* f_append( Expr* c1, Expr* c2 );
+
+inline Expr* f_simplify_clause_h( Expr* pol, Expr* c );
+
+inline Expr* f_simplify_clause( Expr* c );
+
+#endif
+
diff --git a/proofs/lfsc_checker/sccwriter.cpp b/proofs/lfsc_checker/sccwriter.cpp
new file mode 100644
index 000000000..d11a96b19
--- /dev/null
+++ b/proofs/lfsc_checker/sccwriter.cpp
@@ -0,0 +1,977 @@
+#include "sccwriter.h"

+

+#include <fstream>

+#include <sstream>

+

+int sccwriter::exprCount = 0;

+int sccwriter::strCount = 0;

+int sccwriter::argsCount = 0;

+int sccwriter::rnumCount = 0;

+

+int sccwriter::get_prog_index( const std::string& str )

+{

+  for( int a=0; a<(int)progNames.size(); a++ ){

+    if( progNames[a]==str ){

+      return a;

+    }

+  }

+  return -1;

+}

+

+int sccwriter::get_prog_index_by_expr( Expr* e )

+{

+  for( int a=0; a<(int)progPtrs.size(); a++ ){

+    if( progPtrs[a]==e ){

+      return a;

+    }

+  }

+  return -1;

+}

+

+bool sccwriter::is_var( const std::string& str )

+{

+  for( int a=0; a<(int)vars.size(); a++ ){

+    if( vars[a]==str ){

+      return true;

+    }

+  }

+  return false;

+}

+

+void sccwriter::add_global_sym( const std::string& str )

+{

+  for( int a=0; a<(int)globalSyms.size(); a++ ){

+    if( globalSyms[a]==str ){

+      return;

+    }

+  }

+  globalSyms.push_back( str );

+}

+

+void sccwriter::indent( std::ostream& os, int ind )

+{

+   for( int a=0; a<ind; a++ )

+   {

+      os << "   ";

+   }

+}

+

+void sccwriter::write_function_header( std::ostream& os, int index, int opts )

+{

+  //write the function header

+  std::string fname;

+  get_function_name( progNames[index], fname );

+  os << "Expr* " << fname.c_str() << "( ";

+  CExpr* progvars = (CExpr*)get_prog( index )->kids[1];

+  int counter = 0;

+  //write each argument

+  while( progvars->kids[counter] )

+  {

+    if( counter!=0 )

+    {

+      os << ", ";

+    }

+    os << "Expr* ";

+    write_variable( ((SymSExpr*)progvars->kids[counter])->s, os );

+    //add to vars if options are set to do so

+    if( opts&opt_write_add_args )

+    {

+      vars.push_back( ((SymSExpr*)progvars->kids[counter])->s );

+    }

+    counter++;

+  }

+  os << " )";

+  if( opts&opt_write_call_debug )

+  {

+     os << "{" << std::endl;

+     indent( os, 1 );

+     os << "std::cout << \"Call function " << fname.c_str() << " with arguments \";" << std::endl;

+     counter = 0; 

+     while( progvars->kids[counter] )

+     {

+        if( counter!=0 )

+        {

+           indent( os, 1 );

+           os << "std::cout << \", \";" << std::endl;

+        }

+        indent( os, 1 );

+        write_variable( ((SymSExpr*)progvars->kids[counter])->s, os );

+        os << "->print( std::cout );" << std::endl;

+        counter++;

+     }

+     indent( os, 1 );

+     os << "std::cout << std::endl;" << std::endl;

+  }

+}

+

+void sccwriter::get_function_name( const std::string& pname, std::string& fname )

+{

+  fname = std::string( "f_" );

+  fname.append( pname );

+}

+

+void sccwriter::write_variable( const std::string& n, std::ostream& os )

+{

+  std::string nn;

+  get_var_name( n, nn );

+  os << nn.c_str();

+}

+

+void sccwriter::get_var_name( const std::string& n, std::string& nn ) {

+  nn = std::string( n.c_str() );

+  for( int i = 0; i <(int)n.length(); i++ ){

+    char c = n[i];

+    if (c <= 47)

+        c += 65;

+    else if (c >= 58 && c <= 64)

+        c += 97-58;

+    if ((c >= 91 && c <= 94) || c == 96)

+        c += 104-91;

+    else if (c >= 123)

+        c -= 4;

+    nn[i] = c;

+  }  

+}

+

+void sccwriter::write_file()

+{

+  static std::string filename( "scccode" );

+

+  //writer the h file

+  std::fstream fsh;

+  std::string fnameh( filename );

+  fnameh.append(".h");

+  fsh.open( fnameh.c_str(), std::ios::out );

+  //write the header in h

+  fsh << "#ifndef SCC_CODE_H" << std::endl;

+  fsh << "#define SCC_CODE_H" << std::endl << std::endl;

+  //include necessary files in h file

+  fsh << "#include \"check.h\"" << std::endl << std::endl;

+  //write the init function

+  fsh << "void init_compiled_scc();" << std::endl << std::endl;

+  //write the entry function

+  fsh << "Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args );" << std::endl << std::endl;

+  //write the side condition code functions

+  for( int n=0; n<(int)progs.size(); n++ )

+  {

+    //write the header in the h file

+    fsh << "inline ";

+    write_function_header( fsh, n );

+    fsh << ";" << std::endl << std::endl;

+  }

+  fsh << "#endif" << std::endl << std::endl;

+  fsh.close();

+

+

+  //writer the cpp code

+  std::fstream fsc;

+  std::string fnamec( filename );

+  fnamec.append(".cpp");

+  fsc.open( fnamec.c_str(), std::ios::out );

+  //include the h file in the cpp

+  fsc << "#include \"scccode.h\"" << std::endl << std::endl;

+  std::ostringstream fsc_funcs;

+  //write the side condition code functions

+  for( currProgram=0; currProgram<(int)progs.size(); currProgram++ )

+  {

+    //reset naming counters

+    vars.clear();

+    exprCount = 0;

+    strCount = 0;

+    argsCount = 0;

+    rnumCount = 0;

+

+    //for debugging

+    std::cout << "program #" << currProgram << " " << progNames[currProgram].c_str() << std::endl;

+

+    //write the function header

+    write_function_header( fsc_funcs, currProgram, opt_write_add_args|options );

+    if( (options&opt_write_call_debug)==0 )

+    {

+       fsc_funcs << "{" << std::endl;

+    }

+    //write the code

+    //std::vector< std::string > cleanVec;

+    //write_code( get_prog( n )->kids[2], fsc, 1, "return ", cleanVec );

+    //debug_write_code( progs[n].second->kids[2], fsc, 1 );

+    std::string expr;

+    write_expr( get_prog( currProgram )->kids[2], fsc_funcs, 1, expr );

+    indent( fsc_funcs, 1 );

+    fsc_funcs << "return " << expr.c_str() << ";" << std::endl;

+    fsc_funcs << "}" << std::endl << std::endl;

+  }

+  //write the predefined symbols necessary - symbols and progs

+  for( int a=0; a<(int)globalSyms.size(); a++ )

+  {

+    fsc << "Expr* e_" << globalSyms[a].c_str() << ";" << std::endl;

+  }

+  for( int a=0; a<(int)progs.size(); a++ )

+  {

+    fsc << "Expr* e_" << progNames[a].c_str() << ";" << std::endl;

+  }

+  fsc << std::endl;

+  //write the init function - initialize symbols and progs

+  fsc << "void init_compiled_scc(){" << std::endl;

+  for( int a=0; a<(int)globalSyms.size(); a++ )

+  {

+    indent( fsc, 1 );

+    fsc << "e_" << globalSyms[a].c_str() << " = symbols->get(\"" << globalSyms[a].c_str() << "\").first;" << std::endl;

+  }

+  for( int a=0; a<(int)progs.size(); a++ )

+  {

+    indent( fsc, 1 );

+    fsc << "e_" << progNames[a].c_str() << " = progs[\"" << progNames[a].c_str() << "\"];" << std::endl;

+  }

+  fsc << "}" << std::endl << std::endl;

+  fsc << "Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args ){" << std::endl;

+  //for( int n=0; n<(int)progs.size(); n++ ){

+  //  indent( fsc, 1 );

+  //  fsc << "static std::string s_" << progNames[n].c_str() << " = std::string( \"" << progNames[n].c_str() << "\" );" << std::endl;

+  //}

+  for( int n=0; n<(int)progs.size(); n++ ){

+    indent( fsc, 1 );

+    if( n!=0 ){

+      fsc << "}else ";

+    }

+    //for each function, test to see if the string matches the name of the function

+    fsc << "if( p==e_" << progNames[n].c_str() << " ){" << std::endl;

+    indent( fsc, 2 );

+    std::string fname;

+    get_function_name( progNames[n], fname );

+    //map the function to the proper function

+    fsc << "return " << fname.c_str() << "( ";

+    //write the arguments to the function from args

+    CExpr* progvars = (CExpr*)get_prog( n )->kids[1];

+    int counter = 0;

+    bool firstTime = true;

+    while( progvars->kids[counter] )

+    {

+      if( !firstTime )

+      {

+        fsc << ", ";

+      }

+      fsc << "args[" << counter << "]";

+      firstTime = false;

+      counter++;

+    }

+    fsc << " );" << std::endl;

+  }

+  indent( fsc, 1 );

+  fsc << "}else{" << std::endl;

+  indent( fsc, 2 );

+  //return null in the case the function could not be found

+  fsc << "return NULL;" << std::endl;

+  indent( fsc, 1 );

+  fsc << "}" << std::endl;

+  fsc << "}" << std::endl << std::endl;

+  fsc << fsc_funcs.str().c_str();

+

+  fsc.close();

+}

+

+void sccwriter::write_code( Expr* code, std::ostream& os, int ind, const char* retModStr, int opts )

+{

+  std::string retModString;

+  std::string incString;

+  if ( retModStr )

+  {

+    retModString = std::string( retModStr );

+    retModString.append( " = " );

+    incString = std::string( retModStr );

+    incString.append( "->inc();" );

+  }

+  switch( code->getclass() )

+  {

+  case INT_EXPR:

+    {

+      indent( os, ind );

+      os << retModString.c_str();

+      os << "new IntExpr( " << mpz_get_si( ((IntExpr*)code)->n ) << " );" << std::endl;

+      indent( os, ind );

+      os << incString.c_str() << std::endl;

+    }

+    break;

+  case RAT_EXPR:

+    {

+      mpz_t num, den;

+      mpz_init(num);

+      mpz_init(den);

+      mpq_get_num( num, ((RatExpr*)code)->n );

+      mpq_get_den( den, ((RatExpr*)code)->n );

+      indent( os, ind );

+      os << retModString.c_str();

+      os << "new RatExpr( " << mpz_get_si( num ) << ", " << mpz_get_si( den ) << " );" << std::endl;

+      indent( os, ind );

+      os << incString.c_str() << std::endl;

+    }

+    break;

+  case SYMS_EXPR:

+    {

+      //if it is a variable, simply write it to buffer

+      if( is_var( ((SymSExpr*)code)->s ) )

+      {

+        indent( os, ind );

+        os << retModString.c_str();

+        write_variable( ((SymSExpr*)code)->s.c_str(), os );

+        os << ";" << std::endl;  

+      }

+      else  //else must look at symbol lookup table

+      {

+        std::string var;

+        get_var_name( ((SymSExpr*)code)->s, var );

+        indent( os, ind );

+        os << retModString.c_str() << "e_" << var.c_str() << ";" << std::endl;

+        add_global_sym( var ); 

+      }

+      indent( os, ind );

+      os << incString.c_str() << std::endl;

+    }

+    break;

+  default:

+    switch( code->getop() )

+    {

+    case APP:
+      {
+        //collect the arguments
+        std::vector< Expr* > argVector;
+        code->collect_args( argVector );
+        //write the arguments
+        std::vector< std::string > args;
+        for( int a=0; a<(int)argVector.size(); a++ )
+        {
+          std::string expr;
+          write_expr( argVector[a], os, ind, expr );
+          args.push_back( expr );
+        }
+        //write_args( (CExpr*)code, os, ind, 1, args );
+        Expr* hd = code->get_head();
+        //map to a program in the case that it is a program
+        if( hd->getop()==PROG && get_prog_index_by_expr( hd )!=-1 )
+        {
+          indent( os, ind );
+          os << retModString << "f_" << progNames[ get_prog_index_by_expr( hd ) ].c_str() << "( ";
+          for( int a=0; a<(int)args.size(); a++ )
+          {
+            os << args[a].c_str();
+            if( a!=(int)( args.size()-1 ) ){
+              os << ", ";
+            }
+          }
+          os << " );" << std::endl;
+          for( int a=0; a<(int)args.size(); a++ )
+          {
+            write_dec( args[a], os, ind );
+          }
+        }
+        else
+        {
+#ifdef USE_FLAT_APP
+          std::string expr;
+          write_expr( hd, os, ind, expr );
+          indent( os, ind );
+          os << retModString << "new CExpr( APP, ";
+          os << expr.c_str() << ", ";
+          for( int a=0; a<(int)args.size(); a++ )
+          {
+            os << args[a].c_str();
+            if( a!=(int)( args.size()-1 ) ){
+              os << ", ";
+            }
+          }
+          os << " );" << std::endl;
+#else
+          std::string expr;
+          write_expr( hd, os, ind, expr );
+          indent( os, ind );
+          os << retModString;
+          for( int a=0; a<(int)args.size(); a++ )
+          {
+            os << "new CExpr( APP, ";
+          }
+          os << expr.c_str() << ", ";
+          for( int a=0; a<(int)args.size(); a++ )
+          {
+            os << args[a].c_str();
+            os << " )";
+            if( a!=(int)( args.size()-1 ) ){
+              os << ", ";
+            }
+          }
+          os << ";" << std::endl;
+#endif
+          //indent( os, ind );
+          //os << expr.c_str() << "->dec();" << std::endl;
+        }
+      }
+      break;

+    case MATCH:
+      {
+        //calculate the value for the expression
+        std::string expr;
+        write_expr( ((CExpr*)code)->kids[0], os, ind, expr );
+        //get the head
+        std::ostringstream sshd;
+        sshd << "e" << exprCount;
+        exprCount++;
+        indent( os, ind );
+        os << "Expr* " << sshd.str().c_str() << " = " << expr.c_str() << "->followDefs()->get_head();" << std::endl;
+        //write the arguments
+        std::vector< std::string > args;
+        write_args( (CExpr*)code, os, ind, 1, args );
+        bool encounterDefault = false;
+        //now make an if statement corresponding to the match 
+        int a = 0;
+        while( ((CExpr*)code)->kids[a+1] )
+        {
+          indent( os, ind );
+          if( a!=0 ){
+            os << "}else";
+          }
+          if( ((CExpr*)code)->kids[a+1]->getop()!=CASE ){
+            encounterDefault = true;
+            os << "{" << std::endl;
+            //write the body of the case
+            write_code( ((CExpr*)code)->kids[a+1], os, ind+1, retModStr ); 
+            indent( os, ind );
+            os << "}" << std::endl;
+          }else{
+            if( a!=0 )
+              os << " ";
+            os << "if( " << sshd.str().c_str() << "==" << args[a].c_str() << " ){" << std::endl;
+            //collect args from the variable in the code
+            std::ostringstream ssargs;
+            ssargs << "args" << argsCount;
+            argsCount++;
+#ifndef USE_FLAT_APP
+            indent( os, ind+1 );
+            os << "std::vector< Expr* > " << ssargs.str().c_str() << ";" << std::endl;
+            indent( os, ind+1 );
+            os << expr.c_str() << "->followDefs()->collect_args( " << ssargs.str().c_str() << " );" << std::endl;
+#endif
+            //set the variables defined in the pattern equal to the arguments
+            std::vector< Expr* > caseArgs;
+            ((CExpr*)((CExpr*)code)->kids[a+1])->kids[0]->collect_args( caseArgs );
+            for( int b=0; b<(int)caseArgs.size(); b++ )
+            {
+              indent( os, ind+1 );
+              os << "Expr* ";
+              write_variable( ((SymSExpr*)caseArgs[b])->s.c_str(), os );
+#ifdef USE_FLAT_APP
+              os << " = ((CExpr*)" << expr.c_str() << "->followDefs())->kids[" << b+1 << "];" << std::endl;
+#else
+              os << " = " << ssargs.str().c_str() << "[" << b << "];" << std::endl;
+#endif
+              vars.push_back( ((SymSExpr*)caseArgs[b])->s );
+            }
+            //write the body of the case
+            write_code( ((CExpr*)code)->kids[a+1], os, ind+1, retModStr, opt_write_case_body ); 
+          }
+          a++;
+        }
+        if( !encounterDefault )
+        {
+          indent( os, ind );
+          os << "}else{" << std::endl;
+          indent( os, ind + 1 );
+          os << "std::cout << \"Could not find match for expression in function f_";
+          os << progNames[currProgram].c_str() << " \";" << std::endl;
+          indent( os, ind + 1 );
+          os << sshd.str().c_str() << "->print( std::cout );" << std::endl;
+          indent( os, ind + 1 );
+          os << "std::cout << std::endl;" << std::endl;
+          indent( os, ind + 1 );
+          os << "exit( 1 );" << std::endl;
+          indent( os, ind );
+          os << "}" << std::endl;
+        }
+        write_dec( expr, os, ind );
+        for( int a=0; a<(int)args.size(); a++ )
+        {
+          write_dec( args[a], os, ind );
+        }
+      }
+      break;
+    case CASE:
+      if( opts&opt_write_case_body )
+      {
+        write_code( ((CExpr*)code)->kids[1], os, ind, retModStr );
+      }
+      else
+      {
+        write_code( ((CExpr*)code)->kids[0]->get_head(), os, ind, retModStr );
+      }
+      break;
+    case DO:
+      {
+        //write each of the children in sequence
+        int counter = 0;
+        while( ((CExpr*)code)->kids[counter] )
+        {
+          if( ((CExpr*)code)->kids[counter+1]==NULL )
+          {
+            write_code( ((CExpr*)code)->kids[counter], os, ind, retModStr );
+          }
+          else
+          {
+            std::string expr;
+            write_expr( ((CExpr*)code)->kids[counter], os, ind, expr );
+            //clean up memory
+            write_dec( expr, os, ind );
+          }
+          counter++;
+        }
+      }
+      break;
+    case LET:
+      {
+        indent( os, ind );
+        os << "Expr* ";
+        write_variable( ((SymSExpr*)((CExpr*)code)->kids[0])->s, os );
+        os << ";" << std::endl;
+        std::ostringstream ss;
+        write_variable( ((SymSExpr*)((CExpr*)code)->kids[0])->s, ss );
+        write_code( ((CExpr*)code)->kids[1], os, ind, ss.str().c_str() );
+        //add it to the variables
+        vars.push_back( ((SymSExpr*)((CExpr*)code)->kids[0])->s );
+        write_code( ((CExpr*)code)->kids[2], os, ind, retModStr );
+        //clean up memory
+        indent( os, ind );
+        write_variable( ((SymSExpr*)((CExpr*)code)->kids[0])->s, os );
+        os << "->dec();" << std::endl;
+      }
+      break;
+    case FAIL:
+      {
+        indent( os, ind );
+        os << retModString.c_str() << "NULL;" << std::endl;
+      }
+      break;
+#ifndef MARKVAR_32
+    case MARKVAR:
+      {
+        //calculate the value for the expression
+        std::string expr;
+        write_expr( ((CExpr*)code)->kids[0], os, ind, expr, opt_write_check_sym_expr );
+        //set the mark on the expression
+        indent( os, ind );
+        os << "if (" << expr.c_str() << "->followDefs()->getmark())" << std::endl;
+        indent( os, ind+1 );
+        os << expr.c_str() << "->followDefs()->clearmark();" << std::endl;
+        indent( os, ind );
+        os << "else" << std::endl;
+        indent( os, ind+1 );
+        os << expr.c_str() << "->followDefs()->setmark();" << std::endl;
+        //write the return if necessary
+        if( retModStr!=NULL ){
+          indent( os, ind );
+          os << retModString.c_str() << expr.c_str() << ";" << std::endl;
+          indent( os, ind );

+          os << incString.c_str() << std::endl;
+        }
+        write_dec( expr, os, ind );
+      }
+      break;
+    case IFMARKED:

+      {
+        //calculate the value for the expression
+        std::string expr;
+        write_expr( ((CExpr*)code)->kids[0], os, ind, expr, opt_write_check_sym_expr );
+        //if mark is set, write code for kids[1]
+        indent( os, ind );
+        os << "if (" << expr.c_str() << "->followDefs()->getmark()){" << std::endl;
+        write_code( ((CExpr*)code)->kids[1], os, ind+1, retModStr );
+        //else write code for kids[2]
+        indent( os, ind );
+        os << "}else{" << std::endl;
+        write_code( ((CExpr*)code)->kids[2], os, ind+1, retModStr );
+        indent( os, ind );
+        os << "}" << std::endl;

+        //clean up memory

+        write_dec( expr, os, ind );

+      }

+      break;
+#else
+    case MARKVAR:
+      {
+        //calculate the value for the expression
+        std::string expr;
+        write_expr( ((CExpr*)code)->kids[1], os, ind, expr, opt_write_check_sym_expr );
+        //set the mark on the expression
+        indent( os, ind );
+        os << "if ( ((SymExpr*)" << expr.c_str() << "->followDefs())->getmark(";
+        os << ((IntExpr*)((CExpr*)code)->kids[0])->get_num() << "))" << std::endl;
+        indent( os, ind+1 );
+        os << "((SymExpr*)" << expr.c_str() << "->followDefs())->clearmark(";
+        os << ((IntExpr*)((CExpr*)code)->kids[0])->get_num() << ");" << std::endl;
+        indent( os, ind );
+        os << "else" << std::endl;
+        indent( os, ind+1 );
+        os << "((SymExpr*)" << expr.c_str() << "->followDefs())->setmark(";
+        os << ((IntExpr*)((CExpr*)code)->kids[0])->get_num() << ");" << std::endl;
+        //write the return if necessary
+        if( retModStr!=NULL ){
+          indent( os, ind );
+          os << retModString.c_str() << expr.c_str() << ";" << std::endl;
+          indent( os, ind );

+          os << incString.c_str() << std::endl;
+        }
+        write_dec( expr, os, ind );
+      }
+      break;
+    case COMPARE:
+      {
+        std::string expr1, expr2;
+        write_expr( ((CExpr*)code)->kids[0], os, ind, expr1, opt_write_check_sym_expr );
+        write_expr( ((CExpr*)code)->kids[1], os, ind, expr2, opt_write_check_sym_expr );
+        indent( os, ind );
+        os << "if( ((SymExpr*)" << expr1.c_str() << ")->followDefs() < ((SymExpr*)" << expr2.c_str() << ")->followDefs() ){" << std::endl;
+        write_code( ((CExpr*)code)->kids[2], os, ind+1, retModStr );
+        indent( os, ind );
+        os << "}else{" << std::endl;
+        write_code( ((CExpr*)code)->kids[3], os, ind+1, retModStr );
+        indent( os, ind );
+        os << "}" << std::endl;
+        //clean up memory

+        write_dec( expr1, os, ind );
+        write_dec( expr2, os, ind );
+      }
+      break;
+    case IFMARKED:

+      {
+        //calculate the value for the expression
+        std::string expr;
+        write_expr( ((CExpr*)code)->kids[1], os, ind, expr, opt_write_check_sym_expr );
+        //if mark is set, write code for kids[1]
+        indent( os, ind );
+        os << "if ( ((SymExpr*)" << expr.c_str() << "->followDefs())->getmark(";
+        os << ((IntExpr*)((CExpr*)code)->kids[0])->get_num() << ")){" << std::endl;
+        write_code( ((CExpr*)code)->kids[2], os, ind+1, retModStr );
+        //else write code for kids[2]
+        indent( os, ind );
+        os << "}else{" << std::endl;
+        write_code( ((CExpr*)code)->kids[3], os, ind+1, retModStr );
+        indent( os, ind );
+        os << "}" << std::endl;

+        //clean up memory

+        write_dec( expr, os, ind );

+      }

+      break;
+#endif
+    case ADD:
+    case MUL:
+    case DIV:
+      {
+        //calculate the value for the first expression
+        std::string expr1;
+        write_expr( ((CExpr*)code)->kids[0], os, ind, expr1 );
+        //calculate the value for the second expression
+        std::string expr2;
+        write_expr( ((CExpr*)code)->kids[1], os, ind, expr2 );
+        std::ostringstream ss;
+        ss << "rnum" << rnumCount;
+        rnumCount++;
+        indent( os, ind );
+        os << "if( " << expr1.c_str() << "->followDefs()->getclass()==INT_EXPR ){" << std::endl;
+        indent( os, ind+1 );
+        os << "mpz_t " << ss.str().c_str() << ";" << std::endl;
+        indent( os, ind+1 );
+        os << "mpz_init(" << ss.str().c_str() << ");" << std::endl;
+        indent( os, ind+1 );
+        os << "mpz_";
+        if( code->getop()==ADD )
+          os << "add";
+        else
+          os << "mul";
+        os << "( " << ss.str().c_str() << ", ((IntExpr*)" << expr1.c_str() << "->followDefs())->n, ((IntExpr*)" << expr2.c_str() << "->followDefs())->n);" << std::endl;
+        indent( os, ind+1 );
+        os << retModString.c_str() << "new IntExpr(" << ss.str().c_str() << ");" << std::endl;
+        indent( os, ind );
+        os << "}else if( " << expr1.c_str() << "->followDefs()->getclass()==RAT_EXPR ){" << std::endl;
+        indent( os, ind+1 );
+        os << "mpq_t " << ss.str().c_str() << ";" << std::endl;
+        indent( os, ind+1 );
+        os << "mpq_init(" << ss.str().c_str() << ");" << std::endl;
+        indent( os, ind+1 );
+        os << "mpq_";
+        if( code->getop()==ADD )
+          os << "add";
+        else if( code->getop()==MUL )
+          os << "mul";
+        else
+          os << "div";
+        os << "( " << ss.str().c_str() << ", ((RatExpr*)" << expr1.c_str() << "->followDefs())->n, ((RatExpr*)" << expr2.c_str() << "->followDefs())->n);" << std::endl;
+        indent( os, ind+1 );
+        os << retModString.c_str() << "new RatExpr(" << ss.str().c_str() << ");" << std::endl;
+        indent( os, ind );
+        os << "}" << std::endl;
+        //clean up memory
+        write_dec( expr1, os, ind );
+        write_dec( expr2, os, ind );
+      }
+      break;
+    case NEG:

+      {

+        //calculate the value for the first expression
+        std::string expr1;
+        write_expr( ((CExpr*)code)->kids[0], os, ind, expr1 );
+        std::ostringstream ss;
+        ss << "rnum" << rnumCount;
+        rnumCount++;
+        indent( os, ind );
+        os << "if( " << expr1.c_str() << "->followDefs()->getclass()==INT_EXPR ){" << std::endl;
+        indent( os, ind+1 );
+        os << "mpz_t " << ss.str().c_str() << ";" << std::endl;
+        indent( os, ind+1 );
+        os << "mpz_init(" << ss.str().c_str() << ");" << std::endl;
+        indent( os, ind+1 );
+        os << "mpz_neg( " << ss.str().c_str() << ", ((IntExpr*)" << expr1.c_str() << "->followDefs())->n );" << std::endl;
+        indent( os, ind+1 );
+        os << retModString.c_str() << "new IntExpr(" << ss.str().c_str() << ");" << std::endl;

+        indent( os, ind );
+        os << "}else if( " << expr1.c_str() << "->followDefs()->getclass()==RAT_EXPR ){" << std::endl;

+        indent( os, ind+1 );
+        os << "mpq_t " << ss.str().c_str() << ";" << std::endl;
+        indent( os, ind+1 );
+        os << "mpq_init(" << ss.str().c_str() << ");" << std::endl;
+        indent( os, ind+1 );
+        os << "mpq_neg( " << ss.str().c_str() << ", ((RatExpr*)" << expr1.c_str() << "->followDefs())->n );" << std::endl;
+        indent( os, ind+1 );
+        os << retModString.c_str() << "new RatExpr(" << ss.str().c_str() << ");" << std::endl;

+        indent( os, ind );
+        os << "}" << std::endl;

+        //clean up memory

+        write_dec( expr1, os, ind );

+      }

+      break;

+    case IFNEG:

+    case IFZERO:

+      {

+        std::string expr1;
+        write_expr( ((CExpr*)code)->kids[0], os, ind, expr1 );

+        indent( os, ind );
+        os << "if( " << expr1.c_str() << "->followDefs()->getclass()==INT_EXPR ){" << std::endl;

+        indent( os, ind+1 );

+        os << "if( mpz_sgn( ((IntExpr *)" << expr1.c_str() << "->followDefs())->n ) ";

+        if( code->getop()==IFNEG )

+          os << "<";

+        else

+          os << "==";

+        os << " 0 ){" << std::endl;

+        write_code( ((CExpr*)code)->kids[1], os, ind+2, retModStr );

+        indent( os, ind+1 );

+        os << "}else{" << std::endl;

+        write_code( ((CExpr*)code)->kids[2], os, ind+2, retModStr );

+        indent( os, ind+1 );

+        os << "}" << std::endl;

+        indent( os, ind );
+        os << "}else if( " << expr1.c_str() << "->followDefs()->getclass()==RAT_EXPR ){" << std::endl;

+        indent( os, ind+1 );

+        os << "if( mpq_sgn( ((RatExpr *)" << expr1.c_str() << "->followDefs())->n ) ";

+        if( code->getop()==IFNEG )

+          os << "<";

+        else

+          os << "==";

+        os << " 0 ){" << std::endl;

+        write_code( ((CExpr*)code)->kids[1], os, ind+2, retModStr );

+        indent( os, ind+1 );

+        os << "}else{" << std::endl;

+        write_code( ((CExpr*)code)->kids[2], os, ind+2, retModStr );

+        indent( os, ind+1 );

+        os << "}" << std::endl;

+        indent( os, ind );
+        os << "}" << std::endl;

+        //clean up memory

+        write_dec( expr1, os, ind );

+      }

+      break;

+    case RUN:/*?*/break;

+    case PI:/*?*/break;
+    case LAM:/*?*/break;
+    case TYPE:/*?*/break;
+    case KIND:/*?*/break;
+    case ASCRIBE:/*?*/break;
+    case MPZ:/*?*/break;
+    case PROG:/*?*/break;
+    case PROGVARS:/*?*/break;
+    case PAT:/*?*/break;

+    }

+    break;

+  }

+}

+

+void sccwriter::write_args( CExpr* code, std::ostream& os, int ind, int childCounter, 

+                            std::vector< std::string >& args, int opts )

+{

+  bool encounterCase = false;

+  while( code->kids[childCounter] &&
+         (!encounterCase || code->kids[childCounter]->getop()==CASE ) )
+  {
+    encounterCase = encounterCase || code->kids[childCounter]->getop()==CASE;
+    if( code->kids[childCounter]->getclass()==SYMS_EXPR )
+    {
+      args.push_back( ((SymSExpr*)code->kids[childCounter])->s );
+    }
+    else
+    {
+      //calculate the value for the argument
+      std::string expr;
+      write_expr( code->kids[childCounter], os, ind, expr, opts );
+      args.push_back( expr );
+    }
+    childCounter++;
+  }

+}

+

+void sccwriter::write_expr( Expr* code, std::ostream& os, int ind, std::string& expr, int opts )

+{

+  if( code->getclass()==SYMS_EXPR && is_var( ((SymSExpr*)code)->s ) )

+  {

+    get_var_name( ((SymSExpr*)code)->s, expr );

+    indent( os, ind );

+    os << expr.c_str() << "->inc();" << std::endl;

+  }

+  else

+  {

+    std::ostringstream ss;
+    ss << "e" << exprCount;
+    exprCount++;

+    //declare the expression

+    indent( os, ind );

+    if( code->getclass()==SYMS_EXPR && !is_var( ((SymSExpr*)code)->s ) )

+    {

+      os << "static ";

+    }

+    os << "Expr* " << ss.str().c_str() << ";" << std::endl;

+    //write the expression

+    std::ostringstream ss2;
+    ss2 << ss.str().c_str();
+    write_code( code, os, ind, ss2.str().c_str(), opts );

+

+    //if is not a sym expression, then decrement the expression and return null

+    if( opts&opt_write_check_sym_expr )

+    {
+      indent( os, ind );
+      os << "if (" << expr.c_str() << "->getclass() != SYM_EXPR) {" << std::endl;
+      indent( os, ind+1 );
+      os << "exit( 1 );" << std::endl;
+      indent( os, ind );
+      os << "}" << std::endl;

+    }

+

+    expr = std::string( ss.str().c_str() );

+    vars.push_back( expr );

+  }

+  //increment the counter for memory management

+  //indent( os, ind );

+  //os << expr.c_str() << "->inc();" << std::endl;

+}

+

+void sccwriter::write_dec( const std::string& expr, std::ostream& os, int ind )

+{

+  bool wd = true;

+  if( wd )

+  {

+    indent( os, ind );

+    os << expr.c_str() << "->dec();" << std::endl;

+  }

+}

+

+void sccwriter::debug_write_code( Expr* code, std::ostream& os, int ind )

+{

+  indent( os, ind );

+  switch( code->getclass() )

+  {

+  case INT_EXPR:
+    os << "int_expr";
+    break;
+  case HOLE_EXPR:
+    os << "hole_expr";
+    break;
+  case SYM_EXPR:
+    os << "sym_expr";
+    break;
+  case SYMS_EXPR:

+    os << "syms_expr: " << ((SymSExpr*)code)->s.c_str();

+    break;

+  default:

+    switch( code->getop() )

+    {

+    case APP:
+      os << "app";
+      break;
+    case PI:
+      os << "pi";
+      break;
+    case LAM:
+      os << "lam";
+      break;
+    case TYPE:
+      os << "type";
+      break;
+    case KIND:
+      os << "kind";
+      break;
+    case ASCRIBE:
+      os << "ascribe";
+      break;
+    case MPZ:
+      os << "mpz";
+      break;
+    case PROG:
+      os << "prog";
+      break;
+    case PROGVARS:

+      os << "progvars";

+      break;

+    case MATCH:
+      os << "match";
+      break;
+    case CASE:
+      os << "case";
+      break;
+    case PAT:
+      os << "pat";
+      break;
+    case DO:
+      os << "do";
+      break;
+    case ADD:
+      os << "add";
+      break;
+    case NEG:
+      os << "neg";
+      break;
+    case LET:
+      os << "let";
+      break;
+    case RUN:
+      os << "run";
+      break;
+    case FAIL:
+      os << "fail";
+      break;
+    case MARKVAR:
+      os << "markvar";
+      break;
+    case IFMARKED:

+      os << "ifmarked";

+      break;

+    case COMPARE:

+      os << "compare";

+      break;

+    default:

+      os << "???";

+      break;

+    }

+  }

+  os << std::endl;

+  if( code->getop()!=0 )

+  {

+    CExpr* ce = (CExpr*)code;

+    int counter = 0;

+    while( ce->kids[counter] ){

+      debug_write_code( ce->kids[counter], os, ind+1 );

+      counter++;

+    }

+  }

+}

diff --git a/proofs/lfsc_checker/sccwriter.h b/proofs/lfsc_checker/sccwriter.h
new file mode 100644
index 000000000..f8922934f
--- /dev/null
+++ b/proofs/lfsc_checker/sccwriter.h
@@ -0,0 +1,86 @@
+#ifndef SCC_WRITER_H

+#define SCC_WRITER_H

+

+#include "expr.h"

+#include <vector>

+#include "check.h"

+

+enum

+{

+  opt_write_case_body = 0x00000001,

+  opt_write_check_sym_expr = 0x00000002,

+  opt_write_add_args = 0x000000004,

+  opt_write_no_inc = 0x00000008,

+

+  opt_write_call_debug = 0x00000010,

+  opt_write_nested_app = 0x00000020,

+};

+

+class sccwriter

+{

+private:

+  //options

+   int options;

+  //programs to write to file

+  symmap progs;

+  //list of indicies in progs

+  std::vector< Expr* > progPtrs;

+  std::vector< std::string > progNames;

+  int currProgram;

+  //current variables in the scope

+  std::vector< std::string > vars;

+  //global variables stored for lookups

+  std::vector< std::string > globalSyms;

+  //symbols that must be dec'ed

+  std::vector< std::string > decSyms;

+  //get program

+  CExpr* get_prog( int n ) { return (CExpr*)progs[ progNames[n] ]; }

+  //get index for string

+  int get_prog_index_by_expr( Expr* e );

+  int get_prog_index( const std::string& str );

+  //is variable in current scope

+  bool is_var( const std::string& str );

+  //add global sym

+  void add_global_sym( const std::string& str );

+  //expression count

+  static int exprCount;

+  //string count

+  static int strCount;

+  //args count

+  static int argsCount;

+  //num count

+  static int rnumCount;

+  //indent

+  static void indent( std::ostream& os, int ind );

+  //write function header

+  void write_function_header( std::ostream& os, int index, int opts = 0 );

+  void write_code( Expr* code, std::ostream& os, int ind, const char* retModStr, int opts = 0 );

+  //write all children starting at child counter to stream, store in Expr* e_...e_;

+  void write_args( CExpr* code, std::ostream& os, int ind, int childCounter, std::vector< std::string >& args, int opts = 0 );

+  //write expression - store result of code into e_ for some Expr* e_;

+  void write_expr( Expr* code, std::ostream& os, int ind, std::string& expr, int opts = 0 );

+  //write variable

+  void write_variable( const std::string& n, std::ostream& os );

+  //get function name

+  void get_function_name( const std::string& pname, std::string& fname );

+  //get the variable name

+  void get_var_name( const std::string& n, std::string& nn );

+  //write dec

+  void write_dec( const std::string& expr, std::ostream& os, int ind );

+public:

+  sccwriter( int opts = 0 ) : options( opts ){}

+  virtual ~sccwriter(){}

+

+  void add_scc( const std::string& pname, Expr* exp ) { 

+    //progs.push_back( std::pair< std::string, CExpr* >( pname, exp ) ); 

+    progs[pname] = exp;

+    progPtrs.push_back( exp );

+    progNames.push_back( pname );

+  }

+

+  void write_file();

+  //write code

+  static void debug_write_code( Expr* code, std::ostream& os, int ind );

+};

+

+#endif

diff --git a/proofs/lfsc_checker/trie.cpp b/proofs/lfsc_checker/trie.cpp
new file mode 100644
index 000000000..fedb508b0
--- /dev/null
+++ b/proofs/lfsc_checker/trie.cpp
@@ -0,0 +1,24 @@
+#include "trie.h"
+#include <iostream>
+
+class Simple : public Trie<int>::Cleaner {
+public:
+  ~Simple() {}
+  void clean(int p) {
+    (void)p;
+  }
+};
+
+template <>
+Trie<int>::Cleaner *Trie<int>::cleaner = new Simple;
+
+void unit_test_trie() {
+  Trie<int> t;
+  t.insert("a", 1);
+  t.insert("b", 2);
+  t.insert("abc", 3);
+  t.insert("b", 0);
+  std::cout << "a: " << t.get("a") << "\n";
+  std::cout << "b: " << t.get("b") << "\n";
+  std::cout << "abc: " << t.get("abc") << "\n";
+}
diff --git a/proofs/lfsc_checker/trie.h b/proofs/lfsc_checker/trie.h
new file mode 100644
index 000000000..094a9060a
--- /dev/null
+++ b/proofs/lfsc_checker/trie.h
@@ -0,0 +1,129 @@
+#ifndef sc2__trie_h
+#define sc2__trie_h
+
+#include <vector>
+#include <string.h>
+#include <stdlib.h>
+
+template<class Data>
+class Trie {
+protected:
+  char *str;
+  Data d;
+  bool using_next;
+  std::vector<Trie<Data> *> next;
+
+  // s is assumed to be non-empty (and non-null)
+  Data insert_next(const char *s, const Data &x) {
+    unsigned c = s[0];
+    if (c >= next.size()) {
+      using_next = true;
+      next.resize(c+1);
+      next[c] = new Trie<Data>;
+    }
+    else if (!next[c]) 
+      next[c] = new Trie<Data>;
+
+    return next[c]->insert(&s[1], x);
+  }
+
+  // s is assumed to be non-empty (and non-null)
+  Data get_next(const char *s) {
+    unsigned c = s[0];
+    if (c >= next.size())
+      return Data();
+    Trie<Data> *n = next[c];
+    if (!n)
+      return Data();
+    return n->get(&s[1]);
+  }
+
+public:
+  Trie() : str(), d(), using_next(false), next() { }
+
+  ~Trie();
+
+  class Cleaner {
+  public:
+    virtual ~Cleaner() {}
+    virtual void clean(Data d) = 0;
+  };
+
+  static Cleaner *cleaner;
+
+  bool eqstr(const char *s1, const char *s2) {
+    while (*s1 && *s2) {
+      if (*s1++ != *s2++)
+	return false;
+    }
+    return (*s1 == *s2);
+  }
+
+  Data get(const char *s) {
+    if (!s[0] && (!str || !str[0]))
+      return d;
+    if (str && eqstr(str,s))
+      return d;
+    if (using_next)
+      return get_next(s);
+    return Data();
+  }
+
+  Data insert(const char *s, const Data &x) {
+    if (s[0] == 0) {
+      // we need to insert x right here.
+      if (str) {
+	if (str[0] == 0) {
+	  // we need to replace d with x
+	  Data old = d;
+	  d = x;
+	  return old;
+	}
+	// we need to push str into next.
+	(void)insert_next(str,d);
+	free(str);
+      }
+      str = strdup(s);
+      d = x;
+      return Data();
+    }
+    
+    if (str) {
+      // cannot store x here 
+      if (str[0] != 0) {
+	insert_next(str,d);
+	free(str);
+	str = 0;
+	d = Data();
+      }
+      return insert_next(s,x);
+    }
+
+    if (using_next)
+      // also cannot store x here 
+      return insert_next(s,x);
+
+    // we can insert x here as an optimization
+    str = strdup(s);
+    d = x;
+    return Data();
+  }
+
+};
+
+template<class Data> 
+Trie<Data>::~Trie() 
+{
+  cleaner->clean(d);
+  for (int i = 0, iend = next.size(); i < iend; i++) {
+    Trie *t = next[i];
+    if (t)
+      delete t;
+  }
+  if (str)
+    free(str);
+}
+
+extern void unit_test_trie();
+
+#endif