9 files changed, 39 insertions, 45 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 4a21be3e..9211f485 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -23,7 +23,6 @@
 #include "UserSearcher.h"
 #include "ExecutorTimerInfo.h"
 
-#include "../Solver/SolverStats.h"
 
 #include "klee/ExecutionState.h"
 #include "klee/Expr.h"
@@ -47,6 +46,7 @@
 #include "klee/Internal/Support/FloatEvaluation.h"
 #include "klee/Internal/System/Time.h"
 #include "klee/Internal/System/MemoryUsage.h"
+#include "klee/SolverStats.h"
 
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
 #include "llvm/IR/Function.h"
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index 4633a5c5..2e107fb3 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -18,13 +18,13 @@
 #include "klee/Internal/Support/ModuleUtil.h"
 #include "klee/Internal/System/Time.h"
 #include "klee/Internal/Support/ErrorHandling.h"
+#include "klee/SolverStats.h"
 
 #include "CallPathManager.h"
 #include "CoreStats.h"
 #include "Executor.h"
 #include "MemoryManager.h"
 #include "UserSearcher.h"
-#include "../Solver/SolverStats.h"
 
 #if LLVM_VERSION_CODE > LLVM_VERSION(3, 2)
 #include "llvm/IR/BasicBlock.h"
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index 854f6d52..e914cb80 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -331,6 +331,8 @@ namespace {
                                         MaxErrors(~0u),
                                         NumErrors(0) {}
 
+    virtual ~ParserImpl();
+
     /// Initialize - Initialize the parsing state. This must be called
     /// prior to the start of parsing.
     void Initialize() {
@@ -1561,6 +1563,36 @@ void ParserImpl::Error(const char *Message, const Token &At) {
   llvm::errs() << '\n';
 }
 
+ParserImpl::~ParserImpl() {
+  // Free identifiers
+  //
+  // Note the Identifiers are not disjoint across the symbol
+  // tables so we need to keep track of what has freed to
+  // avoid doing a double free.
+  std::set<const Identifier*> freedNodes;
+  for (IdentifierTabTy::iterator pi = IdentifierTab.begin(),
+                                 pe = IdentifierTab.end();
+       pi != pe; ++pi) {
+    const Identifier* id = pi->second;
+    if (freedNodes.insert(id).second)
+      delete id;
+  }
+  for (ExprSymTabTy::iterator pi = ExprSymTab.begin(),
+                              pe = ExprSymTab.end();
+       pi != pe; ++pi) {
+    const Identifier* id = pi->first;
+    if (freedNodes.insert(id).second)
+      delete id;
+  }
+  for (VersionSymTabTy::iterator pi = VersionSymTab.begin(),
+                                 pe = VersionSymTab.end();
+       pi != pe; ++pi) {
+    const Identifier* id = pi->first;
+    if (freedNodes.insert(id).second)
+      delete id;
+  }
+}
+
 // AST API
 // FIXME: Move out of parser.
 
diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp
index cfe08a96..1a6dce52 100644
--- a/lib/Solver/CachingSolver.cpp
+++ b/lib/Solver/CachingSolver.cpp
@@ -15,7 +15,7 @@
 #include "klee/IncompleteSolver.h"
 #include "klee/SolverImpl.h"
 
-#include "SolverStats.h"
+#include "klee/SolverStats.h"
 
 #include <ciso646>
 #ifdef _LIBCPP_VERSION
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index fb07a6ec..8627b2ac 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -18,7 +18,7 @@
 #include "klee/util/ExprVisitor.h"
 #include "klee/Internal/ADT/MapOfSets.h"
 
-#include "SolverStats.h"
+#include "klee/SolverStats.h"
 
 #include "klee/Internal/Support/ErrorHandling.h"
 
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 4bd0145f..2f51c2b9 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -12,9 +12,9 @@
 #include "klee/Expr.h"
 #include "klee/Solver.h"
 #include "klee/util/Bits.h"
+#include "klee/SolverStats.h"
 
 #include "ConstantDivision.h"
-#include "SolverStats.h"
 
 #include "llvm/Support/CommandLine.h"
 
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 341ca17c..6f4bbc5b 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -10,7 +10,6 @@
 #include "klee/Solver.h"
 #include "klee/SolverImpl.h"
 
-#include "SolverStats.h"
 #include "STPBuilder.h"
 #include "MetaSMTBuilder.h"
 
@@ -23,6 +22,7 @@
 #include "klee/Internal/Support/Timer.h"
 #include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/CommandLine.h"
+#include "klee/SolverStats.h"
 
 #define vc_bvBoolExtract IAMTHESPAWNOFSATAN
 
diff --git a/lib/Solver/SolverStats.cpp b/lib/Solver/SolverStats.cpp
index 9d6963cf..4b9c69c8 100644
--- a/lib/Solver/SolverStats.cpp
+++ b/lib/Solver/SolverStats.cpp
@@ -7,7 +7,7 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "SolverStats.h"
+#include "klee/SolverStats.h"
 
 using namespace klee;
 
diff --git a/lib/Solver/SolverStats.h b/lib/Solver/SolverStats.h
deleted file mode 100644
index a38c9826..00000000
--- a/lib/Solver/SolverStats.h
+++ /dev/null
@@ -1,38 +0,0 @@
-//===-- SolverStats.h -------------------------------------------*- C++ -*-===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef KLEE_SOLVERSTATS_H
-#define KLEE_SOLVERSTATS_H
-
-#include "klee/Statistic.h"
-
-namespace klee {
-namespace stats {
-
-  extern Statistic cexCacheTime;
-  extern Statistic queries;
-  extern Statistic queriesInvalid;
-  extern Statistic queriesValid;
-  extern Statistic queryCacheHits;
-  extern Statistic queryCacheMisses;
-  extern Statistic queryCexCacheHits;
-  extern Statistic queryCexCacheMisses;
-  extern Statistic queryConstructTime;
-  extern Statistic queryConstructs;
-  extern Statistic queryCounterexamples;
-  extern Statistic queryTime;
-  
-#ifdef DEBUG
-  extern Statistic arrayHashTime;
-#endif
-
-}
-}
-
-#endif