1 files changed, 2 insertions, 2 deletions
diff --git a/src/main/command_executor_portfolio.h b/src/main/command_executor_portfolio.h
index ee2b270fb..ce9a80a4e 100644
--- a/src/main/command_executor_portfolio.h
+++ b/src/main/command_executor_portfolio.h
@@ -40,7 +40,7 @@ class CommandExecutorPortfolio : public CommandExecutor {
                                  // not too hard to support this changing
   std::vector<SmtEngine*> d_smts;
   CommandSequence* d_seq;
-  std::vector<Options>& d_threadOptions;
+  OptionsList& d_threadOptions;
   std::vector<ExprManagerMapCollection*> d_vmaps;
 
   int d_lastWinner;
@@ -57,7 +57,7 @@ class CommandExecutorPortfolio : public CommandExecutor {
 public:
   CommandExecutorPortfolio(ExprManager &exprMgr,
                            Options &options,
-                           std::vector<Options>& tOpts);
+                           OptionsList& tOpts);
 
   ~CommandExecutorPortfolio();