Make statistics output consistent. (#1647)

* Fixes --hide-zero-stats (and really skips the 0 values)
* Removes the additional newline after each statistic
* Introduces theory::getStatsPrefix(TheoryId) to generate consistent
  prefixes for statistics based on the theory id
  (e.g., THEORY_BV -> "theory::bv").

36 files changed, 167 insertions, 165 deletions

diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp
index f099b017a..1917ea2d1 100644
--- a/examples/sets-translate/sets_translate.cpp
+++ b/examples/sets-translate/sets_translate.cpp
@@ -314,7 +314,7 @@ int main(int argc, char* argv[])
             cout << SetBenchmarkLogicCommand(logicinfo.getLogicString()) << endl;
           }
         } else {
-          logicinfo.enableTheory(theory::THEORY_ARRAY);
+          logicinfo.enableTheory(theory::THEORY_ARRAYS);
           // we print logic string only for Quantifiers, for Z3 stuff
           // we don't set the logic
         }
diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp
index 5f92af622..aa9107a18 100644
--- a/src/expr/kind_template.cpp
+++ b/src/expr/kind_template.cpp
@@ -91,5 +91,15 @@ ${type_constant_to_theory_id}
   throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad type constant");
 }
 
+std::string getStatsPrefix(TheoryId theoryId) {
+  switch(theoryId) {
+${theory_stats_prefixes}
+#line 98 "${template}"
+  default:
+    break;
+  }
+  return "unknown";
+}
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 9247f50dd..6ebbb32c2 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -99,6 +99,7 @@ CVC4_PUBLIC inline TheoryId& operator++(TheoryId& id) {
 std::ostream& operator<<(std::ostream& out, TheoryId theoryId);
 TheoryId kindToTheoryId(::CVC4::Kind k) CVC4_PUBLIC;
 TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) CVC4_PUBLIC;
+std::string getStatsPrefix(TheoryId theoryId) CVC4_PUBLIC;
 
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/expr/mkkind b/src/expr/mkkind
index 2b1901f5d..5e5be7c45 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -75,6 +75,7 @@ seen_theory_builtin=false
 
 theory_enum=
 theory_descriptions=
+theory_stats_prefixes=
 
 function theory {
   # theory ID T header
@@ -109,6 +110,9 @@ function theory {
 "
   theory_descriptions="${theory_descriptions}  case ${theory_id}: out << \"${theory_id}\"; break;
 "
+  prefix=$(echo "$theory_id" | tr '[:upper:]' '[:lower:]')
+  theory_stats_prefixes="${theory_stats_prefixes}  case ${theory_id}: return \"theory::${prefix#theory_}\"; break;
+"
 }
 
 function alternate {
@@ -416,6 +420,7 @@ for var in \
     type_constant_groundterms \
     type_properties_includes \
     theory_descriptions \
+    theory_stats_prefixes \
     template \
     ; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index a7666dfcf..94c0c9e23 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -260,26 +260,29 @@ void CommandExecutor::printStatsFilterZeros(std::ostream& out,
 
   std::getline(iss, statName, ',');
 
-  while( !iss.eof() ) {
-
+  while (!iss.eof())
+  {
     std::getline(iss, statValue, '\n');
 
-    double curFloat;
-    std::istringstream iss_stat_value (statValue);
-    iss_stat_value >> curFloat;
-    bool isFloat = iss_stat_value.good();
+    bool skip = false;
+    try
+    {
+      double dval = std::stod(statValue);
+      skip = (dval == 0.0);
+    }
+    // Value can not be converted, don't skip
+    catch (const std::invalid_argument&) {}
+    catch (const std::out_of_range&) {}
 
-    if( (isFloat && curFloat == 0) ||
-        statValue == " \"0\"" ||
-        statValue == " \"[]\"") {
-      // skip
-    } else {
+    skip = skip || (statValue == " \"0\"" || statValue == " \"[]\"");
+
+    if (!skip)
+    {
       out << statName << "," << statValue << std::endl;
     }
 
     std::getline(iss, statName, ',');
   }
-
 }
 
 void CommandExecutor::flushOutputStreams() {
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index d55b9f54b..332c66be1 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -317,7 +317,7 @@ bool Smt2::isOperatorEnabled(const std::string& name) const {
 bool Smt2::isTheoryEnabled(Theory theory) const {
   switch(theory) {
   case THEORY_ARRAYS:
-    return d_logic.isTheoryEnabled(theory::THEORY_ARRAY);
+    return d_logic.isTheoryEnabled(theory::THEORY_ARRAYS);
   case THEORY_BITVECTORS:
     return d_logic.isTheoryEnabled(theory::THEORY_BV);
   case THEORY_CORE:
@@ -477,7 +477,7 @@ void Smt2::setLogic(std::string name) {
     }
   }
 
-  if(d_logic.isTheoryEnabled(theory::THEORY_ARRAY)) {
+  if(d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)) {
     addTheory(THEORY_ARRAYS);
   }
 
diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index 511a82617..b0290fb3e 100644
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -1232,9 +1232,9 @@ std::string ArrayProof::skolemToLiteral(Expr skolem) {
 }
 
 void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
-  Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARRAY);
+  Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARRAYS);
 
-  if (theory::Theory::theoryOf(term) != theory::THEORY_ARRAY) {
+  if (theory::Theory::theoryOf(term) != theory::THEORY_ARRAYS) {
     // We can get here, for instance, if there's a (select ite ...), e.g. a non-array term
     // hiding as a subterm of an array term. In that case, send it back to the dispatcher.
     d_proofEngine->printBoundTerm(term, os, map);
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 89adf6c2b..f0fdf38b5 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -123,7 +123,7 @@ BitVectorProof* ProofManager::getBitVectorProof() {
 
 ArrayProof* ProofManager::getArrayProof() {
   Assert (options::proof());
-  TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_ARRAY);
+  TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_ARRAYS);
   return (ArrayProof*)pf;
 }
 
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 47a1191ad..0dd573dc6 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -83,7 +83,7 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) {
         return;
       }
 
-      if (id == theory::THEORY_ARRAY) {
+      if (id == theory::THEORY_ARRAYS) {
         d_theoryProofTable[id] = new LFSCArrayProof((theory::arrays::TheoryArrays*)th, this);
         return;
       }
@@ -169,9 +169,9 @@ void TheoryProofEngine::registerTerm(Expr term) {
 
   // A special case: the array theory needs to know of every skolem, even if
   // it belongs to another theory (e.g., a BV skolem)
-  if (ProofManager::getSkolemizationManager()->isSkolem(term) && theory_id != theory::THEORY_ARRAY) {
+  if (ProofManager::getSkolemizationManager()->isSkolem(term) && theory_id != theory::THEORY_ARRAYS) {
     Debug("pf::tp::register") << "TheoryProofEngine::registerTerm: registering a non-array skolem: " << term << std::endl;
-    getTheoryProof(theory::THEORY_ARRAY)->registerTerm(term);
+    getTheoryProof(theory::THEORY_ARRAYS)->registerTerm(term);
   }
 
   d_registrationCache.insert(term);
@@ -272,7 +272,7 @@ void LFSCTheoryProofEngine::printSort(Type type, std::ostream& os) {
   }
 
   if (type.isArray()) {
-    getTheoryProof(theory::THEORY_ARRAY)->printOwnedSort(type, os);
+    getTheoryProof(theory::THEORY_ARRAYS)->printOwnedSort(type, os);
     return;
   }
 
@@ -989,7 +989,7 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
     th = new theory::uf::TheoryUF(&fakeContext, &fakeContext, oc, v,
                                   ProofManager::currentPM()->getLogicInfo(),
                                   "replay::");
-  } else if (d_theory->getId()==theory::THEORY_ARRAY) {
+  } else if (d_theory->getId()==theory::THEORY_ARRAYS) {
     th = new theory::arrays::TheoryArrays(&fakeContext, &fakeContext, oc, v,
                                           ProofManager::currentPM()->getLogicInfo(),
                                           "replay::");
@@ -1067,7 +1067,7 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
 }
 
 bool TheoryProofEngine::supportedTheory(theory::TheoryId id) {
-  return (id == theory::THEORY_ARRAY ||
+  return (id == theory::THEORY_ARRAYS ||
           id == theory::THEORY_ARITH ||
           id == theory::THEORY_BV ||
           id == theory::THEORY_UF ||
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index edd0d5a11..e3632c08d 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -239,22 +239,18 @@ void BVMinisatSatSolver::toSatClause(const BVMinisat::Clause& clause,
 BVMinisatSatSolver::Statistics::Statistics(StatisticsRegistry* registry,
                                            const std::string& prefix)
     : d_registry(registry),
-      d_statStarts("theory::bv::" + prefix + "bvminisat::starts"),
-      d_statDecisions("theory::bv::" + prefix + "bvminisat::decisions"),
-      d_statRndDecisions("theory::bv::" + prefix + "bvminisat::rnd_decisions"),
-      d_statPropagations("theory::bv::" + prefix + "bvminisat::propagations"),
-      d_statConflicts("theory::bv::" + prefix + "bvminisat::conflicts"),
-      d_statClausesLiterals("theory::bv::" + prefix
-                            + "bvminisat::clauses_literals"),
-      d_statLearntsLiterals("theory::bv::" + prefix
-                            + "bvminisat::learnts_literals"),
-      d_statMaxLiterals("theory::bv::" + prefix + "bvminisat::max_literals"),
-      d_statTotLiterals("theory::bv::" + prefix + "bvminisat::tot_literals"),
-      d_statEliminatedVars("theory::bv::" + prefix
-                           + "bvminisat::eliminated_vars"),
-      d_statCallsToSolve("theory::bv::" + prefix
-                         + "bvminisat::calls_to_solve", 0),
-      d_statSolveTime("theory::bv::" + prefix + "bvminisat::solve_time"),
+      d_statStarts(prefix + "::bvminisat::starts"),
+      d_statDecisions(prefix + "::bvminisat::decisions"),
+      d_statRndDecisions(prefix + "::bvminisat::rnd_decisions"),
+      d_statPropagations(prefix + "::bvminisat::propagations"),
+      d_statConflicts(prefix + "::bvminisat::conflicts"),
+      d_statClausesLiterals(prefix + "::bvminisat::clauses_literals"),
+      d_statLearntsLiterals(prefix + "::bvminisat::learnts_literals"),
+      d_statMaxLiterals(prefix + "::bvminisat::max_literals"),
+      d_statTotLiterals(prefix + "::bvminisat::tot_literals"),
+      d_statEliminatedVars(prefix + "::bvminisat::eliminated_vars"),
+      d_statCallsToSolve(prefix + "::bvminisat::calls_to_solve", 0),
+      d_statSolveTime(prefix + "::bvminisat::solve_time"),
       d_registerStats(!prefix.empty())
 {
   if (!d_registerStats)
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 74d6c1b10..ae00b4caf 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1502,7 +1502,7 @@ void SmtEngine::setDefaults() {
     d_logic = log;
     d_logic.lock();
   }
-  if(d_logic.isTheoryEnabled(THEORY_ARRAY) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_SETS)) {
+  if(d_logic.isTheoryEnabled(THEORY_ARRAYS) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_SETS)) {
     if(!d_logic.isTheoryEnabled(THEORY_UF)) {
       LogicInfo log(d_logic.getUnlockedCopy());
       Trace("smt") << "because a theory that permits Boolean terms is enabled, also enabling UF" << endl;
@@ -1528,9 +1528,9 @@ void SmtEngine::setDefaults() {
   }
 
   // If in arrays, set the UF handler to arrays
-  if(d_logic.isTheoryEnabled(THEORY_ARRAY) && ( !d_logic.isQuantified() ||
+  if(d_logic.isTheoryEnabled(THEORY_ARRAYS) && ( !d_logic.isQuantified() ||
      (d_logic.isQuantified() && !d_logic.isTheoryEnabled(THEORY_UF)))) {
-    Theory::setUninterpretedSortOwner(THEORY_ARRAY);
+    Theory::setUninterpretedSortOwner(THEORY_ARRAYS);
   } else {
     Theory::setUninterpretedSortOwner(THEORY_UF);
   }
@@ -1540,7 +1540,7 @@ void SmtEngine::setDefaults() {
   // QF_LIA logics. --K [2014/10/15]
   if(! options::doITESimp.wasSetByUser()) {
     bool qf_aufbv = !d_logic.isQuantified() &&
-      d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+      d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
       d_logic.isTheoryEnabled(THEORY_UF) &&
       d_logic.isTheoryEnabled(THEORY_BV);
     bool qf_lia = !d_logic.isQuantified() &&
@@ -1566,7 +1566,7 @@ void SmtEngine::setDefaults() {
   }
   if(! options::simplifyWithCareEnabled.wasSetByUser() ){
     bool qf_aufbv = !d_logic.isQuantified() &&
-      d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+      d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
       d_logic.isTheoryEnabled(THEORY_UF) &&
       d_logic.isTheoryEnabled(THEORY_BV);
 
@@ -1577,7 +1577,7 @@ void SmtEngine::setDefaults() {
   // Turn off array eager index splitting for QF_AUFLIA
   if(! options::arraysEagerIndexSplitting.wasSetByUser()) {
     if (not d_logic.isQuantified() &&
-        d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+        d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
         d_logic.isTheoryEnabled(THEORY_UF) &&
         d_logic.isTheoryEnabled(THEORY_ARITH)) {
       Trace("smt") << "setting array eager index splitting to false" << endl;
@@ -1587,8 +1587,8 @@ void SmtEngine::setDefaults() {
   // Turn on model-based arrays for QF_AX (unless models are enabled)
   // if(! options::arraysModelBased.wasSetByUser()) {
   //   if (not d_logic.isQuantified() &&
-  //       d_logic.isTheoryEnabled(THEORY_ARRAY) &&
-  //       d_logic.isPure(THEORY_ARRAY) &&
+  //       d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
+  //       d_logic.isPure(THEORY_ARRAYS) &&
   //       !options::produceModels() &&
   //       !options::checkModels()) {
   //     Trace("smt") << "turning on model-based array solver" << endl;
@@ -1598,7 +1598,7 @@ void SmtEngine::setDefaults() {
   // 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_ARRAYS) &&
                       d_logic.isTheoryEnabled(THEORY_UF) &&
                       d_logic.isTheoryEnabled(THEORY_BV)) &&
                       !options::unsatCores();
@@ -1616,7 +1616,7 @@ void SmtEngine::setDefaults() {
                    !options::produceAssignments() &&
                    !options::checkModels() &&
                    !options::unsatCores() &&
-                   (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_BV));
+                   (d_logic.isTheoryEnabled(THEORY_ARRAYS) && d_logic.isTheoryEnabled(THEORY_BV));
     Trace("smt") << "setting unconstrained simplification to " << uncSimp << endl;
     options::unconstrainedSimp.set(uncSimp);
   }
@@ -1657,7 +1657,7 @@ void SmtEngine::setDefaults() {
   }
 
   if (! options::bvEagerExplanations.wasSetByUser() &&
-      d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+      d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
       d_logic.isTheoryEnabled(THEORY_BV)) {
     Trace("smt") << "enabling eager bit-vector explanations " << endl;
     options::bvEagerExplanations.set(true);
@@ -1720,13 +1720,13 @@ void SmtEngine::setDefaults() {
           ) ||
         // QF_AUFBV or QF_ABV or QF_UFBV
         (not d_logic.isQuantified() &&
-         (d_logic.isTheoryEnabled(THEORY_ARRAY) ||
+         (d_logic.isTheoryEnabled(THEORY_ARRAYS) ||
           d_logic.isTheoryEnabled(THEORY_UF)) &&
          d_logic.isTheoryEnabled(THEORY_BV)
          ) ||
         // QF_AUFLIA (and may be ends up enabling QF_AUFLRA?)
         (not d_logic.isQuantified() &&
-         d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+         d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
          d_logic.isTheoryEnabled(THEORY_UF) &&
          d_logic.isTheoryEnabled(THEORY_ARITH)
          ) ||
@@ -1747,7 +1747,7 @@ void SmtEngine::setDefaults() {
       d_logic.hasEverything() || d_logic.isTheoryEnabled(THEORY_STRINGS) ? false :
       ( // QF_AUFLIA
         (not d_logic.isQuantified() &&
-         d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+         d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
          d_logic.isTheoryEnabled(THEORY_UF) &&
          d_logic.isTheoryEnabled(THEORY_ARITH)
          ) ||
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index be16d684d..2ae658e6b 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -4,7 +4,7 @@
 # src/theory/builtin/kinds.
 #
 
-theory THEORY_ARRAY ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h"
+theory THEORY_ARRAYS ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h"
 typechecker "theory/arrays/theory_arrays_type_rules.h"
 
 properties polite stable-infinite parametric
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 508c9d8ff..dfa543ff3 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -58,7 +58,7 @@ const bool d_solveWrite2 = false;
 TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u,
                            OutputChannel& out, Valuation valuation,
                            const LogicInfo& logicInfo, std::string name)
-    : Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, name),
+    : Theory(THEORY_ARRAYS, c, u, out, valuation, logicInfo, name),
       d_numRow(name + "theory::arrays::number of Row lemmas", 0),
       d_numExt(name + "theory::arrays::number of Ext lemmas", 0),
       d_numProp(name + "theory::arrays::number of propagations", 0),
@@ -69,15 +69,15 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u,
       d_numGetModelValConflicts(name + "theory::arrays::number of getModelVal conflicts", 0),
       d_numSetModelValSplits(name + "theory::arrays::number of setModelVal splits", 0),
       d_numSetModelValConflicts(name + "theory::arrays::number of setModelVal conflicts", 0),
-      d_ppEqualityEngine(u, name + "theory::arrays::TheoryArraysPP" , true),
+      d_ppEqualityEngine(u, name + "theory::arrays::pp" , true),
       d_ppFacts(u),
       //      d_ppCache(u),
       d_literalsToPropagate(c),
       d_literalsToPropagateIndex(c, 0),
       d_isPreRegistered(c),
-      d_mayEqualEqualityEngine(c, name + "theory::arrays::TheoryArraysMayEqual", true),
+      d_mayEqualEqualityEngine(c, name + "theory::arrays::mayEqual", true),
       d_notify(*this),
-      d_equalityEngine(d_notify, c, name + "theory::arrays::TheoryArrays", true),
+      d_equalityEngine(d_notify, c, name + "theory::arrays", true),
       d_conflict(c, false),
       d_backtracker(c),
       d_infoMap(c, &d_backtracker, name),
@@ -681,7 +681,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
 
     if (node.getType().isArray()) {
       d_mayEqualEqualityEngine.addTerm(node);
-      d_equalityEngine.addTriggerTerm(node, THEORY_ARRAY);
+      d_equalityEngine.addTriggerTerm(node, THEORY_ARRAYS);
     }
     else {
       d_equalityEngine.addTerm(node);
@@ -723,7 +723,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     if (d_equalityEngine.hasTerm(node)) {
       break;
     }
-    d_equalityEngine.addTriggerTerm(node, THEORY_ARRAY);
+    d_equalityEngine.addTriggerTerm(node, THEORY_ARRAYS);
 
     TNode a = d_equalityEngine.getRepresentative(node[0]);
 
@@ -786,7 +786,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     d_infoMap.setConstArr(node, node);
     d_mayEqualEqualityEngine.addTerm(node);
     Assert(d_mayEqualEqualityEngine.getRepresentative(node) == node);
-    d_equalityEngine.addTriggerTerm(node, THEORY_ARRAY);
+    d_equalityEngine.addTriggerTerm(node, THEORY_ARRAYS);
     d_defValues[node] = defaultValue;
     break;
   }
@@ -795,7 +795,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     if (node.getType().isArray()) {
       // The may equal needs the node
       d_mayEqualEqualityEngine.addTerm(node);
-      d_equalityEngine.addTriggerTerm(node, THEORY_ARRAY);
+      d_equalityEngine.addTriggerTerm(node, THEORY_ARRAYS);
       Assert(d_equalityEngine.getSize(node) == 1);
     }
     else {
@@ -849,7 +849,7 @@ Node TheoryArrays::explain(TNode literal, eq::EqProof* proof) {
 
 void TheoryArrays::addSharedTerm(TNode t) {
   Debug("arrays::sharing") << spaces(getSatContext()->getLevel()) << "TheoryArrays::addSharedTerm(" << t << ")" << std::endl;
-  d_equalityEngine.addTriggerTerm(t, THEORY_ARRAY);
+  d_equalityEngine.addTriggerTerm(t, THEORY_ARRAYS);
   if (t.getType().isArray()) {
     d_sharedArrays.insert(t);
   }
@@ -882,7 +882,7 @@ void TheoryArrays::checkPair(TNode r1, TNode r2)
 
   TNode x = r1[1];
   TNode y = r2[1];
-  Assert(d_equalityEngine.isTriggerTerm(x, THEORY_ARRAY));
+  Assert(d_equalityEngine.isTriggerTerm(x, THEORY_ARRAYS));
 
   if (d_equalityEngine.hasTerm(x) && d_equalityEngine.hasTerm(y) &&
       (d_equalityEngine.areEqual(x,y) || d_equalityEngine.areDisequal(x,y,false))) {
@@ -909,14 +909,14 @@ void TheoryArrays::checkPair(TNode r1, TNode r2)
     }
   }
 
-  if (!d_equalityEngine.isTriggerTerm(y, THEORY_ARRAY)) {
+  if (!d_equalityEngine.isTriggerTerm(y, THEORY_ARRAYS)) {
     Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl;
     return;
   }
 
   // Get representative trigger terms
-  TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_ARRAY);
-  TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_ARRAY);
+  TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_ARRAYS);
+  TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_ARRAYS);
   EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared);
   switch (eqStatusDomain) {
     case EQUALITY_TRUE_AND_PROPAGATED:
@@ -987,11 +987,11 @@ void TheoryArrays::computeCareGraph()
       Assert(d_equalityEngine.hasTerm(r1));
       TNode x = r1[1];
 
-      if (!d_equalityEngine.isTriggerTerm(x, THEORY_ARRAY)) {
+      if (!d_equalityEngine.isTriggerTerm(x, THEORY_ARRAYS)) {
         Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl;
         continue;
       }
-      Node x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_ARRAY);
+      Node x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_ARRAYS);
 
       // Get the model value of index and find all reads that read from that same model value: these are the pairs we have to check
       // Also, insert this read in the list at the proper index
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index a36ec2e16..c04e8bde9 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -1111,9 +1111,10 @@ AbstractionModule::ArgsTableEntry& AbstractionModule::ArgsTable::getEntry(TNode
 }
 
 AbstractionModule::Statistics::Statistics(const std::string& name)
-  : d_numFunctionsAbstracted(name + "theory::bv::AbstractioModule::NumFunctionsAbstracted", 0)
-  , d_numArgsSkolemized(name + "theory::bv::AbstractioModule::NumArgsSkolemized", 0)
-  , d_abstractionTime(name + "theory::bv::AbstractioModule::AbstractionTime")
+    : d_numFunctionsAbstracted(name + "::abstraction::NumFunctionsAbstracted",
+                               0),
+      d_numArgsSkolemized(name + "::abstraction::NumArgsSkolemized", 0),
+      d_abstractionTime(name + "::abstraction::AbstractionTime")
 {
   smtStatisticsRegistry()->registerStat(&d_numFunctionsAbstracted);
   smtStatisticsRegistry()->registerStat(&d_numArgsSkolemized);
diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp
index 354b58376..101b64173 100644
--- a/src/theory/bv/bv_quick_check.cpp
+++ b/src/theory/bv/bv_quick_check.cpp
@@ -353,13 +353,13 @@ Node QuickXPlain::minimizeConflict(TNode confl) {
 }
 
 QuickXPlain::Statistics::Statistics(const std::string& name)
-  : d_xplainTime("theory::bv::"+name+"::QuickXplain::Time")
-  , d_numSolved("theory::bv::"+name+"::QuickXplain::NumSolved", 0)
-  , d_numUnknown("theory::bv::"+name+"::QuickXplain::NumUnknown", 0)
-  , d_numUnknownWasUnsat("theory::bv::"+name+"::QuickXplain::NumUnknownWasUnsat", 0)
-  , d_numConflictsMinimized("theory::bv::"+name+"::QuickXplain::NumConflictsMinimized", 0)
-  , d_finalPeriod("theory::bv::"+name+"::QuickXplain::FinalPeriod", 0)
-  , d_avgMinimizationRatio("theory::bv::"+name+"::QuickXplain::AvgMinRatio")
+  : d_xplainTime(name + "::QuickXplain::Time")
+  , d_numSolved(name + "::QuickXplain::NumSolved", 0)
+  , d_numUnknown(name + "::QuickXplain::NumUnknown", 0)
+  , d_numUnknownWasUnsat(name + "::QuickXplain::NumUnknownWasUnsat", 0)
+  , d_numConflictsMinimized(name + "::QuickXplain::NumConflictsMinimized", 0)
+  , d_finalPeriod(name + "::QuickXplain::FinalPeriod", 0)
+  , d_avgMinimizationRatio(name + "::QuickXplain::AvgMinRatio")
 {
   smtStatisticsRegistry()->registerStat(&d_xplainTime);
   smtStatisticsRegistry()->registerStat(&d_numSolved);
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index d163bf7f9..d941d018f 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -117,7 +117,7 @@ class QuickXPlain {
     IntStat d_numConflictsMinimized;
     IntStat d_finalPeriod;
     AverageStat d_avgMinimizationRatio;
-    Statistics(const std::string&);
+    Statistics(const std::string& name);
     ~Statistics();
   };
   BVQuickCheck* d_solver;
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 888c95692..456f627d0 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -229,7 +229,7 @@ void SubstitutionEx::storeCache(TNode from, TNode to, Node reason) {
 AlgebraicSolver::AlgebraicSolver(context::Context* c, TheoryBV* bv)
   : SubtheorySolver(c, bv)
   , d_modelMap(NULL)
-  , d_quickSolver(new BVQuickCheck("alg", bv))
+  , d_quickSolver(new BVQuickCheck("theory::bv::algebraic", bv))
   , d_isComplete(c, false)
   , d_isDifficult(c, false)
   , d_budget(options::bitvectorAlgebraicBudget())
@@ -239,7 +239,7 @@ AlgebraicSolver::AlgebraicSolver(context::Context* c, TheoryBV* bv)
   , d_numSolved(0)
   , d_numCalls(0)
   , d_ctx(new context::Context())
-  , d_quickXplain(options::bitvectorQuickXplain() ? new QuickXPlain("alg", d_quickSolver) : NULL)
+  , d_quickXplain(options::bitvectorQuickXplain() ? new QuickXPlain("theory::bv::algebraic", d_quickSolver) : NULL)
   , d_statistics()
 {}
 
@@ -778,14 +778,14 @@ Node AlgebraicSolver::getModelValue(TNode node) {
 }
 
 AlgebraicSolver::Statistics::Statistics()
-  : d_numCallstoCheck("theory::bv::AlgebraicSolver::NumCallsToCheck", 0)
-  , d_numSimplifiesToTrue("theory::bv::AlgebraicSolver::NumSimplifiesToTrue", 0)
-  , d_numSimplifiesToFalse("theory::bv::AlgebraicSolver::NumSimplifiesToFalse", 0)
-  , d_numUnsat("theory::bv::AlgebraicSolver::NumUnsat", 0)
-  , d_numSat("theory::bv::AlgebraicSolver::NumSat", 0)
-  , d_numUnknown("theory::bv::AlgebraicSolver::NumUnknown", 0)
-  , d_solveTime("theory::bv::AlgebraicSolver::SolveTime")
-  , d_useHeuristic("theory::bv::AlgebraicSolver::UseHeuristic", 0.2)
+  : d_numCallstoCheck("theory::bv::algebraic::NumCallsToCheck", 0)
+  , d_numSimplifiesToTrue("theory::bv::algebraic::NumSimplifiesToTrue", 0)
+  , d_numSimplifiesToFalse("theory::bv::algebraic::NumSimplifiesToFalse", 0)
+  , d_numUnsat("theory::bv::algebraic::NumUnsat", 0)
+  , d_numSat("theory::bv::algebraic::NumSat", 0)
+  , d_numUnknown("theory::bv::algebraic::NumUnknown", 0)
+  , d_solveTime("theory::bv::algebraic::SolveTime")
+  , d_useHeuristic("theory::bv::algebraic::UseHeuristic", 0.2)
 {
   smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
   smtStatisticsRegistry()->registerStat(&d_numSimplifiesToTrue);
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 61bbf667d..902a4dbe0 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -36,9 +36,9 @@ namespace bv {
 
 BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
   : SubtheorySolver(c, bv),
-    d_bitblaster(new TLazyBitblaster(c, bv, bv->getFullInstanceName() + "lazy")),
+    d_bitblaster(new TLazyBitblaster(c, bv, "theory::bv::lazy")),
     d_bitblastQueue(c),
-    d_statistics(bv->getFullInstanceName()),
+    d_statistics(),
     d_validModelCache(c, true),
     d_lemmaAtomsQueue(c),
     d_useSatPropagation(options::bitvectorPropagate()),
@@ -54,9 +54,9 @@ BitblastSolver::~BitblastSolver() {
   delete d_bitblaster;
 }
 
-BitblastSolver::Statistics::Statistics(const std::string &instanceName)
-  : d_numCallstoCheck(instanceName + "theory::bv::BitblastSolver::NumCallsToCheck", 0)
-  , d_numBBLemmas(instanceName + "theory::bv::BitblastSolver::NumTimesLemmasBB", 0)
+BitblastSolver::Statistics::Statistics()
+  : d_numCallstoCheck("theory::bv::BitblastSolver::NumCallsToCheck", 0)
+  , d_numBBLemmas("theory::bv::BitblastSolver::NumTimesLemmasBB", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
   smtStatisticsRegistry()->registerStat(&d_numBBLemmas);
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index f88810fca..509e59b19 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -39,7 +39,7 @@ class BitblastSolver : public SubtheorySolver {
   struct Statistics {
     IntStat d_numCallstoCheck;
     IntStat d_numBBLemmas;
-    Statistics(const std::string &instanceName);
+    Statistics();
     ~Statistics();
   };
   /** Bitblaster */
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 2c543b3da..bd4040dd7 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -34,7 +34,7 @@ using namespace CVC4::theory::bv::utils;
 CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
   : SubtheorySolver(c, bv),
     d_notify(*this),
-    d_equalityEngine(d_notify, c, "theory::bv::TheoryBV", true),
+    d_equalityEngine(d_notify, c, "theory::bv::ee", true),
     d_slicer(new Slicer()),
     d_isComplete(c, true),
     d_lemmaThreshold(16),
diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
index bed922830..54c9cb08a 100644
--- a/src/theory/bv/bv_to_bool.cpp
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -241,12 +241,12 @@ void BvToBoolPreprocessor::liftBvToBool(const std::vector<Node>& assertions, std
 }
 
 BvToBoolPreprocessor::Statistics::Statistics()
-  : d_numTermsLifted("theory::bv::BvToBoolPreprocess::NumberOfTermsLifted", 0)
-  , d_numAtomsLifted("theory::bv::BvToBoolPreprocess::NumberOfAtomsLifted", 0)
-  , d_numTermsForcedLifted("theory::bv::BvToBoolPreprocess::NumberOfTermsForcedLifted", 0)
-  , d_numTermsLowered("theory::bv::BvToBoolPreprocess::NumberOfTermsLowered", 0)
-  , d_numAtomsLowered("theory::bv::BvToBoolPreprocess::NumberOfAtomsLowered", 0)    
-  , d_numTermsForcedLowered("theory::bv::BvToBoolPreprocess::NumberOfTermsForcedLowered", 0)
+  : d_numTermsLifted("theory::bv::BvToBool::NumTermsLifted", 0)
+  , d_numAtomsLifted("theory::bv::BvToBool::NumAtomsLifted", 0)
+  , d_numTermsForcedLifted("theory::bv::BvToBool::NumTermsForcedLifted", 0)
+  , d_numTermsLowered("theory::bv::BvToBool::NumTermsLowered", 0)
+  , d_numAtomsLowered("theory::bv::BvToBool::NumAtomsLowered", 0)
+  , d_numTermsForcedLowered("theory::bv::BvToBool::NumTermsForcedLowered", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_numTermsLifted);
   smtStatisticsRegistry()->registerStat(&d_numAtomsLifted);
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index 6cd4a3314..189898c0c 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -369,13 +369,13 @@ void TLazyBitblaster::getConflict(std::vector<TNode>& conflict)
 }
 
 TLazyBitblaster::Statistics::Statistics(const std::string& prefix) :
-  d_numTermClauses("theory::bv::"+prefix+"::NumberOfTermSatClauses", 0),
-  d_numAtomClauses("theory::bv::"+prefix+"::NumberOfAtomSatClauses", 0),
-  d_numTerms("theory::bv::"+prefix+"::NumberOfBitblastedTerms", 0),
-  d_numAtoms("theory::bv::"+prefix+"::NumberOfBitblastedAtoms", 0),
-  d_numExplainedPropagations("theory::bv::"+prefix+"::NumberOfExplainedPropagations", 0),
-  d_numBitblastingPropagations("theory::bv::"+prefix+"::NumberOfBitblastingPropagations", 0),
-  d_bitblastTimer("theory::bv::"+prefix+"::BitblastTimer")
+  d_numTermClauses(prefix + "::NumTermSatClauses", 0),
+  d_numAtomClauses(prefix + "::NumAtomSatClauses", 0),
+  d_numTerms(prefix + "::NumBitblastedTerms", 0),
+  d_numAtoms(prefix + "::NumBitblastedAtoms", 0),
+  d_numExplainedPropagations(prefix + "::NumExplainedPropagations", 0),
+  d_numBitblastingPropagations(prefix + "::NumBitblastingPropagations", 0),
+  d_bitblastTimer(prefix + "::BitblastTimer")
 {
   smtStatisticsRegistry()->registerStat(&d_numTermClauses);
   smtStatisticsRegistry()->registerStat(&d_numAtomClauses);
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index fa234fcde..4c4b7c723 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -640,12 +640,12 @@ std::string UnionFind::debugPrint(TermId id) {
 }
 
 UnionFind::Statistics::Statistics():
-  d_numNodes("theory::bv::slicer::NumberOfNodes", 0),
-  d_numRepresentatives("theory::bv::slicer::NumberOfRepresentatives", 0),
-  d_numSplits("theory::bv::slicer::NumberOfSplits", 0),
-  d_numMerges("theory::bv::slicer::NumberOfMerges", 0),
+  d_numNodes("theory::bv::slicer::NumNodes", 0),
+  d_numRepresentatives("theory::bv::slicer::NumRepresentatives", 0),
+  d_numSplits("theory::bv::slicer::NumSplits", 0),
+  d_numMerges("theory::bv::slicer::NumMerges", 0),
   d_avgFindDepth("theory::bv::slicer::AverageFindDepth"),
-  d_numAddedEqualities("theory::bv::slicer::NumberOfEqualitiesAdded", Slicer::d_numAddedEqualities)
+  d_numAddedEqualities("theory::bv::slicer::NumEqualitiesAdded", Slicer::d_numAddedEqualities)
 {
   smtStatisticsRegistry()->registerStat(&d_numRepresentatives);
   smtStatisticsRegistry()->registerStat(&d_numSplits);
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index fd9ad0c6a..47f2b9245 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -51,7 +51,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
     d_sharedTermsSet(c),
     d_subtheories(),
     d_subtheoryMap(),
-    d_statistics(getFullInstanceName()),
+    d_statistics(),
     d_staticLearnCache(),
     d_BVDivByZero(),
     d_BVRemByZero(),
@@ -64,7 +64,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
     d_literalsToPropagateIndex(c, 0),
     d_propagatedBy(c),
     d_eagerSolver(NULL),
-    d_abstractionModule(new AbstractionModule(getFullInstanceName())),
+    d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))),
     d_isCoreTheory(false),
     d_calledPreregister(false),
     d_needsLastCallCheck(false),
@@ -130,14 +130,14 @@ void TheoryBV::spendResource(unsigned amount)
   getOutputChannel().spendResource(amount);
 }
 
-TheoryBV::Statistics::Statistics(const std::string &name):
-  d_avgConflictSize(name + "theory::bv::AvgBVConflictSize"),
-  d_solveSubstitutions(name + "theory::bv::NumberOfSolveSubstitutions", 0),
-  d_solveTimer(name + "theory::bv::solveTimer"),
-  d_numCallsToCheckFullEffort(name + "theory::bv::NumberOfFullCheckCalls", 0),
-  d_numCallsToCheckStandardEffort(name + "theory::bv::NumberOfStandardCheckCalls", 0),
-  d_weightComputationTimer(name + "theory::bv::weightComputationTimer"),
-  d_numMultSlice(name + "theory::bv::NumMultSliceApplied", 0)
+TheoryBV::Statistics::Statistics():
+  d_avgConflictSize("theory::bv::AvgBVConflictSize"),
+  d_solveSubstitutions("theory::bv::NumSolveSubstitutions", 0),
+  d_solveTimer("theory::bv::solveTimer"),
+  d_numCallsToCheckFullEffort("theory::bv::NumFullCheckCalls", 0),
+  d_numCallsToCheckStandardEffort("theory::bv::NumStandardCheckCalls", 0),
+  d_weightComputationTimer("theory::bv::weightComputationTimer"),
+  d_numMultSlice("theory::bv::NumMultSliceApplied", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_avgConflictSize);
   smtStatisticsRegistry()->registerStat(&d_solveSubstitutions);
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 1992c0ae3..90bd6275c 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -117,7 +117,7 @@ private:
     IntStat     d_numCallsToCheckStandardEffort;
     TimerStat   d_weightComputationTimer;
     IntStat     d_numMultSlice;
-    Statistics(const std::string &name);
+    Statistics();
     ~Statistics();
   };
 
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index d91eace99..18fadd052 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -50,7 +50,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
       d_infer_exp(c),
       d_term_sk( u ),
       d_notify( *this ),
-      d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes", true),
+      d_equalityEngine(d_notify, c, "theory::datatypes", true),
       d_labels( c ),
       d_selector_apps( c ),
       //d_consEqc( c ),
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 5be4a4601..748c5c1c6 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -100,7 +100,7 @@ TheoryFp::TheoryFp(context::Context *c, context::UserContext *u,
                    const LogicInfo &logicInfo)
     : Theory(THEORY_FP, c, u, out, valuation, logicInfo),
       d_notification(*this),
-      d_equalityEngine(d_notification, c, "theory::fp::TheoryFp", true),
+      d_equalityEngine(d_notification, c, "theory::fp::ee", true),
       d_registeredTerms(u),
       d_conv(u),
       d_expansionRequested(false),
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index a458eec30..9fe3b713f 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -264,7 +264,7 @@ std::string LogicInfo::getLogicString() const {
       if(!isQuantified()) {
         ss << "QF_";
       }
-      if(d_theories[THEORY_ARRAY]) {
+      if(d_theories[THEORY_ARRAYS]) {
         ss << (d_sharingTheories == 1 ? "AX" : "A");
         ++seen;
       }
@@ -385,11 +385,11 @@ void LogicInfo::setLogicString(std::string logicString)
       enableQuantifiers();
     }
     if(!strncmp(p, "AX", 2)) {
-      enableTheory(THEORY_ARRAY);
+      enableTheory(THEORY_ARRAYS);
       p += 2;
     } else {
       if(*p == 'A') {
-        enableTheory(THEORY_ARRAY);
+        enableTheory(THEORY_ARRAYS);
         ++p;
       }
       if(!strncmp(p, "UF", 2)) {
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 0107b80c8..fd64a4ae6 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -39,7 +39,7 @@ TheorySep::TheorySep(context::Context* c, context::UserContext* u, OutputChannel
   Theory(THEORY_SEP, c, u, out, valuation, logicInfo),
   d_lemmas_produced_c(u),
   d_notify(*this),
-  d_equalityEngine(d_notify, c, "theory::sep::TheorySep", true),
+  d_equalityEngine(d_notify, c, "theory::sep::ee", true),
   d_conflict(c, false),
   d_reduce(u),
   d_infer(c),
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 6bafbb0de..71857b7a5 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -49,7 +49,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
   d_var_elim(u),
   d_external(external),
   d_notify(*this),
-  d_equalityEngine(d_notify, c, "theory::sets::TheorySetsPrivate", true),
+  d_equalityEngine(d_notify, c, "theory::sets::ee", true),
   d_conflict(c)
 {
 
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 17551b528..d0b3ec181 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -63,7 +63,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u,
     : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
       RMAXINT(LONG_MAX),
       d_notify( *this ),
-      d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings", true),
+      d_equalityEngine(d_notify, c, "theory::strings", true),
       d_conflict(c, false),
       d_infer(c),
       d_infer_exp(c),
@@ -3995,11 +3995,11 @@ Node TheoryStrings::ppRewrite(TNode atom) {
 
 // Stats
 TheoryStrings::Statistics::Statistics():
-  d_splits("TheoryStrings::NumOfSplitOnDemands", 0),
-  d_eq_splits("TheoryStrings::NumOfEqSplits", 0),
-  d_deq_splits("TheoryStrings::NumOfDiseqSplits", 0),
-  d_loop_lemmas("TheoryStrings::NumOfLoops", 0),
-  d_new_skolems("TheoryStrings::NumOfNewSkolems", 0)
+  d_splits("theory::strings::NumOfSplitOnDemands", 0),
+  d_eq_splits("theory::strings::NumOfEqSplits", 0),
+  d_deq_splits("theory::strings::NumOfDiseqSplits", 0),
+  d_loop_lemmas("theory::strings::NumOfLoops", 0),
+  d_new_skolems("theory::strings::NumOfNewSkolems", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_splits);
   smtStatisticsRegistry()->registerStat(&d_eq_splits);
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 069767968..2ef4f42bf 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -69,8 +69,8 @@ Theory::Theory(TheoryId id,
       d_careGraph(NULL),
       d_quantEngine(NULL),
       d_extTheory(NULL),
-      d_checkTime(getFullInstanceName() + "::checkTime"),
-      d_computeCareGraphTime(getFullInstanceName() + "::computeCareGraphTime"),
+      d_checkTime(getStatsPrefix(id) + "::checkTime"),
+      d_computeCareGraphTime(getStatsPrefix(id) + "::computeCareGraphTime"),
       d_sharedTerms(satContext),
       d_out(&out),
       d_valuation(valuation),
@@ -337,12 +337,6 @@ EntailmentCheckParameters::EntailmentCheckParameters(TheoryId tid)
   : d_tid(tid) {
 }
 
-std::string Theory::getFullInstanceName() const {
-  std::stringstream ss;
-  ss << "theory<" << d_id << ">" << d_instanceName;
-  return ss.str();
-}
-
 EntailmentCheckParameters::~EntailmentCheckParameters(){}
 
 TheoryId EntailmentCheckParameters::getTheoryId() const {
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 0571a67b7..f38cda90a 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -343,13 +343,6 @@ public:
   }
 
   /**
-   * Returns a string that uniquely identifies this theory solver w.r.t. the
-   * SmtEngine.
-   */
-  std::string getFullInstanceName() const;
-
-
-  /**
    * Get the SAT context associated to this Theory.
    */
   context::Context* getSatContext() const {
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index a6c42f584..375027d34 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -2361,12 +2361,12 @@ bool TheoryEngine::useTheoryAlternative(const std::string& name) {
 
 
 TheoryEngine::Statistics::Statistics(theory::TheoryId theory):
-    conflicts(mkName("theory<", theory, ">::conflicts"), 0),
-    propagations(mkName("theory<", theory, ">::propagations"), 0),
-    lemmas(mkName("theory<", theory, ">::lemmas"), 0),
-    requirePhase(mkName("theory<", theory, ">::requirePhase"), 0),
-    flipDecision(mkName("theory<", theory, ">::flipDecision"), 0),
-    restartDemands(mkName("theory<", theory, ">::restartDemands"), 0)
+    conflicts(getStatsPrefix(theory) + "::conflicts", 0),
+    propagations(getStatsPrefix(theory) + "::propagations", 0),
+    lemmas(getStatsPrefix(theory) + "::lemmas", 0),
+    requirePhase(getStatsPrefix(theory) + "::requirePhase", 0),
+    flipDecision(getStatsPrefix(theory) + "::flipDecision", 0),
+    restartDemands(getStatsPrefix(theory) + "::restartDemands", 0)
 {
   smtStatisticsRegistry()->registerStat(&conflicts);
   smtStatisticsRegistry()->registerStat(&propagations);
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 38ddb1246..b3fb8e211 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -47,8 +47,7 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u,
       /* The strong theory solver can be notified by EqualityEngine::init(),
        * so make sure it's initialized first. */
       d_thss(NULL),
-      d_equalityEngine(d_notify, c, instanceName + "theory::uf::TheoryUF",
-                       true),
+      d_equalityEngine(d_notify, c, instanceName + "theory::uf::ee", true),
       d_conflict(c, false),
       d_extensionality_deq(u),
       d_uf_std_skolem(u),
diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp
index 9273f2167..04078ef50 100644
--- a/src/util/statistics.cpp
+++ b/src/util/statistics.cpp
@@ -112,8 +112,8 @@ void StatisticsBase::flushInformation(std::ostream &out) const {
       out << d_prefix << s_regDelim;
     }
     s->flushStat(out);
-    out << std::endl;
   }
+  out << std::endl;
 #endif /* CVC4_STATISTICS_ON */
 }
 
@@ -126,8 +126,8 @@ void StatisticsBase::safeFlushInformation(int fd) const {
       safe_print(fd, s_regDelim);
     }
     s->safeFlushStat(fd);
-    safe_print(fd, "\n");
   }
+  safe_print(fd, "\n");
 #endif /* CVC4_STATISTICS_ON */
 }