3 files changed, 42 insertions, 8 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index e1547d23d..2adad092e 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -377,9 +377,13 @@ command returns [CVC4::Command* cmd = NULL]
     { cmd = new GetAssignmentCommand(); }
   | /* assertion */
     ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    { PARSER_STATE->clearLastNamedTerm(); }
     term[expr, expr2]
-    { cmd = new AssertCommand(expr, /* inUnsatCore */ PARSER_STATE->lastNamedTerm() == expr);
-      PARSER_STATE->setLastNamedTerm(Expr());
+    { bool inUnsatCore = PARSER_STATE->lastNamedTerm().first == expr;
+      cmd = new AssertCommand(expr, inUnsatCore);
+      if(inUnsatCore) {
+        PARSER_STATE->registerUnsatCoreName(PARSER_STATE->lastNamedTerm());
+      }
     }
   | /* check-sat */
     CHECKSAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
@@ -398,7 +402,7 @@ command returns [CVC4::Command* cmd = NULL]
     { cmd = new GetProofCommand(); }
   | /* get-unsat-core */
     GET_UNSAT_CORE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { cmd = new GetUnsatCoreCommand(); }
+    { cmd = new GetUnsatCoreCommand(PARSER_STATE->getUnsatCoreNames()); }
   | /* push */
     PUSH_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     ( k=INTEGER_LITERAL
@@ -407,11 +411,13 @@ command returns [CVC4::Command* cmd = NULL]
           cmd = new EmptyCommand();
         } else if(n == 1) {
           PARSER_STATE->pushScope();
+          PARSER_STATE->pushUnsatCoreNameScope();
           cmd = new PushCommand();
         } else {
           CommandSequence* seq = new CommandSequence();
           do {
             PARSER_STATE->pushScope();
+            PARSER_STATE->pushUnsatCoreNameScope();
             Command* c = new PushCommand();
             c->setMuted(n > 1);
             seq->addCommand(c);
@@ -434,11 +440,13 @@ command returns [CVC4::Command* cmd = NULL]
         if(n == 0) {
           cmd = new EmptyCommand();
         } else if(n == 1) {
+          PARSER_STATE->popUnsatCoreNameScope();
           PARSER_STATE->popScope();
           cmd = new PopCommand();
         } else {
           CommandSequence* seq = new CommandSequence();
           do {
+            PARSER_STATE->popUnsatCoreNameScope();
             PARSER_STATE->popScope();
             Command* c = new PopCommand();
             c->setMuted(n > 1);
@@ -1213,7 +1221,7 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
       // define it
       Expr func = PARSER_STATE->mkFunction(name, expr.getType());
       // remember the last term to have been given a :named attribute
-      PARSER_STATE->setLastNamedTerm(expr);
+      PARSER_STATE->setLastNamedTerm(expr, name);
       // bind name to expr with define-fun
       Command* c =
         new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr);
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index fecccfa44..21b6a1e5b 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -31,6 +31,7 @@ namespace parser {
 Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
   Parser(exprManager,input,strictMode,parseOnly),
   d_logicSet(false) {
+  d_unsatCoreNames.push(std::map<Expr, std::string>());
   if( !strictModeEnabled() ) {
     addTheory(Smt2::THEORY_CORE);
   }
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 7ecd2e5b1..290bbc975 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -24,7 +24,10 @@
 #include "theory/logic_info.h"
 #include "util/abstract_value.h"
 
+#include <string>
 #include <sstream>
+#include <utility>
+#include <stack>
 
 namespace CVC4 {
 
@@ -54,7 +57,9 @@ private:
   bool d_logicSet;
   LogicInfo d_logic;
   std::hash_map<std::string, Kind, StringHashFunction> operatorKindMap;
-  Expr d_lastNamedTerm;
+  std::pair<Expr, std::string> d_lastNamedTerm;
+  // this is a user-context stack
+  std::stack< std::map<Expr, std::string> > d_unsatCoreNames;
 
 protected:
   Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
@@ -106,14 +111,34 @@ public:
 
   void includeFile(const std::string& filename);
 
-  void setLastNamedTerm(Expr e) {
-    d_lastNamedTerm = e;
+  void setLastNamedTerm(Expr e, std::string name) {
+    d_lastNamedTerm = std::make_pair(e, name);
   }
 
-  Expr lastNamedTerm() {
+  void clearLastNamedTerm() {
+    d_lastNamedTerm = std::make_pair(Expr(), "");
+  }
+
+  std::pair<Expr, std::string> lastNamedTerm() {
     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;