From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 14 Nov 2012 20:59:00 +0000 (+0000)
Subject: Quantifiers enabled with portfolio, closing bug 423.
X-Git-Tag: cvc5-1.0.0~7602
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b273e586629c5759dc88cd962e52a89f65b674a7;p=cvc5.git

Quantifiers enabled with portfolio, closing bug 423.
---

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