Removing unused bool members in command.cpp. Also initializes a bool member. (#2321)

1 files changed, 14 insertions, 19 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)