3 files changed, 17 insertions, 26 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 2805d8793..3d838d21c 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -387,10 +387,8 @@ std::string PopCommand::getCommandName() const { return "pop"; }
 /* -------------------------------------------------------------------------- */
 
 CheckSatCommand::CheckSatCommand() : d_expr() {}
-CheckSatCommand::CheckSatCommand(const Expr& expr, bool inUnsatCore)
-    : d_expr(expr), d_inUnsatCore(inUnsatCore)
-{
-}
+
+CheckSatCommand::CheckSatCommand(const Expr& expr) : d_expr(expr) {}
 
 Expr CheckSatCommand::getExpr() const { return d_expr; }
 void CheckSatCommand::invoke(SmtEngine* smtEngine)
@@ -422,15 +420,15 @@ void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const
 Command* CheckSatCommand::exportTo(ExprManager* exprManager,
                                    ExprManagerMapCollection& variableMap)
 {
-  CheckSatCommand* c = new CheckSatCommand(
-      d_expr.exportTo(exprManager, variableMap), d_inUnsatCore);
+  CheckSatCommand* c =
+      new CheckSatCommand(d_expr.exportTo(exprManager, variableMap));
   c->d_result = d_result;
   return c;
 }
 
 Command* CheckSatCommand::clone() const
 {
-  CheckSatCommand* c = new CheckSatCommand(d_expr, d_inUnsatCore);
+  CheckSatCommand* c = new CheckSatCommand(d_expr);
   c->d_result = d_result;
   return c;
 }
@@ -441,14 +439,10 @@ std::string CheckSatCommand::getCommandName() const { return "check-sat"; }
 /* class CheckSatAssumingCommand                                              */
 /* -------------------------------------------------------------------------- */
 
-CheckSatAssumingCommand::CheckSatAssumingCommand(Expr term) : d_terms()
-{
-  d_terms.push_back(term);
-}
+CheckSatAssumingCommand::CheckSatAssumingCommand(Expr term) : d_terms({term}) {}
 
-CheckSatAssumingCommand::CheckSatAssumingCommand(const std::vector<Expr>& terms,
-                                                 bool inUnsatCore)
-    : d_terms(terms), d_inUnsatCore(inUnsatCore)
+CheckSatAssumingCommand::CheckSatAssumingCommand(const std::vector<Expr>& terms)
+    : d_terms(terms)
 {
 }
 
@@ -496,16 +490,14 @@ Command* CheckSatAssumingCommand::exportTo(
   {
     exportedTerms.push_back(e.exportTo(exprManager, variableMap));
   }
-  CheckSatAssumingCommand* c =
-      new CheckSatAssumingCommand(exportedTerms, d_inUnsatCore);
+  CheckSatAssumingCommand* c = new CheckSatAssumingCommand(exportedTerms);
   c->d_result = d_result;
   return c;
 }
 
 Command* CheckSatAssumingCommand::clone() const
 {
-  CheckSatAssumingCommand* c =
-      new CheckSatAssumingCommand(d_terms, d_inUnsatCore);
+  CheckSatAssumingCommand* c = new CheckSatAssumingCommand(d_terms);
   c->d_result = d_result;
   return c;
 }
@@ -1779,7 +1771,10 @@ std::string GetSynthSolutionCommand::getCommandName() const
 /* class GetQuantifierEliminationCommand                                      */
 /* -------------------------------------------------------------------------- */
 
-GetQuantifierEliminationCommand::GetQuantifierEliminationCommand() : d_expr() {}
+GetQuantifierEliminationCommand::GetQuantifierEliminationCommand()
+    : d_expr(), d_doFull(true)
+{
+}
 GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(
     const Expr& expr, bool doFull)
     : d_expr(expr), d_doFull(doFull)
diff --git a/src/smt/command.h b/src/smt/command.h
index 08f83e7a9..be6d84305 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -552,7 +552,7 @@ class CVC4_PUBLIC CheckSatCommand : public Command
 {
  public:
   CheckSatCommand();
-  CheckSatCommand(const Expr& expr, bool inUnsatCore = true);
+  CheckSatCommand(const Expr& expr);
 
   Expr getExpr() const;
   Result getResult() const;
@@ -566,7 +566,6 @@ class CVC4_PUBLIC CheckSatCommand : public Command
  private:
   Expr d_expr;
   Result d_result;
-  bool d_inUnsatCore;
 }; /* class CheckSatCommand */
 
 /**
@@ -578,8 +577,7 @@ class CVC4_PUBLIC CheckSatAssumingCommand : public Command
 {
  public:
   CheckSatAssumingCommand(Expr term);
-  CheckSatAssumingCommand(const std::vector<Expr>& terms,
-                          bool inUnsatCore = true);
+  CheckSatAssumingCommand(const std::vector<Expr>& terms);
 
   const std::vector<Expr>& getTerms() const;
   Result getResult() const;
@@ -593,7 +591,6 @@ class CVC4_PUBLIC CheckSatAssumingCommand : public Command
  private:
   std::vector<Expr> d_terms;
   Result d_result;
-  bool d_inUnsatCore;
 }; /* class CheckSatAssumingCommand */
 
 class CVC4_PUBLIC QueryCommand : public Command
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index fbe6bcd63..f9ea2f1ac 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4647,8 +4647,7 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
       }
       else
       {
-        Dump("benchmark") << CheckSatAssumingCommand(d_assumptions,
-                                                     inUnsatCore);
+        Dump("benchmark") << CheckSatAssumingCommand(d_assumptions);
       }
     }