Remove option --continued-execution. (#3189)

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 7e46b163b99d1b0ac0ca8e46f37957a2675e94b0..241ca2b8f9e57ffb460e61c04a9532a94e793a82 100644 (file)
--- 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 7af8a6fdbc4bd0ffeb470fcd59ab57148532a5d8..d0fce8d00d54d7184731dec487021ff92d66d95b 100644 (file)
--- 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 7230f544d0fa2261010238cddca167d127ac02f4..c6d92c97b87d99ae8e444b47f361fd9f0ddc7db0 100644 (file)
--- 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 9f75e9426e9ed11ade88c75f6867e737213d96ba..71c96467815577cb935d22204a6c79c170b163df 100644 (file)
--- 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 020350c496751b265524b2af4062bf737f861254..0d26c60b9567f90135d17347d4f74445bab09f11 100644 (file)
--- 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 39f2eb1408122d29221170a399b5c0f78b1b5de3..43b44b93e1dec07461a160ac847a7f3f83962b9b 100644 (file)
--- 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 78f47993f9e99e5dd14a43f51ee79c80b6947a7d..1827d902cfcb6d7eff659fe5896bfa9830fd6f98 100644 (file)
--- 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") {