diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-11-14 20:59:00 +0000 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-11-14 20:59:00 +0000 |
| commit | b273e586629c5759dc88cd962e52a89f65b674a7 (patch) | |
| tree | fb4ad5fc6e6649e7798f862df5b150a7e74ef5a4 | |
| parent | 8c6c93e0b65e67046ed654886b1294dcc6667687 (diff) | |
Quantifiers enabled with portfolio, closing bug 423.
| -rw-r--r-- | src/main/command_executor_portfolio.cpp | 11 |
1 files changed, 0 insertions, 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 |