Some cleanup and copyright updating

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

41 files changed, 157 insertions, 153 deletions

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