7 files changed, 15 insertions, 14 deletions
diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp
index 499d362a9..ec4b223cf 100644
--- a/src/theory/bv/bv_inequality_graph.cpp
+++ b/src/theory/bv/bv_inequality_graph.cpp
@@ -30,7 +30,7 @@ const ReasonId CVC4::theory::bv::AxiomReasonId = -2;
 
 
 bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason) {
-  Debug("bv-inequality") << "InequlityGraph::addInequality " << a << " " << b << " strict: " << strict << "\n"; 
+  Debug("bv-inequality") << "InequalityGraph::addInequality " << a << " " << b << " strict: " << strict << "\n"; 
 
   TermId id_a = registerTerm(a);
   TermId id_b = registerTerm(b);
@@ -121,7 +121,7 @@ bool InequalityGraph::processQueue(BFSQueue& queue, TermId start) {
   while (!queue.empty()) {
     TermId current = queue.top();
     queue.pop();
-    Debug("bv-inequality-internal") << "InequalityGraph::processQueue proceessing " << getTermNode(current) << "\n";
+    Debug("bv-inequality-internal") << "InequalityGraph::processQueue processing " << getTermNode(current) << "\n";
   
     BitVector current_value = getValue(current);
   
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 2ea92635e..ca22f29b6 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -208,12 +208,13 @@ public:
    */
   virtual void spendResource() throw() {}
 
-  /** Handle user attribute
-    *   Associates theory t with the attribute attr.  Theory t will be
-    *   notifed whenever an attribute of name attr is set on a node.
-    *   This can happen through, for example, the SMT LIB v2 language.
-    */
-  virtual void handleUserAttribute( const char* attr, Theory* t ){}
+  /**
+   * Handle user attribute.
+   * Associates theory t with the attribute attr.  Theory t will be
+   * notified whenever an attribute of name attr is set on a node.
+   * This can happen through, for example, the SMT-LIBv2 language.
+   */
+  virtual void handleUserAttribute(const char* attr, Theory* t) {}
 
 };/* class OutputChannel */
 
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 0b4f2654b..187587227 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -31,7 +31,7 @@ namespace theory {
 class QuantRelevance
 {
 private:
-  /** for computing relavance */
+  /** for computing relevance */
   bool d_computeRel;
   /** map from quantifiers to symbols they contain */
   std::map< Node, std::vector< Node > > d_syms;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 6bfea5c44..e232a382e 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -212,7 +212,7 @@ private:
   std::map< TNode, std::vector< TNode > > d_var_contains;
   /** triggers for each operator */
   std::map< Node, std::vector< inst::Trigger* > > d_op_triggers;
-  /** helper for is intance of */
+  /** helper for is instance of */
   bool isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs );
 public:
   /** compute var contains */
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 45f161143..016abb2ac 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -291,7 +291,7 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) {
       d_subtermsToEvaluate[result] = t.getNumChildren();
       for (unsigned i = 0; i < t.getNumChildren(); ++ i) {
 	if (isConstant(getNodeId(t[i]))) {
-	  Debug("equality::evaluation") << d_name << "::eq::addTermInternal(" << t << "): evaluatates " << t[i] << std::endl;
+	  Debug("equality::evaluation") << d_name << "::eq::addTermInternal(" << t << "): evaluates " << t[i] << std::endl;
 	  subtermEvaluates(result);
 	}
       }
@@ -390,7 +390,7 @@ void EqualityEngine::assertPredicate(TNode t, bool polarity, TNode reason) {
 }
 
 void EqualityEngine::mergePredicates(TNode p, TNode q, TNode reason) {
-  Debug("equality") << d_name << "::eq::mergePredicats(" << p << "," << q << ")" << std::endl;
+  Debug("equality") << d_name << "::eq::mergePredicates(" << p << "," << q << ")" << std::endl;
   assertEqualityInternal(p, q, reason);
   propagate();
 }
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 2373c7f9a..34cb2443f 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -727,7 +727,7 @@ public:
   }
 
   /**
-   * Returns true if this kind is used for congruencce closure + evaluation of constants.
+   * Returns true if this kind is used for congruence closure + evaluation of constants.
    */
   bool isInterpretedFunctionKind(Kind fun) const {
     return d_congruenceKindsInterpreted.tst(fun);
diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h
index f993b941b..9caa8b1f1 100644
--- a/src/theory/uf/equality_engine_types.h
+++ b/src/theory/uf/equality_engine_types.h
@@ -282,7 +282,7 @@ enum FunctionApplicationType {
 struct FunctionApplication {
   /** Type of application */
   FunctionApplicationType type;
-  /** The actuall application elements */
+  /** The actual application elements */
   EqualityNodeId a, b;
 
   /** Construct an application */