diff --git a/src/bin/common_finput.cc b/src/bin/common_finput.cc
index 094004713..fb7298f4d 100644
--- a/src/bin/common_finput.cc
+++ b/src/bin/common_finput.cc
@@ -81,6 +81,10 @@ parse_formula(const std::string& s, spot::ltl::parse_error_list& pel)
 			    false, lenient);
 }
 
+job_processor::job_processor()
+  : abort_run(false)
+{
+}
 
 int
 job_processor::process_string(const std::string& input,
@@ -109,7 +113,7 @@ job_processor::process_stream(std::istream& is,
   int error = 0;
   int linenum = 0;
   std::string line;
-  while (std::getline(is, line))
+  while (!abort_run && std::getline(is, line))
     error |= process_string(line, filename, ++linenum);
   return error;
 }
@@ -133,7 +137,7 @@ job_processor::run()
 {
   int error = 0;
   jobs_t::const_iterator i;
-  for (i = jobs.begin(); i != jobs.end(); ++i)
+  for (i = jobs.begin(); i != jobs.end() && !abort_run; ++i)
     {
       if (!i->file_p)
 	error |= process_string(i->str);
diff --git a/src/bin/common_finput.hh b/src/bin/common_finput.hh
index 397bbf2d9..15cdc82b6 100644
--- a/src/bin/common_finput.hh
+++ b/src/bin/common_finput.hh
@@ -51,7 +51,11 @@ parse_formula(const std::string& s, spot::ltl::parse_error_list& error_list);
 
 class job_processor
 {
+protected:
+  bool abort_run;  // Set to true in process_formula() to abort run().
 public:
+  job_processor();
+
   virtual ~job_processor()
   {
   }
diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc
index 08c7f9855..00fb43591 100644
--- a/src/bin/ltlcross.cc
+++ b/src/bin/ltlcross.cc
@@ -80,6 +80,7 @@ Exit status:\n\
 #define OPT_CSV 4
 #define OPT_DUPS 5
 #define OPT_NOCHECKS 6
+#define OPT_STOP_ERR 7
 
 static const argp_option options[] =
   {
@@ -110,6 +111,9 @@ static const argp_option options[] =
     { "no-checks", OPT_NOCHECKS, 0, 0,
       "do not perform any sanity checks (negated formulas "
       "will not be translated)", 0 },
+    { "stop-on-error", OPT_STOP_ERR, 0, 0,
+      "stop on first execution error or failure to pass"
+      " sanity checks (timeouts are OK)", 0 },
     /**************************************************/
     { 0, 0, 0, 0, "State-space generation:", 5 },
     { "states", OPT_STATES, "INT", 0,
@@ -143,6 +147,7 @@ const char* csv_output = 0;
 bool want_stats = false;
 bool allow_dups = false;
 bool no_checks = false;
+bool stop_on_error = false;
 
 std::vector<char*> translators;
 bool global_error_flag = false;
@@ -295,6 +300,9 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_STATES:
       states = to_pos_int(arg);
       break;
+    case OPT_STOP_ERR:
+      stop_on_error = true;
+      break;
     default:
       return ARGP_ERR_UNKNOWN;
     }
@@ -964,6 +972,9 @@ namespace
 	}
       delete statespace;
       std::cerr << std::endl;
+
+      // Shall we stop processing formulas now?
+      abort_run = global_error_flag && stop_on_error;
       return 0;
     }
   };