diff options
Diffstat (limited to 'src/main/driver_unified.cpp')
-rw-r--r-- | src/main/driver_unified.cpp | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index d1baaa2e9..bf66629dd 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -108,6 +108,10 @@ int runCvc4(int argc, char* argv[], Options& opts) { ! opts[options::threadArgv].empty() ) { throw OptionException("Thread options cannot be used with sequential CVC4. Please build and use the portfolio binary `pcvc4'."); } +# else + if( opts[options::checkProofs] ) { + throw OptionException("Cannot run portfolio in check-proofs mode."); + } # endif progName = opts[options::binary_name].c_str(); @@ -201,8 +205,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { << "Notice: ...the experimental --incremental-parallel option.\n"; exprMgr = new ExprManager(opts); pExecutor = new CommandExecutor(*exprMgr, opts); - } - else { + } else { exprMgr = new ExprManager(threadOpts[0]); pExecutor = new CommandExecutorPortfolio(*exprMgr, opts, threadOpts); } |