summaryrefslogtreecommitdiff
path: root/src/main/command_executor_portfolio.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/main/command_executor_portfolio.cpp')
-rw-r--r--src/main/command_executor_portfolio.cpp11
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback