Quantifiers enabled with portfolio, closing bug 423.

diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 883989fb01e785ebfb8aeccd7f3a6dbc157ff18d..a4a0fcad3282f74da0a5196db05c5c80e57bbcdd 100644 (file)
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -191,17 +191,6 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
     return CommandExecutor::doCommandSingleton(cmd);
   } else if(mode == 1) {               // portfolio
 
-    // If quantified, stay sequential
-    LogicInfo logicInfo = d_smts[0]->getLogicInfo();
-    logicInfo.lock();
-    if(logicInfo.isQuantified()) {
-      if(d_options[options::fallbackSequential])
-        return CommandExecutor::doCommandSingleton(cmd);
-      else
-        throw Exception("Quantified formulas are (currenltly) unsupported in portfolio mode.\n"
-                        "Please see option --fallback-sequential to make this a soft error.");
-    }
-
     d_seq->addCommand(cmd->clone());
 
     // We currently don't support changing number of threads for each