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").

1 files changed, 2 insertions, 2 deletions

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);