summaryrefslogtreecommitdiff
path: root/src/main
diff options
context:
space:
mode:
Diffstat (limited to 'src/main')
-rw-r--r--src/main/command_executor_portfolio.cpp8
1 files changed, 6 insertions, 2 deletions
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 25b160d6c..948e05ad3 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -197,9 +197,13 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
// mode = 2 : run _only_ the lastWinner thread, not saving the
// command
+ if( dynamic_cast<CheckSynthCommand*>(cmd) != NULL ){
+ // sygus not supported in portfolio : FIXME: can support once datatypes exportTo is supported
+ return CommandExecutor::doCommandSingleton(cmd);
+ }
+
if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
- dynamic_cast<QueryCommand*>(cmd) != NULL ||
- dynamic_cast<CheckSynthCommand*>(cmd) != NULL) {
+ dynamic_cast<QueryCommand*>(cmd) != NULL ) {
mode = 1;
} else if(dynamic_cast<GetValueCommand*>(cmd) != NULL ||
dynamic_cast<GetAssignmentCommand*>(cmd) != NULL ||
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback