Some cleanup and copyright updating

* update some copyrights for 2013
* cleaned up some comments/ifdefs, indentation
* some spelling corrections
* add some missing makefiles

46 files changed, 180 insertions, 163 deletions

diff --git a/COPYING b/COPYING
index 5016b3fbd..38196791a 100644
--- a/COPYING
+++ b/COPYING
@@ -1,5 +1,5 @@
-CVC4 is copyright (C) 2009, 2010, 2011, 2012 New York University and
-The University of Iowa.  All rights reserved.
+CVC4 is copyright (C) 2009, 2010, 2011, 2012, 2013 New York University
+and The University of Iowa.  All rights reserved.
 
 CVC4 is open-source; distribution is under the terms of the modified BSD
 license.  However, certain builds of CVC4 link against GPLed libraries,
@@ -19,7 +19,7 @@ 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.
 
--- Morgan Deters <mdeters@cs.nyu.edu>  Fri, 04 Feb 2011 14:56:41 -0500
+-- Morgan Deters <mdeters@cs.nyu.edu>  Mon, 28 Jan 2013 17:22:36 -0500
 
 CVC4 incorporates MiniSat code, excluded from the above copyright.
 See src/sat/minisat.  Its copyright:
diff --git a/contrib/configure-in-place b/contrib/configure-in-place
index 9da584d36..81517cfe4 100755
--- a/contrib/configure-in-place
+++ b/contrib/configure-in-place
@@ -1,8 +1,8 @@
-#!/bin/sh
+#!/bin/bash -ex
 #
 # configure-in-place
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010, 2011  The CVC4 Project
+# Copyright (c) 2010-2013  The CVC4 Project
 #
 # usage: configure-in-place [ arguments... ]
 #
@@ -10,9 +10,9 @@
 # should be invoked).
 #
 
-if [ -e .svn ]; then
+if [ -e .git ] && ! [ x"$1" = x-f ]; then
   echo
-  echo "DO NOT USE THIS IN SUBVERSION WORKING DIRECTORIES!"
+  echo "DO NOT USE THIS IN GIT WORKING DIRECTORIES!"
   echo
   echo "You might accidentally commit Makefiles in the source directories"
   echo "improperly, since they exist in the source directory for"
@@ -21,6 +21,10 @@ if [ -e .svn ]; then
   exit 1
 fi
 
+if [ x"$1" = x-f ]; then
+  shift
+fi
+
 ./configure "$@"
-. builds/current
-builds/$(CURRENT_BUILD)/config.status
+CURRENT_BUILD="$(grep '^CURRENT_BUILD *= *' builds/current | awk 'BEGIN {FS=" *= *"} {print$2}')"
+builds/$CURRENT_BUILD/config.status
diff --git a/contrib/mac-build b/contrib/mac-build
index 834191a0c..2501b667d 100755
--- a/contrib/mac-build
+++ b/contrib/mac-build
@@ -16,6 +16,7 @@ if [ $# -ne 0 ]; then
   echo "MacPorts must be installed (but this script installs prerequisite port" >&2
   echo "packages for CVC4).  If this script is successful, it prints a configure" >&2
   echo "line that you can use to configure CVC4." >&2
+  exit 1
 fi
 
 function reporterror {
diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java
index d45a8ad16..0af8da640 100644
--- a/examples/api/java/Combination.java
+++ b/examples/api/java/Combination.java
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file Combination.cpp
+/*! \file Combination.java
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
diff --git a/src/context/cdinsert_hashmap.h b/src/context/cdinsert_hashmap.h
index 0c84eda80..74e2fcf28 100644
--- a/src/context/cdinsert_hashmap.h
+++ b/src/context/cdinsert_hashmap.h
@@ -392,7 +392,7 @@ class CDInsertHashMap <TNode, Data, HashFcn > : public ContextObj {
    * If the key is a TNode and the backing (the hard node reference)
    * for the key in another data structure removes the key at the same context
    * the ref count could drop to 0.  The key would then not be eligible to be
-   * hashed. Getting the order right with a guarentee is to hard.
+   * hashed. Getting the order right with a guarantee is too hard.
    */
 
   BOOST_STATIC_ASSERT(sizeof(Data) == 0);
diff --git a/src/context/cdtrail_hashmap.h b/src/context/cdtrail_hashmap.h
index 5f090341d..2d2020a16 100644
--- a/src/context/cdtrail_hashmap.h
+++ b/src/context/cdtrail_hashmap.h
@@ -540,7 +540,7 @@ public:
     return d_trailMap->find(k);
   }
 
-  /** Returns an iterator to the begining of the map.  */
+  /** Returns an iterator to the beginning of the map.  */
   const_iterator begin() const{
     return d_trailMap->begin();
   }
@@ -561,7 +561,7 @@ class CDTrailHashMap <TNode, Data, HashFcn > : public ContextObj {
    * If the key is a TNode and the backing (the hard node reference)
    * for the key in another data structure removes the key at the same context
    * the ref count could drop to 0.  The key would then not be eligible to be
-   * hashed. Getting the order right with a guarentee is to hard.
+   * hashed. Getting the order right with a guarantee is too hard.
    */
 
   BOOST_STATIC_ASSERT(sizeof(Data) == 0);
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 9e8add752..08a3e49d0 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -96,7 +96,7 @@ bool DecisionEngine::isRelevant(SatVariable var)
 
 SatValue DecisionEngine::getPolarity(SatVariable var)
 {
-  Debug("decision") << "getPolariry(" << var <<")" << std::endl;
+  Debug("decision") << "getPolarity(" << var <<")" << std::endl;
   if(d_relevancyStrategy != NULL) {
     Assert(isRelevant(var));
     return d_relevancyStrategy->getPolarity( d_cnfStream->getNode(SatLiteral(var)) );
diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
index a3c0d1684..a2fda44fe 100644
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -9,7 +9,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Decision stategy
+ ** \brief Decision strategy
  **
  ** Decision strategy
  **/
diff --git a/src/expr/command.h b/src/expr/command.h
index 342aec5ff..9877044fb 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -401,7 +401,7 @@ public:
 
 /**
  * The command when an attribute is set by a user.  In SMT-LIBv2 this is done
- *  via the syntax (! expr :atrr)
+ *  via the syntax (! expr :attr)
  */
 class CVC4_PUBLIC SetUserAttributeCommand : public Command {
 protected:
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 5134d561e..ca89dfc91 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -2,7 +2,7 @@
 #
 # mkexpr
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2012  The CVC4 Project
+# Copyright (c) 2010-2013  The CVC4 Project
 #
 # The purpose of this script is to create {expr,expr_manager}.{h,cpp}
 # from template files and a list of theory kinds.  Basically it just
@@ -15,7 +15,7 @@
 # Output is to standard out.
 #
 
-copyright=2010-2012
+copyright=2010-2013
 
 filename=`basename "$1" | sed 's,_template,,'`
 
@@ -23,7 +23,8 @@ cat <<EOF
 /*********************                                                        */
 /** $filename
  **
- ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ ** Copyright $copyright  New York University and The University of Iowa,
+ ** and as below.
  **
  ** This file automatically generated by:
  **
diff --git a/src/expr/mkkind b/src/expr/mkkind
index 786d6187b..f8432466d 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -2,7 +2,7 @@
 #
 # mkkind
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2012  The CVC4 Project
+# Copyright (c) 2010-2013  The CVC4 Project
 #
 # The purpose of this script is to create kind.h (and also
 # type_properties.h) from a template and a list of theory kinds.
@@ -14,7 +14,7 @@
 # Output is to standard out.
 #
 
-copyright=2010-2012
+copyright=2010-2013
 
 filename=`basename "$1" | sed 's,_template,,'`
 
@@ -22,7 +22,8 @@ cat <<EOF
 /*********************                                                        */
 /** $filename
  **
- ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ ** Copyright $copyright  New York University and The University of Iowa,
+ ** and as below.
  **
  ** This header file automatically generated by:
  **
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 47ffc77f9..160a74eac 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -2,7 +2,7 @@
 #
 # mkmetakind
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2012  The CVC4 Project
+# Copyright (c) 2010-2013  The CVC4 Project
 #
 # The purpose of this script is to create metakind.h from a template
 # and a list of theory kinds.
@@ -17,13 +17,14 @@
 # Output is to standard out.
 #
 
-copyright=2010-2012
+copyright=2010-2013
 
 cat <<EOF
 /*********************                                                        */
 /** metakind.h
  **
- ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ ** Copyright $copyright  New York University and The University of Iowa,
+ ** and as below.
  **
  ** This header file automatically generated by:
  **
diff --git a/src/options/mkoptions b/src/options/mkoptions
index 0632cb3f9..fa6c4c260 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -2,7 +2,7 @@
 #
 # mkoptions
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2011-2012  The CVC4 Project
+# Copyright (c) 2011-2013  The CVC4 Project
 #
 # The purpose of this script is to create options.{h,cpp}
 # from template files and a list of options.
@@ -12,7 +12,7 @@
 #   mkoptions (template-file output-file)+ -t options.h-template options.cpp-template (options-file output-dir)+
 #
 
-copyright=2011-2012
+copyright=2011-2013
 
 me=$(basename "$0")
 
@@ -1314,7 +1314,8 @@ function output_module {
 /*********************                                                        */
 /** $filename
  **
- ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ ** Copyright $copyright  New York University and The University of Iowa,
+ ** and as below.
  **
  ** This file automatically generated by:
  **
@@ -1496,7 +1497,8 @@ cat <<EOF
 /*********************                                                        */
 /** $filename
  **
- ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ ** Copyright $copyright  New York University and The University of Iowa,
+ ** and as below.
  **
  ** This file automatically generated by:
  **
diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp
index 904f9a7fa..6a6ae8609 100644
--- a/src/parser/bounded_token_buffer.cpp
+++ b/src/parser/bounded_token_buffer.cpp
@@ -512,7 +512,7 @@ static pANTLR3_COMMON_TOKEN nextToken(pBOUNDED_TOKEN_BUFFER buffer) {
 }
 
 
-/// Return a string that represents the name assoicated with the input source
+/// Return a string that represents the name associated with the input source
 ///
 /// /param[in] is The ANTLR3_INT_STREAM interface that is representing this token stream.
 ///
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 1af4799be..b8ec160e8 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -416,10 +416,8 @@ Expr addNots(ExprManager* em, size_t n, Expr e) {
 
 @header {
 /**
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
+ ** This file is part of CVC4.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **/
diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g
index e3c36cf91..f8331c899 100644
--- a/src/parser/smt1/Smt1.g
+++ b/src/parser/smt1/Smt1.g
@@ -1,3 +1,4 @@
+/* *******************                                                        */
 /*! \file Smt1.g
  ** \verbatim
  ** Original author: cconway
@@ -30,10 +31,8 @@ options {
 
 @header {
 /**
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
+ ** This file is part of CVC4.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **/
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 648666091..1ee288aa4 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -31,10 +31,8 @@ options {
 
 @header {
 /**
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
+ ** This file is part of CVC4.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **/
diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h
index 62ed33632..62959c766 100644
--- a/src/parser/smt2/smt2_input.h
+++ b/src/parser/smt2/smt2_input.h
@@ -41,7 +41,7 @@ class Smt2Input : public AntlrInput {
   /** The ANTLR3 SMT2 lexer for the input. */
   pSmt2Lexer d_pSmt2Lexer;
 
-  /** The ANTLR3 CVC parser for the input. */
+  /** The ANTLR3 SMT2 parser for the input. */
   pSmt2Parser d_pSmt2Parser;
 
   /**
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 2180255ca..ec6868c5b 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -32,10 +32,8 @@ options {
 
 @header {
 /**
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
+ ** This file is part of CVC4.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **/
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 1e40ea63f..59b1d205b 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -151,7 +151,7 @@ void Tptp::includeFile(std::string fileName){
 
   if( d_tptpDir.empty() ){
     parseError("Couldn't open included file: " + fileName
-               + " at " + currentDirFileName + " and the TPTP directory is not specified (environnement variable TPTP)");
+               + " at " + currentDirFileName + " and the TPTP directory is not specified (environment variable TPTP)");
   };
 
   std::string tptpDirFileName = d_tptpDir + fileName;
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 324988585..ccbde6e80 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -160,8 +160,8 @@ protected:
    * Does a depth first search on removed literals and adds the literals
    * to be removed in the proper order to the stack. 
    * 
-   * @param lit the literal we are recusing on
-   * @param removedSet the previously computed set of redundantant literals
+   * @param lit the literal we are recursing on
+   * @param removedSet the previously computed set of redundant literals
    * @param removeStack the stack of literals in reverse order of resolution
    */
   void removedDfs(::Minisat::Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen);
diff --git a/src/prop/bvminisat/Makefile b/src/prop/bvminisat/Makefile
new file mode 100644
index 000000000..71888016d
--- /dev/null
+++ b/src/prop/bvminisat/Makefile
@@ -0,0 +1,4 @@
+topdir = ../../..
+srcdir = src/prop/bvminisat
+
+include $(topdir)/Makefile.subdir
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ca65ab1df..6b0d953dd 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -424,7 +424,7 @@ public:
   }
 
   void nmNotifyNewSkolem(TNode n, const std::string& comment, bool isGlobal) {
-    std::string id = n.getAttribute(expr::VarNameAttr());
+    string id = n.getAttribute(expr::VarNameAttr());
     DeclareFunctionCommand c(id,
                              n.toExpr(),
                              n.getType().toType());
@@ -541,8 +541,6 @@ public:
 
 }/* namespace CVC4::smt */
 
-using namespace CVC4::smt;
-
 SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_context(em->getContext()),
   d_userLevels(),
@@ -658,17 +656,17 @@ void SmtEngine::finalOptionsAreSet() {
 
   if(options::checkModels()) {
     if(! options::produceModels()) {
-      Notice() << "SmtEngine: turning on produce-models to support check-model" << std::endl;
+      Notice() << "SmtEngine: turning on produce-models to support check-model" << endl;
       setOption("produce-models", SExpr("true"));
     }
     if(! options::interactive()) {
-      Notice() << "SmtEngine: turning on interactive-mode to support check-model" << std::endl;
+      Notice() << "SmtEngine: turning on interactive-mode to support check-model" << endl;
       setOption("interactive-mode", SExpr("true"));
     }
   }
 
   if(options::produceAssignments() && !options::produceModels()) {
-    Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << std::endl;
+    Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << endl;
     setOption("produce-models", SExpr("true"));
   }
 
@@ -819,15 +817,15 @@ void SmtEngine::setLogicInternal() throw() {
   // by default, symmetry breaker is on only for QF_UF
   if(! options::ufSymmetryBreaker.wasSetByUser()) {
     bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified();
-    Trace("smt") << "setting uf symmetry breaker to " << qf_uf << std::endl;
+    Trace("smt") << "setting uf symmetry breaker to " << qf_uf << endl;
     options::ufSymmetryBreaker.set(qf_uf);
   }
   // by default, nonclausal simplification is off for QF_SAT and for quantifiers
   if(! options::simplificationMode.wasSetByUser()) {
     bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
     bool quantifiers = d_logic.isQuantified();
-    Trace("smt") << "setting simplification mode to <" << d_logic.getLogicString() << "> " << (!qf_sat && !quantifiers) << std::endl;
-    //simplifaction=none works better for SMT LIB benchmarks with quantifiers, not others
+    Trace("smt") << "setting simplification mode to <" << d_logic.getLogicString() << "> " << (!qf_sat && !quantifiers) << endl;
+    //simplification=none works better for SMT LIB benchmarks with quantifiers, not others
     //options::simplificationMode.set(qf_sat || quantifiers ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
     options::simplificationMode.set(qf_sat ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
   }
@@ -843,14 +841,14 @@ void SmtEngine::setLogicInternal() throw() {
     bool iteSimp = !d_logic.isQuantified() &&
       ((d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areRealsUsed()) ||
        (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_UF) && d_logic.isTheoryEnabled(THEORY_BV)));
-    Trace("smt") << "setting ite simplification to " << iteSimp << std::endl;
+    Trace("smt") << "setting ite simplification to " << iteSimp << endl;
     options::doITESimp.set(iteSimp);
   }
   // Turn on multiple-pass non-clausal simplification for QF_AUFBV
   if(! options::repeatSimp.wasSetByUser()) {
     bool repeatSimp = !d_logic.isQuantified() &&
       (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_UF) && d_logic.isTheoryEnabled(THEORY_BV));
-    Trace("smt") << "setting repeat simplification to " << repeatSimp << std::endl;
+    Trace("smt") << "setting repeat simplification to " << repeatSimp << endl;
     options::repeatSimp.set(repeatSimp);
   }
   // Turn on unconstrained simplification for QF_AUFBV
@@ -859,24 +857,24 @@ void SmtEngine::setLogicInternal() throw() {
     //    bool uncSimp = false && !qf_sat && !options::incrementalSolving();
     bool uncSimp = !options::incrementalSolving() && !d_logic.isQuantified() && !options::produceModels() && !options::checkModels() &&
       (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_BV));
-    Trace("smt") << "setting unconstrained simplification to " << uncSimp << std::endl;
+    Trace("smt") << "setting unconstrained simplification to " << uncSimp << endl;
     options::unconstrainedSimp.set(uncSimp);
   }
   // Unconstrained simp currently does *not* support model generation
   if (options::unconstrainedSimp.wasSetByUser() && options::unconstrainedSimp()) {
     if (options::produceModels()) {
-      Notice() << "SmtEngine: turning off produce-models to support unconstrainedSimp" << std::endl;
+      Notice() << "SmtEngine: turning off produce-models to support unconstrainedSimp" << endl;
       setOption("produce-models", SExpr("false"));
     }
     if (options::checkModels()) {
-      Notice() << "SmtEngine: turning off check-models to support unconstrainedSimp" << std::endl;
+      Notice() << "SmtEngine: turning off check-models to support unconstrainedSimp" << endl;
       setOption("check-models", SExpr("false"));
     }
   }
   // Turn on arith rewrite equalities only for pure arithmetic
   if(! options::arithRewriteEq.wasSetByUser()) {
     bool arithRewriteEq = d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified();
-    Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << std::endl;
+    Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << endl;
     options::arithRewriteEq.set(arithRewriteEq);
   }
   if(!  options::arithHeuristicPivots.wasSetByUser()) {
@@ -888,7 +886,7 @@ void SmtEngine::setLogicInternal() throw() {
         heuristicPivots = 0;
       }
     }
-    Trace("smt") << "setting arithHeuristicPivots  " << heuristicPivots << std::endl;
+    Trace("smt") << "setting arithHeuristicPivots  " << heuristicPivots << endl;
     options::arithHeuristicPivots.set(heuristicPivots);
   }
   if(! options::arithPivotThreshold.wasSetByUser()){
@@ -898,7 +896,7 @@ void SmtEngine::setLogicInternal() throw() {
         pivotThreshold = 16;
       }
     }
-    Trace("smt") << "setting arith arithPivotThreshold  " << pivotThreshold << std::endl;
+    Trace("smt") << "setting arith arithPivotThreshold  " << pivotThreshold << endl;
     options::arithPivotThreshold.set(pivotThreshold);
   }
   if(! options::arithStandardCheckVarOrderPivots.wasSetByUser()){
@@ -906,7 +904,7 @@ void SmtEngine::setLogicInternal() throw() {
     if(d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified()){
       varOrderPivots = 200;
     }
-    Trace("smt") << "setting arithStandardCheckVarOrderPivots  " << varOrderPivots << std::endl;
+    Trace("smt") << "setting arithStandardCheckVarOrderPivots  " << varOrderPivots << endl;
     options::arithStandardCheckVarOrderPivots.set(varOrderPivots);
   }
   // Turn off early theory preprocessing if arithRewriteEq is on
@@ -965,7 +963,7 @@ void SmtEngine::setLogicInternal() throw() {
         ? true : false
       );
 
-    Trace("smt") << "setting decision mode to " << decMode << std::endl;
+    Trace("smt") << "setting decision mode to " << decMode << endl;
     options::decisionMode.set(decMode);
     options::decisionStopOnly.set(stoponly);
   }
@@ -973,7 +971,7 @@ void SmtEngine::setLogicInternal() throw() {
   //for finite model finding
   if( ! options::instWhenMode.wasSetByUser()){
     if( options::fmfInstEngine() ){
-      Trace("smt") << "setting inst when mode to LAST_CALL" << std::endl;
+      Trace("smt") << "setting inst when mode to LAST_CALL" << endl;
       options::instWhenMode.set( INST_WHEN_LAST_CALL );
     }
   }
@@ -986,11 +984,11 @@ void SmtEngine::setLogicInternal() throw() {
   }
   else if (options::minisatUseElim()) {
     if (options::produceModels()) {
-      Notice() << "SmtEngine: turning off produce-models to support minisatUseElim" << std::endl;
+      Notice() << "SmtEngine: turning off produce-models to support minisatUseElim" << endl;
       setOption("produce-models", SExpr("false"));
     }
     if (options::checkModels()) {
-      Notice() << "SmtEngine: turning off check-models to support minisatUseElim" << std::endl;
+      Notice() << "SmtEngine: turning off check-models to support minisatUseElim" << endl;
       setOption("check-models", SExpr("false"));
     }
   }
@@ -1005,11 +1003,11 @@ void SmtEngine::setLogicInternal() throw() {
   if (d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
       !d_logic.isLinear()) {
     if (options::produceModels()) {
-      Warning() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << std::endl;
+      Warning() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << endl;
       setOption("produce-models", SExpr("false"));
     }
     if (options::checkModels()) {
-      Warning() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << std::endl;
+      Warning() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << endl;
       setOption("check-models", SExpr("false"));
     }
   }
@@ -1030,7 +1028,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
   Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
   if(Dump.isOn("benchmark")) {
     if(key == "status") {
-      std::string s = value.getValue();
+      string s = value.getValue();
       BenchmarkStatus status =
         (s == "sat") ? SMT_SATISFIABLE :
           ((s == "unsat") ? SMT_UNSATISFIABLE : SMT_UNKNOWN);
@@ -1210,7 +1208,7 @@ void SmtEngine::defineFunction(Expr func,
   // Permit (check-sat) (define-fun ...) (get-value ...) sequences.
   // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks
   // d_haveAdditions = true;
-  Debug("smt") << "definedFunctions insert " << funcNode << " " << formNode << std::endl;
+  Debug("smt") << "definedFunctions insert " << funcNode << " " << formNode << endl;
   d_definedFunctions->insert(funcNode, def);
 }
 
@@ -1220,7 +1218,7 @@ Node SmtEnginePrivate::getBVDivByZero(Kind k, unsigned width) {
   if (k == kind::BITVECTOR_UDIV) {
     if (d_BVDivByZero.find(width) == d_BVDivByZero.end()) {
       // lazily create the function symbols
-      std::ostringstream os;
+      ostringstream os;
       os << "BVUDivByZero_" << width;
       Node divByZero = nm->mkSkolem(os.str(),
                                     nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
@@ -1231,7 +1229,7 @@ Node SmtEnginePrivate::getBVDivByZero(Kind k, unsigned width) {
   }
   else if (k == kind::BITVECTOR_UREM) {
     if (d_BVRemByZero.find(width) == d_BVRemByZero.end()) {
-      std::ostringstream os;
+      ostringstream os;
       os << "BVURemByZero_" << width;
       Node divByZero = nm->mkSkolem(os.str(),
                                     nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
@@ -1271,7 +1269,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
     if(i != d_smt.d_definedFunctions->end()) {
       // replacement must be closed
       if((*i).second.getFormals().size() > 0) {
-        throw TypeCheckingException(n.toExpr(), std::string("Defined function requires arguments: `") + n.toString() + "'");
+        throw TypeCheckingException(n.toExpr(), string("Defined function requires arguments: `") + n.toString() + "'");
       }
       // don't bother putting in the cache
       return (*i).second.getFormula();
@@ -1300,9 +1298,9 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
     break;
   }
 
- case kind::BITVECTOR_UDIV:
- case kind::BITVECTOR_UREM: {
-   node = expandBVDivByZero(node);
+  case kind::BITVECTOR_UDIV:
+  case kind::BITVECTOR_UREM: {
+    node = expandBVDivByZero(node);
     break;
   }
   case kind::DIVISION: {
@@ -1374,7 +1372,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
       Debug("expand") << "     : \"" << name << "\"" << endl;
     }
     if(i == d_smt.d_definedFunctions->end()) {
-      throw TypeCheckingException(n.toExpr(), std::string("Undefined function: `") + func.toString() + "'");
+      throw TypeCheckingException(n.toExpr(), string("Undefined function: `") + func.toString() + "'");
     }
     if(Debug.isOn("expand")) {
       Debug("expand") << " defn: " << def.getFunction() << endl
@@ -1443,16 +1441,16 @@ static bool containsQuantifiers(Node n) {
 }
 
 Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< Node >& fvs ){
-  Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << std::endl;
+  Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << endl;
   if( n.getKind()==kind::NOT ){
     Node nn = preSkolemizeQuantifiers( n[0], !polarity, fvs );
     return nn.negate();
   }else if( n.getKind()==kind::FORALL ){
     if( polarity ){
-      std::vector< Node > children;
+      vector< Node > children;
       children.push_back( n[0] );
       //add children to current scope
-      std::vector< Node > fvss;
+      vector< Node > fvss;
       fvss.insert( fvss.begin(), fvs.begin(), fvs.end() );
       for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
         fvss.push_back( n[0][i] );
@@ -1468,13 +1466,13 @@ Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vect
       //process body
       Node nn = preSkolemizeQuantifiers( n[1], polarity, fvs );
       //now, substitute skolems for the variables
-      std::vector< TypeNode > argTypes;
+      vector< TypeNode > argTypes;
       for( int i=0; i<(int)fvs.size(); i++ ){
         argTypes.push_back( fvs[i].getType() );
       }
       //calculate the variables and substitution
-      std::vector< Node > vars;
-      std::vector< Node > subs;
+      vector< Node > vars;
+      vector< Node > subs;
       for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
         vars.push_back( n[0][i] );
       }
@@ -1487,7 +1485,7 @@ Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vect
           TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, n[0][i].getType() );
           Node op = NodeManager::currentNM()->mkSkolem( "skop_$$", typ, "op created during pre-skolemization" );
           //DOTHIS: set attribute on op, marking that it should not be selected as trigger
-          std::vector< Node > funcArgs;
+          vector< Node > funcArgs;
           funcArgs.push_back( op );
           funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() );
           subs.push_back( NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs ) );
@@ -1527,7 +1525,7 @@ Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vect
         return preSkolemizeQuantifiers( nn, polarity, fvs );
       }else{
         Assert( n.getKind() == kind::AND || n.getKind() == kind::OR );
-        std::vector< Node > children;
+        vector< Node > children;
         for( int i=0; i<(int)n.getNumChildren(); i++ ){
           children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvs ) );
         }
@@ -1576,7 +1574,7 @@ void SmtEnginePrivate::staticLearning() {
 static void dumpAssertions(const char* key,
                            const std::vector<Node>& assertionList) {
   if( Dump.isOn("assertions") &&
-      Dump.isOn(std::string("assertions:") + key) ) {
+      Dump.isOn(string("assertions:") + key) ) {
     // Push the simplified assertions to the dump output stream
     for(unsigned i = 0; i < assertionList.size(); ++ i) {
       TNode n = assertionList[i];
@@ -2350,7 +2348,7 @@ bool SmtEnginePrivate::simplifyAssertions()
       d_assertionsToCheck.swap(d_assertionsToPreprocess);
     }
 
-    Trace("smt") << "POST nonClasualSimplify" << std::endl;
+    Trace("smt") << "POST nonClausalSimplify" << endl;
     Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
     Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
@@ -2367,7 +2365,7 @@ bool SmtEnginePrivate::simplifyAssertions()
       }
     }
 
-    Trace("smt") << "POST theoryPP" << std::endl;
+    Trace("smt") << "POST theoryPP" << endl;
     Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
     Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
@@ -2377,7 +2375,7 @@ bool SmtEnginePrivate::simplifyAssertions()
       simpITE();
     }
 
-    Trace("smt") << "POST iteSimp" << std::endl;
+    Trace("smt") << "POST iteSimp" << endl;
     Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
     Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
@@ -2387,14 +2385,14 @@ bool SmtEnginePrivate::simplifyAssertions()
       unconstrainedSimp();
     }
 
-    Trace("smt") << "POST unconstrainedSimp" << std::endl;
+    Trace("smt") << "POST unconstrainedSimp" << endl;
     Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
     Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
     if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE) {
       Chat() << "...doing another round of nonclausal simplification..." << endl;
       Trace("simplify") << "SmtEnginePrivate::simplify(): "
-                        << " doing repeated simplification" << std::endl;
+                        << " doing repeated simplification" << endl;
       d_assertionsToCheck.swap(d_assertionsToPreprocess);
       Assert(d_assertionsToCheck.empty());
       bool noConflict = nonClausalSimplify();
@@ -2403,7 +2401,7 @@ bool SmtEnginePrivate::simplifyAssertions()
       }
     }
 
-    Trace("smt") << "POST repeatSimp" << std::endl;
+    Trace("smt") << "POST repeatSimp" << endl;
     Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
     Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
@@ -2630,11 +2628,11 @@ void SmtEnginePrivate::processAssertions() {
     //apply pre-skolemization to existential quantifiers
     for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
       Node prev = d_assertionsToPreprocess[i];
-      std::vector< Node > fvs;
+      vector< Node > fvs;
       d_assertionsToPreprocess[i] = Rewriter::rewrite( preSkolemizeQuantifiers( d_assertionsToPreprocess[i], true, fvs ) );
       if( prev!=d_assertionsToPreprocess[i] ){
-        Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << std::endl;
-        Trace("quantifiers-rewrite") << "   ...got " << d_assertionsToPreprocess[i] << std::endl;
+        Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << endl;
+        Trace("quantifiers-rewrite") << "   ...got " << d_assertionsToPreprocess[i] << endl;
       }
     }
   }
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index cf3aeafee..4655ea34e 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -371,8 +371,8 @@ void ConstraintValue::setAssertedToTheTheory(TNode witness) {
   d_database->pushAssertionOrderWatch(this, witness);
 }
 
-// bool ConstraintValue::isPsuedoConstraint() const {
-//   return d_proof == d_database->d_psuedoConstraintProof;
+// bool ConstraintValue::isPseudoConstraint() const {
+//   return d_proof == d_database->d_pseudoConstraintProof;
 // }
 
 bool ConstraintValue::isSelfExplaining() const {
@@ -486,7 +486,7 @@ ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Co
   d_equalityEngineProof = d_proofs.size();
   d_proofs.push_back(NullConstraint);
 
-  // d_psuedoConstraintProof = d_proofs.size();
+  // d_pseudoConstraintProof = d_proofs.size();
   // d_proofs.push_back(NullConstraint);
 }
 
@@ -833,11 +833,11 @@ void ConstraintValue::impliedBy(const std::vector<Constraint>& b){
   }
 }
 
-// void ConstraintValue::setPsuedoConstraint(){
+// void ConstraintValue::setPseudoConstraint(){
 //   Assert(truthIsUnknown());
 //   Assert(!hasLiteral());
 
-//   d_database->pushProofWatch(this, d_database->d_psuedoConstraintProof);
+//   d_database->pushProofWatch(this, d_database->d_pseudoConstraintProof);
 // }
 
 void ConstraintValue::setEqualityEngineProof(){
@@ -856,7 +856,7 @@ void ConstraintValue::markAsTrue(){
 void ConstraintValue::markAsTrue(Constraint imp){
   Assert(truthIsUnknown());
   Assert(imp->hasProof());
-  //Assert(!imp->isPsuedoConstraint());
+  //Assert(!imp->isPseudoConstraint());
 
   d_database->d_proofs.push_back(NullConstraint);
   d_database->d_proofs.push_back(imp);
@@ -868,8 +868,8 @@ void ConstraintValue::markAsTrue(Constraint impA, Constraint impB){
   Assert(truthIsUnknown());
   Assert(impA->hasProof());
   Assert(impB->hasProof());
-  //Assert(!impA->isPsuedoConstraint());
-  //Assert(!impB->isPsuedoConstraint());
+  //Assert(!impA->isPseudoConstraint());
+  //Assert(!impB->isPseudoConstraint());
 
   d_database->d_proofs.push_back(NullConstraint);
   d_database->d_proofs.push_back(impA);
@@ -886,7 +886,7 @@ void ConstraintValue::markAsTrue(const vector<Constraint>& a){
   for(vector<Constraint>::const_iterator i = a.begin(), end = a.end(); i != end; ++i){
     Constraint c_i = *i;
     Assert(c_i->hasProof());
-    //Assert(!c_i->isPsuedoConstraint());
+    //Assert(!c_i->isPseudoConstraint());
     d_database->d_proofs.push_back(c_i);
   }
 
@@ -903,7 +903,7 @@ SortedConstraintMap& ConstraintValue::constraintSet() const{
 bool ConstraintValue::proofIsEmpty() const{
   Assert(hasProof());
   bool result = d_database->d_proofs[d_proof] == NullConstraint;
-  //Assert((!result) || isSelfExplaining() || hasEqualityEngineProof() || isPsuedoConstraint());
+  //Assert((!result) || isSelfExplaining() || hasEqualityEngineProof() || isPseudoConstraint());
   Assert((!result) || isSelfExplaining() || hasEqualityEngineProof());
   return result;
 }
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 52aa5a5ce..82023a48b 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -273,7 +273,7 @@ private:
    */
   AssertionOrder _d_assertionOrder;
   /**
-   * This is guarenteed to be on the fact queue.
+   * This is guaranteed to be on the fact queue.
    * For example if x + y = x + 1 is on the fact queue, then use this 
    */
   TNode d_witness;
@@ -491,8 +491,8 @@ public:
    * The explanation is the constant true.
    * explainInto() does nothing.
    */
-  //void setPsuedoConstraint();
-  //bool isPsuedoConstraint() const;
+  //void setPseudoConstraint();
+  //bool isPseudoConstraint() const;
 
   /**
    * Returns a explanation of the constraint that is appropriate for conflicts.
@@ -709,7 +709,7 @@ private:
    *
    * This is a special proof that is always a member of the list.
    */
-  //ProofId d_psuedoConstraintProof;
+  //ProofId d_pseudoConstraintProof;
 
   typedef context::CDList<Constraint, ConstraintValue::ProofCleanup> ProofCleanupList;
   typedef context::CDList<Constraint, ConstraintValue::CanBePropagatedCleanup> CBPList;
diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index 19a16d558..51c1e5138 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -249,7 +249,7 @@ public:
   }
 
   /**
-   * Computes a sufficient upperbound to seperate two DeltaRationals.
+   * Computes a sufficient upperbound to separate two DeltaRationals.
    * This value is stored in res.
    * For any rational d such that
    *   0 < d < res
diff --git a/src/theory/arith/options b/src/theory/arith/options
index 9e758a0ef..efe594766 100644
--- a/src/theory/arith/options
+++ b/src/theory/arith/options
@@ -60,7 +60,6 @@ option arithMLTrickSubstitutions miplib-trick-subs --miplib-trick-subs unsigned
 
 option doCutAllBounded --enable-cut-all-bounded/--disable-cut-all-bounded bool :default false :read-write
  turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds
-/ turns off the integer solving step of periodically cutting all integer variables that have both upper and lower bounds
-
+/turns off the integer solving step of periodically cutting all integer variables that have both upper and lower bounds
 
 endmodule
diff --git a/src/theory/arith/options_handlers.h b/src/theory/arith/options_handlers.h
index 52e7cbf2a..f8f851964 100644
--- a/src/theory/arith/options_handlers.h
+++ b/src/theory/arith/options_handlers.h
@@ -52,7 +52,7 @@ This decides on kind of propagation arithmetic attempts to do during the search.
 ";
 
 static const std::string heuristicPivotRulesHelp = "\
-This decides on the rule used by simplex during hueristic rounds\n\
+This decides on the rule used by simplex during heuristic rounds\n\
 for deciding the next basic variable to select.\n\
 Heuristic pivot rules available:\n\
 +min\n\
diff --git a/src/theory/arrays/theory_arrays_model.cpp b/src/theory/arrays/theory_arrays_model.cpp
index 86bdad53f..4f7584ac1 100644
--- a/src/theory/arrays/theory_arrays_model.cpp
+++ b/src/theory/arrays/theory_arrays_model.cpp
@@ -41,7 +41,7 @@ Node ArrayModel::getValue( TheoryModel* m, Node i ){
     return it->second;
   }else{
     return NodeManager::currentNM()->mkNode( SELECT, getArrayValue(), i );
-    //return d_default_value;   //TODO: guarentee I can return this here
+    //return d_default_value;   //TODO: guarantee I can return this here
   }
 }
 
diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter
index 88ac5b9fb..2d8012bfb 100755
--- a/src/theory/mkrewriter
+++ b/src/theory/mkrewriter
@@ -2,7 +2,7 @@
 #
 # mkrewriter
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2012  The CVC4 Project
+# Copyright (c) 2010-2013  The CVC4 Project
 #
 # The purpose of this script is to create rewriter_tables.h from a template
 # and a list of theory kinds.
@@ -14,13 +14,14 @@
 # Output is to standard out.
 #
 
-copyright=2010-2012
+copyright=2010-2013
 
 cat <<EOF
 /*********************                                                        */
 /** rewriter_tables.h
  **
- ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ ** Copyright $copyright  New York University and The University of Iowa,
+ ** and as below.
  **
  ** This header file automatically generated by:
  **
diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index a44d8e9c3..3edc7c140 100755
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -2,7 +2,7 @@
 #
 # mktheorytraits
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2012  The CVC4 Project
+# Copyright (c) 2010-2013  The CVC4 Project
 #
 # The purpose of this script is to create theory_traits.h from a template
 # and a list of theory kinds.
@@ -14,7 +14,7 @@
 # Output is to standard out.
 #
 
-copyright=2010-2012
+copyright=2010-2013
 
 filename=`basename "$1" | sed 's,_template,,'`
 
@@ -22,7 +22,8 @@ cat <<EOF
 /*********************                                                        */
 /** $filename
  **
- ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ ** Copyright $copyright  New York University and The University of Iowa,
+ ** and as below.
  **
  ** This header file automatically generated by:
  **
diff --git a/src/theory/model.h b/src/theory/model.h
index e283ee183..98eeda97a 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -87,7 +87,7 @@ public:
   void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
   /** add term function
     *   addTerm( n ) will do any model-specific processing necessary for n,
-    *   such as contraining the interpretation of uninterpretted functions,
+    *   such as constraining the interpretation of uninterpreted functions,
     *   and adding n to the equality engine of this model
     */
   virtual void addTerm(TNode n);
diff --git a/src/theory/quantifiers/inst_gen.h b/src/theory/quantifiers/inst_gen.h
index 94922df18..930133954 100644
--- a/src/theory/quantifiers/inst_gen.h
+++ b/src/theory/quantifiers/inst_gen.h
@@ -50,10 +50,10 @@ public:
   int getNumMatches() { return d_matches.size(); }
   bool getMatch( EqualityQuery* q, int i, InstMatch& m );
   Node getMatchValue( int i ) { return d_match_values[i]; }
-};
+};/* class InstGenProcess */
 
-}
-}
-}
+}/* CVC4::theory::quantifiers namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
-#endif
+#endif /* __CVC4__THEORY__QUANTIFIERS__INST_GEN_H */
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 9f08764a9..bf67bdd25 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -358,7 +358,7 @@ Node QuantifierMacros::simplify( Node n ){
   if( n.getKind()==APPLY_UF ){
     Node op = n.getOperator();
     if( d_macro_defs.find( op )!=d_macro_defs.end() && !d_macro_defs[op].isNull() ){
-      //do subsitutition
+      //do substitution
       Node ret = d_macro_defs[op];
       ret = ret.substitute( d_macro_basis[op].begin(), d_macro_basis[op].end(), children.begin(), children.end() );
       return ret;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 9ac431107..6bfea5c44 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -167,7 +167,7 @@ public:
   /** get counterexample literal (for cbqi) */
   Node getCounterexampleLiteral( Node f );
   /** returns node n with bound vars of f replaced by instantiation constants of f
-      node n : is the futur pattern
+      node n : is the future pattern
       node f : is the quantifier containing which bind the variable
       return a pattern where the variable are replaced by variable for
       instantiation.
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index dc31f2d5f..019f69ec2 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__REP_SET_H
-#define __CVC4__REP_SET_H
+#ifndef __CVC4__THEORY__REP_SET_H
+#define __CVC4__THEORY__REP_SET_H
 
 #include "expr/node.h"
 #include <map>
@@ -45,7 +45,7 @@ public:
   void complete( TypeNode t );
   /** debug print */
   void toStream(std::ostream& out);
-};
+};/* class RepSet */
 
 //representative domain
 typedef std::vector< int > RepDomain;
@@ -104,9 +104,9 @@ public:
   /** debug print */
   void debugPrint( const char* c );
   void debugPrintSmall( const char* c );
-};
+};/* class RepSetIterator */
 
-}
-}
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
 
-#endif
\ No newline at end of file
+#endif /* __CVC4__THEORY__REP_SET_H */
diff --git a/src/theory/rewriterules/rr_candidate_generator.h b/src/theory/rewriterules/rr_candidate_generator.h
index 97c710219..d12c67f6a 100644
--- a/src/theory/rewriterules/rr_candidate_generator.h
+++ b/src/theory/rewriterules/rr_candidate_generator.h
@@ -32,7 +32,7 @@ typedef CVC4::theory::rrinst::CandidateGenerator CandidateGenerator;
 
 //New CandidateGenerator. They have a simpler semantic than the old one
 
-// Just iterate amoung the equivalence classes
+// Just iterate among the equivalence classes
 // node::Null() must be given to reset
 class CandidateGeneratorTheoryEeClasses : public CandidateGenerator{
 private:
@@ -54,7 +54,7 @@ public:
   };
 };
 
-// Just iterate amoung the equivalence class of the given node
+// Just iterate among the equivalence class of the given node
 // node::Null() *can't* be given to reset
 class CandidateGeneratorTheoryEeClass : public CandidateGenerator{
 private:
diff --git a/src/theory/rewriterules/rr_inst_match.h b/src/theory/rewriterules/rr_inst_match.h
index 63728a95b..636a4dbc1 100644
--- a/src/theory/rewriterules/rr_inst_match.h
+++ b/src/theory/rewriterules/rr_inst_match.h
@@ -180,7 +180,7 @@ public:
   /** If reset, or getNextMatch return false they remove from the
       InstMatch the binding that they have previously created */
 
-  /** virtual Matcher in order to have definned behavior */
+  /** virtual Matcher in order to have defined behavior */
   virtual ~Matcher(){};
 };
 
@@ -195,7 +195,7 @@ private:
   std::vector< triple< Matcher*, size_t, EqualityQuery* > > d_childrens;
   /** the variable that have been set by this matcher (during its own reset) */
   std::vector< TNode > d_binded; /* TNode because the variable are already in d_pattern */
-  /** the representant of the argument of the term given by the last reset */
+  /** the representative of the argument of the term given by the last reset */
   std::vector< Node > d_reps;
 public:
   /** The pattern we are producing matches for */
@@ -250,7 +250,7 @@ public:
 PatsMatcher* mkPatterns( std::vector< Node > pat, QuantifiersEngine* qe );
 PatsMatcher* mkPatternsEfficient( std::vector< Node > pat, QuantifiersEngine* qe );
 
-/** return true if whatever Node is subsituted for the variables the
+/** return true if whatever Node is substituted for the variables the
     given Node can't match the pattern */
 bool nonunifiable( TNode t, TNode pat, const std::vector<Node> & vars);
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f85a5f3cd..f7f689850 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -809,7 +809,7 @@ Node TheoryEngine::preprocess(TNode assertion) {
       stringstream ss;
       ss << "The logic was specified as " << d_logicInfo.getLogicString()
          << ", which doesn't include " << Theory::theoryOf(current)
-         << ", but got a preprocesing-time fact for that theory." << endl
+         << ", but got a preprocessing-time fact for that theory." << endl
          << "The fact:" << endl
          << current;
       throw LogicException(ss.str());
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 388c0edf0..a3779f0e8 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -269,7 +269,7 @@ class TheoryEngine {
     void safePoint() throw(theory::Interrupted, AssertionException) {
       if (d_engine->d_interrupted)
         throw theory::Interrupted();
-   }
+    }
 
     void conflict(TNode conflictNode) throw(AssertionException) {
       Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl;
@@ -741,20 +741,23 @@ private:
   std::map< std::string, std::vector< theory::Theory* > > d_attr_handle;
 public:
 
-  /** Set user attribute
-    * This function is called when an attribute is set by a user.  In SMT-LIBv2 this is done
-    *  via the syntax (! n :attr)
-    */
+  /**
+   * Set user attribute.
+   * This function is called when an attribute is set by a user.  In SMT-LIBv2 this is done
+   * via the syntax (! n :attr)
+   */
   void setUserAttribute(const std::string& attr, Node n);
 
-  /** Handle user attribute
-    *   Associates theory t with the attribute attr.  Theory t will be
-    *   notifed whenever an attribute of name attr is set.
-    */
+  /**
+   * Handle user attribute.
+   * Associates theory t with the attribute attr.  Theory t will be
+   * notified whenever an attribute of name attr is set.
+   */
   void handleUserAttribute(const char* attr, theory::Theory* t);
 
-  /** Check that the theory assertions are satisfied in the model
-   *  This function is called from the smt engine's checkModel routine
+  /**
+   * Check that the theory assertions are satisfied in the model.
+   * This function is called from the smt engine's checkModel routine.
    */
   void checkTheoryAssertionsWithModel();
 
diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index e0c750749..4378badc8 100644
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -124,7 +124,7 @@ This is CVC4 version " CVC4_RELEASE_STRING ) + \
     )) + "\n\
 compiled with " + ::CVC4::Configuration::getCompiler() + "\n\
 on " + ::CVC4::Configuration::getCompiledDateTime() + "\n\n\
-Copyright (C) 2009, 2010, 2011, 2012\n\
+Copyright (C) 2009, 2010, 2011, 2012, 2013\n\
   New York University and The University of Iowa\n\n" + \
     ( IS_CLN_BUILD ? "\
 This CVC4 library uses CLN as its multi-precision arithmetic library.\n\n\
diff --git a/src/util/integer.h.in b/src/util/integer.h.in
index 1f0174083..27b589b5a 100644
--- a/src/util/integer.h.in
+++ b/src/util/integer.h.in
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file integer.h
+/*! \file integer.h.in
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
diff --git a/src/util/rational.h.in b/src/util/rational.h.in
index c8e42a253..7f5b1feb4 100644
--- a/src/util/rational.h.in
+++ b/src/util/rational.h.in
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file rational.h
+/*! \file rational.h.in
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp
index 0304a8e35..d700b70d9 100644
--- a/src/util/sort_inference.cpp
+++ b/src/util/sort_inference.cpp
@@ -425,4 +425,4 @@ void SortInference::setSkolemVar( Node f, Node v, Node sk ){
   d_op_return_types[sk] = getSortId( f, v );
 }
 
-}
\ No newline at end of file
+}/* CVC4 namespace */
diff --git a/src/util/tls.h.in b/src/util/tls.h.in
index 17f1f1d6e..935586f77 100644
--- a/src/util/tls.h.in
+++ b/src/util/tls.h.in
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file tls.h
+/*! \file tls.h.in
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
diff --git a/test/regress/regress1/arith/Makefile b/test/regress/regress1/arith/Makefile
new file mode 100644
index 000000000..481d240e4
--- /dev/null
+++ b/test/regress/regress1/arith/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress1/arith
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check