Move LFSC checker out of the CVC repository. (#222)

LFSC now lives outside of the CVC4 repository and is not part of the CVC4 distribution
anymore. As a consequence, we

+ Add --with-lfsc and --with-lfsc-directory as configure options.
   In the case where CVC4 has not been built with integrated LFSC, all code that interacts with
   LFSC is disabled.

+ Disable proof checking if CVC4_USE_LFSC is not defined.
   Configuring the build with --check-proofs but without --with-lfsc results in an error.

+ Do not call LFSC's cleanup function (but we should in the future).
   LFSC checker segfaults during cleanup on regression testcase regress0/bv/core/bitvec7.smt.
   Disabled call to lfscc_cleanup until the problem in lfscc is fixed.

+ Disable building with LFSC for the distcheck travis build since it is not part of the distribution
   anymore. Further, make distcheck with LFSC would require to call contrib/get-lfsc-checker
   before calling make check on the temp build (the build of the unpacked distribution tar ball).

29 files changed, 0 insertions, 6924 deletions

diff --git a/proofs/lfsc_checker/.gitignore b/proofs/lfsc_checker/.gitignore
deleted file mode 100644
index 0712efe67..000000000
--- a/proofs/lfsc_checker/.gitignore
+++ /dev/null
@@ -1,15 +0,0 @@
-/autom4te.cache
-/stamp-h
-/config.h.in
-/config.log
-/config.status
-/config.cache
-/libtool
-/stamp-h1
-.dep
-Makefile.in
-/configure
-/aclocal.m4
-*~
-\#*\#
-*.swp
diff --git a/proofs/lfsc_checker/AUTHORS b/proofs/lfsc_checker/AUTHORS
deleted file mode 100644
index 0bd0a37b0..000000000
--- a/proofs/lfsc_checker/AUTHORS
+++ /dev/null
@@ -1,5 +0,0 @@
-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
deleted file mode 100644
index b220a3147..000000000
--- a/proofs/lfsc_checker/COPYING
+++ /dev/null
@@ -1,17 +0,0 @@
-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
deleted file mode 100644
index a1e89e18a..000000000
--- a/proofs/lfsc_checker/INSTALL
+++ /dev/null
@@ -1,370 +0,0 @@
-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
deleted file mode 100644
index ff483f5fb..000000000
--- a/proofs/lfsc_checker/Makefile.am
+++ /dev/null
@@ -1,30 +0,0 @@
-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
deleted file mode 100644
index 1a357ab4c..000000000
--- a/proofs/lfsc_checker/NEWS
+++ /dev/null
@@ -1,9 +0,0 @@
-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
deleted file mode 100644
index 5073569bc..000000000
--- a/proofs/lfsc_checker/README
+++ /dev/null
@@ -1,83 +0,0 @@
-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
deleted file mode 100644
index e100efa69..000000000
--- a/proofs/lfsc_checker/check.cpp
+++ /dev/null
@@ -1,1383 +0,0 @@
-#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  //AJR: deprecated
-
-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);
-Expr *statKind = new CExpr(KIND);
-Expr *statMpz = new CExpr(MPZ);
-Expr *statMpq = new CExpr(MPQ);
-
-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 = NULL;
-      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
-        Expr* orig_headtrm = headtrm;
-        headtrm = Expr::make_app( headtrm, arg );
-        if( orig_headtrm->getclass()==CEXPR ){
-          orig_headtrm->dec();
-        }
-#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;
-
-  std::string f;
-  if (strcmp(_filename,"stdin") == 0) {
-    curfile = stdin;
-    f = std::string(_filename);
-  }
-  else {
-    if (prev_curfile) {
-      f = std::string(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
-      // Note: dirname may modify its argument, so we create a non-const copy.
-      char *f_copy = strdup(f.c_str());
-      std::string str = std::string(dirname(f_copy));
-      free(f_copy);
-#endif
-            f = str + std::string("/") + std::string(_filename);
-    } else {
-      f = std::string(_filename);
-    }
-    curfile = fopen(f.c_str(), "r");
-    if (!curfile)
-      report_error(string("Could not open file \"") + f +
-                   string("\" for reading.\n"));
-  }
-
-  linenum = 1;
-  colnum = 1;
-  filename = f.c_str();
-
-  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);
-      }
-    }
-  }
-  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
deleted file mode 100644
index 756bb4db6..000000000
--- a/proofs/lfsc_checker/check.h
+++ /dev/null
@@ -1,167 +0,0 @@
-#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 char(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 != char(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 != char(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
deleted file mode 100644
index bdf938d32..000000000
--- a/proofs/lfsc_checker/chunking_memory_management.h
+++ /dev/null
@@ -1,157 +0,0 @@
-///////////////////////////////////////////////////////////////////////////////
-//                                                                           //
-//  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
deleted file mode 100644
index 48ebc5578..000000000
--- a/proofs/lfsc_checker/code.cpp
+++ /dev/null
@@ -1,1404 +0,0 @@
-#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
-      Expr* orig_pat = pat;
-      pat = Expr::make_app(pat,var);
-      if( orig_pat->getclass()==CEXPR ){
-        orig_pat->dec();
-      }
-#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();
-        Expr* orig_ret = ret;
-        ret = Expr::make_app(ret,ke);
-        if( orig_ret->getclass()==CEXPR ){
-          orig_ret->dec();
-        }
-#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 = true;
-    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;
-    }
-
-    assert(hd->getclass() == CEXPR);
-    CExpr *prog = (CExpr *)hd;
-    assert(prog->kids[1]->getclass() == CEXPR);
-    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++)) {
-        // Check whether not enough arguments were supplied
-        if (i >= args.size()) {
-          for (size_t i = 0; i < args.size(); i++) {
-             args[i]->dec();
-          }
-          return NULL;
-        }
-
-        old_vals.push_back(var->val);
-        var->val = args[i++];
-      }
-
-      // Check whether too many arguments were supplied
-      if (i < args.size()) {
-        for (size_t i = 0; i < args.size(); i++) {
-           args[i]->dec();
-        }
-        return NULL;
-      }
-
-      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++)) {
-        assert(i < args.size());
-        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;
-}
diff --git a/proofs/lfsc_checker/code.h b/proofs/lfsc_checker/code.h
deleted file mode 100644
index 9d00a6378..000000000
--- a/proofs/lfsc_checker/code.h
+++ /dev/null
@@ -1,15 +0,0 @@
-#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/config/ax_cxx_compile_stdcxx.m4 b/proofs/lfsc_checker/config/ax_cxx_compile_stdcxx.m4
deleted file mode 120000
index 0543a154f..000000000
--- a/proofs/lfsc_checker/config/ax_cxx_compile_stdcxx.m4
+++ /dev/null
@@ -1 +0,0 @@
-../../../config/ax_cxx_compile_stdcxx.m4
\ No newline at end of file
diff --git a/proofs/lfsc_checker/config/ax_cxx_compile_stdcxx_11.m4 b/proofs/lfsc_checker/config/ax_cxx_compile_stdcxx_11.m4
deleted file mode 120000
index 77adcd7a9..000000000
--- a/proofs/lfsc_checker/config/ax_cxx_compile_stdcxx_11.m4
+++ /dev/null
@@ -1 +0,0 @@
-../../../config/ax_cxx_compile_stdcxx_11.m4
\ No newline at end of file
diff --git a/proofs/lfsc_checker/configure.ac b/proofs/lfsc_checker/configure.ac
deleted file mode 100644
index 9ef902237..000000000
--- a/proofs/lfsc_checker/configure.ac
+++ /dev/null
@@ -1,51 +0,0 @@
-#                                               -*- Autoconf -*-
-# Process this file with autoconf to produce a configure script.
-
-AC_PREREQ([2.61])
-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
-
-# C++11 support in the compiler is now mandatory. Check for support and add
-# switches if necessary.
-AX_CXX_COMPILE_STDCXX_11([ext], [mandatory])
-
-# 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
deleted file mode 100644
index 8c8120edb..000000000
--- a/proofs/lfsc_checker/expr.cpp
+++ /dev/null
@@ -1,986 +0,0 @@
-#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; \
-    if (ref == 0) {  \
-      _e = r;		  \
-      goto start_destroy; \
-    } \
-    else \
-      r->data = (ref << 9) | (r->data & 511); \
-  } while(0)
-
-//removed from below "ref = ref -1;":   r->debugrefcnt(ref,DEC);
-
-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;
-    }
-    }
-  }
-  }
-  std::abort();  // 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
-  {
-    Expr **kids = new Expr *[args.size() - start + 2];
-    kids[0] = hd;
-    for (int i = start, iend = args.size(); i < iend; i++)
-      kids[i - start + 1] = args[i];
-    kids[args.size() - start + 1] = NULL;
-    return new CExpr(APP, true /* dummy */, kids);
-  }
-#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++;
-      }
-      Expr **kids = new Expr *[counter + 2];
-      counter = 0;
-      while( ((CExpr*)e1)->kids[counter] ){
-        kids[counter] = ((CExpr *)e1)->kids[counter];
-        kids[counter]->inc();
-        counter++;
-      }
-      kids[counter] = e2;
-      kids[counter + 1] = NULL;
-      ret = new CExpr(APP, true /* dummy */, kids);
-   }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) const {
-  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) const {
-  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 );
-    Expr **kids = new Expr *[args.size() + 2];
-    kids[0] = hd;
-    for (size_t a = 0; a < args.size(); a++) {
-      kids[a + 1] = convert_to_flat_app(args[a]);
-    }
-    kids[args.size() + 1] = 0;
-    CExpr *nce = new CExpr(APP, true /* dummy */, kids);
-    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( e1->kids[counter]!=e2->kids[counter] ){
-           if( !e2->kids[counter] || !e1->kids[counter]->defeq( e2->kids[counter] ) )
-              return false;
-           //--- optimization : replace child with equivalent pointer if was defeq
-           // Heuristic: prefer symbolic kids because they may be cheaper to
-           // deal with (e.g. in free_in()).
-           if (e2->kids[counter]->isSymbolic() ||
-               (!e1->kids[counter]->isSymbolic() &&
-                e1->kids[counter]->getrefcnt() <
-                    e2->kids[counter]->getrefcnt())) {
-             e1->kids[counter]->dec();
-             e2->kids[counter]->inc();
-             e1->kids[counter] = e2->kids[counter];
-           }else{
-             e2->kids[counter]->dec();
-             e1->kids[counter]->inc();
-             e2->kids[counter] = e1->kids[counter];
-           }
-         }
-         //---
-         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)
-
-  std::abort();  // never reached.
-}
-
-int Expr::fiCounter = 0;
-
-bool Expr::_free_in(Expr *x, expr_ptr_set_t *visited) {
-  // fiCounter++;
-  // if( fiCounter%1==0 )
-  //   std::cout << fiCounter << std::endl;
-  if (visited->find(this) != visited->end()) {
-    return false;
-  }
-
-  switch (getop()) {
-    case NOT_CEXPR:
-      switch (getclass()) {
-      case HOLE_EXPR: {
-         HoleExpr *h = (HoleExpr *)this;
-         if (h->val) return h->val->_free_in(x, visited);
-         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, visited);
-         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
-      assert(this->getclass() == CEXPR);
-      CExpr *e = (CExpr *)this;
-      Expr *tmp;
-      Expr **cur = e->kids;
-      visited->insert(this);
-      while ((tmp = *cur++))
-        if (tmp->_free_in(x, visited)) return true;
-      return false;
-   }
-   }
-   std::abort();  // 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
diff --git a/proofs/lfsc_checker/expr.h b/proofs/lfsc_checker/expr.h
deleted file mode 100644
index 0677533da..000000000
--- a/proofs/lfsc_checker/expr.h
+++ /dev/null
@@ -1,423 +0,0 @@
-#ifndef sc2__expr_h
-#define sc2__expr_h
-
-#include <stdint.h>
-#include <iostream>
-#include <map>
-#include <string>
-#include <unordered_set>
-#include <vector>
-
-#include "chunking_memory_management.h"
-#include "gmp.h"
-
-#define USE_FLAT_APP  //AJR: off deprecated
-#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 Expr;
-class SymExpr;
-
-struct hashExprPtr {
-  size_t operator()(const Expr *x) const {
-    return reinterpret_cast<uintptr_t>(x);
-  }
-};
-
-struct eqExprPtr {
-  bool operator()(const Expr *e1, const Expr *e2) const { return e1 == e2; }
-};
-
-typedef std::unordered_set<Expr *, hashExprPtr, eqExprPtr> expr_ptr_set_t;
-
-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;
-
-  enum { INC, DEC, CREATE };
-  void debugrefcnt(int ref, int what) {
-    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";
-  }
-
-  Expr(int _class, int _op)
-    : data(1 << 9 /* refcount 1, not cloned */| (_op << 3) | _class)
-  { }
-
-  bool _free_in(Expr *x, expr_ptr_set_t *visited);
-
- public:
-  virtual ~Expr() {}
-
-  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;
-#ifdef DEBUG_REFCNT    
-    debugrefcnt(ref,INC);
-#endif
-    data = (ref << 9) | (data & 511);
-  }
-  static void destroy(Expr *, bool);
-  inline void dec(bool dec_kids = true) {
-    int ref = getrefcnt();
-    ref = ref - 1;
-#ifdef DEBUG_REFCNT    
-    debugrefcnt(ref,DEC);
-#endif
-    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() const {
-    return getclass() == SYMS_EXPR || getop() == MPZ || getop() == MPQ;
-  }
-  inline bool isArithTerm() const {
-    return getop() == ADD || getop() == NEG;
-  }
-  inline bool isSymbolic() const {
-    return getclass() == SYM_EXPR || getclass() == SYMS_EXPR;
-  }
-
-  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) const;
-
-  Expr *get_body(int op = PI, bool follow_defs = true) const;
-
-  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) {
-    expr_ptr_set_t visited;
-    return _free_in(x, &visited);
-  }
-  bool get_free_in() const { 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;
-  virtual ~CExpr() {
-    delete[] kids;
-  }
-  CExpr(int _op) : Expr(CEXPR, _op), kids() {
-    kids = new Expr *[1];
-    kids[0] = 0;
-#ifdef DEBUG_REFCNT    
-    debugrefcnt(1,CREATE);
-#endif
-  }
-  CExpr(int _op, Expr *e1) : Expr(CEXPR, _op), kids() {
-    kids = new Expr *[2];
-    kids[0] = e1;
-    kids[1] = 0;
-#ifdef DEBUG_REFCNT    
-    debugrefcnt(1,CREATE);
-#endif
-  }
-  CExpr(int _op, Expr *e1, Expr *e2)
-    : Expr(CEXPR, _op), kids() {
-    kids = new Expr *[3];
-    kids[0] = e1;
-    kids[1] = e2;
-    kids[2] = 0;
-#ifdef DEBUG_REFCNT    
-    debugrefcnt(1,CREATE);
-#endif
-  }
-  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;
-#ifdef DEBUG_REFCNT    
-    debugrefcnt(1,CREATE);
-#endif
-  }
-  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;
-#ifdef DEBUG_REFCNT    
-    debugrefcnt(1,CREATE);
-#endif
-  }
-  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;
-#ifdef DEBUG_REFCNT    
-    debugrefcnt(1,CREATE);
-#endif
-  }
-
-  // _kids must be null-terminated.
-  CExpr(int _op, bool dummy, Expr **_kids) : Expr(CEXPR, _op), kids(_kids) {
-    (void)dummy;
-#ifdef DEBUG_REFCNT    
-    debugrefcnt(1,CREATE);
-#endif
-  }
-
-  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;
-  virtual ~IntExpr() {
-    mpz_clear(n);
-  }
-  IntExpr(mpz_t _n) : Expr(INT_EXPR, 0), n() {
-    mpz_init_set(n,_n);
-#ifdef DEBUG_REFCNT    
-    debugrefcnt(1,CREATE);
-#endif
-  }
-  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;
-  virtual ~RatExpr() {
-    mpq_clear(n);
-  }
-  RatExpr(mpq_t _n) : Expr(RAT_EXPR, 0), n() {
-    mpq_init( n );
-    mpq_set(n,_n);
-#ifdef DEBUG_REFCNT   
-    debugrefcnt(1,CREATE);
-#endif
-    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;
-#ifdef DEBUG_REFCNT   
-    if (theclass == SYM_EXPR)
-      debugrefcnt(1,CREATE);
-#endif
-  }
-  SymExpr(const SymExpr &e, int theclass = SYM_EXPR) 
-    : Expr(theclass, 0), val(0)
-  {
-    (void)e;
-#ifdef DEBUG_REFCNT   
-    if (theclass == SYM_EXPR)
-      debugrefcnt(1,CREATE);
-#endif
-  }
-
-  virtual ~SymExpr() {}
-
-#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)
-  {
-#ifdef DEBUG_REFCNT   
-    debugrefcnt(1,CREATE);
-#endif
-  }
-  SymSExpr(const SymSExpr &e, int theclass = SYMS_EXPR) 
-    : SymExpr(e, theclass), s(e.s)
-  { 
-#ifdef DEBUG_REFCNT   
-    debugrefcnt(1,CREATE);
-#endif
-  }
-
-  virtual ~SymSExpr() {}
-};
-
-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
-#ifdef DEBUG_REFCNT   
-    debugrefcnt(1,CREATE);
-#endif
-  }
-  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
deleted file mode 100644
index 016016c9d..000000000
--- a/proofs/lfsc_checker/libwriter.cpp
+++ /dev/null
@@ -1,238 +0,0 @@
-#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
deleted file mode 100644
index 91db5e911..000000000
--- a/proofs/lfsc_checker/libwriter.h
+++ /dev/null
@@ -1,28 +0,0 @@
-#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
deleted file mode 100644
index 1d8ba5809..000000000
--- a/proofs/lfsc_checker/main.cpp
+++ /dev/null
@@ -1,140 +0,0 @@
-#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 << "Proof checked successfully!" << std::endl << std::endl;
-  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
deleted file mode 100644
index a5c51ffc6..000000000
--- a/proofs/lfsc_checker/position.h
+++ /dev/null
@@ -1,30 +0,0 @@
-#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
deleted file mode 100644
index 40d9d1206..000000000
--- a/proofs/lfsc_checker/print_smt2.cpp
+++ /dev/null
@@ -1,122 +0,0 @@
-#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!=(int)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
deleted file mode 100644
index 9bee0e81c..000000000
--- a/proofs/lfsc_checker/print_smt2.h
+++ /dev/null
@@ -1,17 +0,0 @@
-#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
deleted file mode 100644
index 19712579c..000000000
--- a/proofs/lfsc_checker/scccode.cpp
+++ /dev/null
@@ -1,11 +0,0 @@
-#include "scccode.h"
-
-void init_compiled_scc(){
-
-}
-
-Expr* run_compiled_scc( Expr* p, std::vector< Expr* >& args ){
-  return NULL;
-}
-
-
diff --git a/proofs/lfsc_checker/scccode.h b/proofs/lfsc_checker/scccode.h
deleted file mode 100644
index 2ab549c10..000000000
--- a/proofs/lfsc_checker/scccode.h
+++ /dev/null
@@ -1,11 +0,0 @@
-#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 );
-
-#endif
-
diff --git a/proofs/lfsc_checker/sccwriter.cpp b/proofs/lfsc_checker/sccwriter.cpp
deleted file mode 100644
index d93341ab8..000000000
--- a/proofs/lfsc_checker/sccwriter.cpp
+++ /dev/null
@@ -1,977 +0,0 @@
-#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( (signed long int)" << 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 << " = NULL;" << 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() << " = NULL;" << 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
deleted file mode 100644
index bd9732579..000000000
--- a/proofs/lfsc_checker/sccwriter.h
+++ /dev/null
@@ -1,86 +0,0 @@
-#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
deleted file mode 100644
index fedb508b0..000000000
--- a/proofs/lfsc_checker/trie.cpp
+++ /dev/null
@@ -1,24 +0,0 @@
-#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
deleted file mode 100644
index 401fdb453..000000000
--- a/proofs/lfsc_checker/trie.h
+++ /dev/null
@@ -1,123 +0,0 @@
-#ifndef sc2__trie_h
-#define sc2__trie_h
-
-#include <assert.h>
-#include <stdlib.h>
-#include <string.h>
-#include <vector>
-
-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) {
-    assert(s != NULL && s[0] != '\0');
-    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) {
-    assert(s != NULL && s[0] != '\0');
-    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;
-
-  Data get(const char *s) {
-    if (!s[0] && (!str || !str[0]))
-      return d;
-    if (str && strcmp(str, s) == 0) 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