diff options
Diffstat (limited to 'src/main')
| -rw-r--r-- | src/main/portfolio.cpp | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp index 757b6cd3c..abe27eb06 100644 --- a/src/main/portfolio.cpp +++ b/src/main/portfolio.cpp @@ -20,6 +20,7 @@ #include <boost/exception_ptr.hpp> #include "smt/smt_engine.h" +#include "util/output.h" #include "util/result.h" #include "util/statistics_registry.h" #include "options/options.h" @@ -92,8 +93,17 @@ std::pair<int, S> runPortfolio(int numThreads, threads[t] = boost::thread(boost::bind(runThread<S>, t, threadFns[t], boost::ref(threads_returnValue[t]) ) ); + #endif /* BOOST_HAS_THREAD_ATTR */ + if(Chat.isOn()) { + void *stackaddr; + size_t stacksize; + pthread_attr_t attr; + pthread_getattr_np(threads[t].native_handle(), &attr); + pthread_attr_getstack(&attr, &stackaddr, &stacksize); + Chat() << "Created worker thread " << t << " with stack size " << stacksize << std::endl; + } } if(not driverFn.empty()) |