1 files changed, 0 insertions, 18 deletions
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 46f1c631b..9614c5524 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -61,8 +61,6 @@ private:
   LogicInfo d_logic;
   std::unordered_map<std::string, Kind> operatorKindMap;
   std::pair<Expr, std::string> d_lastNamedTerm;
-  // this is a user-context stack
-  std::stack< std::map<Expr, std::string> > d_unsatCoreNames;
   // for sygus
   std::vector<Expr> d_sygusVars, d_sygusConstraints, d_sygusFunSymbols;
   std::map< Expr, bool > d_sygusVarPrimed;
@@ -156,22 +154,6 @@ public:
     return d_lastNamedTerm;
   }
 
-  void pushUnsatCoreNameScope() {
-    d_unsatCoreNames.push(d_unsatCoreNames.top());
-  }
-
-  void popUnsatCoreNameScope() {
-    d_unsatCoreNames.pop();
-  }
-
-  void registerUnsatCoreName(std::pair<Expr, std::string> name) {
-    d_unsatCoreNames.top().insert(name);
-  }
-
-  std::map<Expr, std::string> getUnsatCoreNames() {
-    return d_unsatCoreNames.top();
-  }
-
   bool isAbstractValue(const std::string& name) {
     return name.length() >= 2 && name[0] == '@' && name[1] != '0' &&
       name.find_first_not_of("0123456789", 1) == std::string::npos;