From b273e586629c5759dc88cd962e52a89f65b674a7 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 14 Nov 2012 20:59:00 +0000
Subject: [PATCH] Quantifiers enabled with portfolio, closing bug 423.

---
 src/main/command_executor_portfolio.cpp | 11 -----------
 1 file changed, 11 deletions(-)

diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 883989fb0..a4a0fcad3 100644
--- 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
-- 
2.30.2