From 044891b406eb3ee143403ad8fecd7acb99d17ecb Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 14 Aug 2019 13:12:19 -0700
Subject: [PATCH] Remove option --continued-execution. (#3189)

---
 src/main/command_executor.cpp            | 10 ++++++----
 src/main/driver_unified.cpp              |  6 ++++--
 src/options/didyoumean_test.cpp          |  1 -
 src/options/main_options.toml            | 10 ----------
 src/options/options.h                    |  1 -
 src/options/options_public_functions.cpp |  4 ----
 src/smt/smt_engine.cpp                   |  7 +------
 7 files changed, 11 insertions(+), 28 deletions(-)

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 7e46b163b..241ca2b8f 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -89,9 +89,10 @@ bool CommandExecutor::doCommand(Command* cmd)
     // assume no error
     bool status = true;
 
-    for(CommandSequence::iterator subcmd = seq->begin();
-        (status || d_options.getContinuedExecution()) && subcmd != seq->end();
-        ++subcmd) {
+    for (CommandSequence::iterator subcmd = seq->begin();
+         status && subcmd != seq->end();
+         ++subcmd)
+    {
       status = doCommand(*subcmd);
     }
 
@@ -183,7 +184,8 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
       }
       for (const auto& getterCommand : getterCommands) {
         status = doCommandSingleton(getterCommand.get());
-        if (!status && !d_options.getContinuedExecution()) {
+        if (!status)
+        {
           break;
         }
       }
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 7af8a6fdb..d0fce8d00 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -362,7 +362,8 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       int needReset = 0;
       // true if one of the commands was interrupted
       bool interrupted = false;
-      while (status || opts.getContinuedExecution()) {
+      while (status)
+      {
         if (interrupted) {
           (*opts.getOut()) << CommandInterrupted();
           break;
@@ -515,7 +516,8 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         replayParser->useDeclarationsFrom(parser.get());
       }
       bool interrupted = false;
-      while(status || opts.getContinuedExecution()) {
+      while (status)
+      {
         if (interrupted) {
           (*opts.getOut()) << CommandInterrupted();
           pExecutor->reset();
diff --git a/src/options/didyoumean_test.cpp b/src/options/didyoumean_test.cpp
index 7230f544d..c6d92c97b 100644
--- a/src/options/didyoumean_test.cpp
+++ b/src/options/didyoumean_test.cpp
@@ -734,7 +734,6 @@ set<string> getOptionStrings() {
       "incremental-parallel",
       "no-incremental-parallel",
       "no-interactive-prompt",
-      "continued-execution",
       "immediate-exit",
       "segv-spin",
       "no-segv-spin",
diff --git a/src/options/main_options.toml b/src/options/main_options.toml
index 9f75e9426..71c964678 100644
--- a/src/options/main_options.toml
+++ b/src/options/main_options.toml
@@ -162,16 +162,6 @@ header = "options/main_options.h"
   read_only  = true
   help       = "interactive prompting while in interactive mode"
 
-[[option]]
-  name       = "continuedExecution"
-  category   = "regular"
-  long       = "continued-execution"
-  type       = "bool"
-  default    = "false"
-  links      = ["--interactive", "--no-interactive-prompt"]
-  read_only  = true
-  help       = "continue executing commands, even on error"
-
 [[option]]
   name       = "segvSpin"
   category   = "regular"
diff --git a/src/options/options.h b/src/options/options.h
index 020350c49..0d26c60b9 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -198,7 +198,6 @@ public:
   InstFormatMode getInstFormatMode() const;
   OutputLanguage getOutputLanguage() const;
   bool getCheckProofs() const;
-  bool getContinuedExecution() const;
   bool getDumpInstantiations() const;
   bool getDumpModels() const;
   bool getDumpProofs() const;
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index 39f2eb140..43b44b93e 100644
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -54,10 +54,6 @@ bool Options::getCheckProofs() const{
   return (*this)[options::checkProofs];
 }
 
-bool Options::getContinuedExecution() const{
-  return (*this)[options::continuedExecution];
-}
-
 bool Options::getDumpInstantiations() const{
   return (*this)[options::dumpInstantiations];
 }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 78f47993f..1827d902c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2438,12 +2438,7 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const {
     }
     return SExpr(stats);
   } else if(key == "error-behavior") {
-    // immediate-exit | continued-execution
-    if( options::continuedExecution() || options::interactive() ) {
-      return SExpr(SExpr::Keyword("continued-execution"));
-    } else {
-      return SExpr(SExpr::Keyword("immediate-exit"));
-    }
+    return SExpr(SExpr::Keyword("immediate-exit"));
   } else if(key == "name") {
     return SExpr(Configuration::getName());
   } else if(key == "version") {
-- 
2.30.2