Merge pull request #48 from kbansal/segfaultfix

Segfaultfix

4 files changed, 26 insertions, 3 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())
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index e54c8d174..b6238460b 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -135,6 +135,15 @@ Solver::Solver(CVC4::context::Context* c) :
   , progress_estimate  (0)
   , remove_satisfied   (true)
 
+  , ca                 ()
+
+  // even though these are temporaries and technically should be set
+  // before calling, lets intialize them. this will reduces chances of
+  // non-determinism in portfolio (parallel) solver if variables are
+  // being (incorrectly) used without initialization.
+  , seen(),  analyze_stack(), analyze_toclear(), add_tmp()
+  , max_learnts(0.0), learntsize_adjust_confl(0.0), learntsize_adjust_cnt(0)
+
     // Resource constraints:
     //
   , conflict_budget    (-1)
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 79aa04fc6..4c784ce6f 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -194,6 +194,10 @@ AlgebraicSolver::AlgebraicSolver(context::Context* c, TheoryBV* bv)
   , d_isDifficult(c, false)
   , d_budget(options::bitvectorAlgebraicBudget())
   , d_explanations()
+  , d_inputAssertions()
+  , d_ids()
+  , d_numSolved(0)
+  , d_numCalls(0)
   , d_ctx(new context::Context())
   , d_quickXplain(options::bitvectorQuickXplain() ? new QuickXPlain("alg", d_quickSolver) : NULL)
   , d_statistics()
@@ -642,7 +646,7 @@ bool AlgebraicSolver::useHeuristic() {
   if (d_numCalls == 0)
     return true;
   
-  double success_rate = d_numSolved/d_numCalls;
+  double success_rate = double(d_numSolved)/double(d_numCalls);
   d_statistics.d_useHeuristic.setData(success_rate);
   return success_rate > 0.8;
 }
diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h
index 4ce02cae1..03588a78f 100644
--- a/src/theory/bv/bv_subtheory_algebraic.h
+++ b/src/theory/bv/bv_subtheory_algebraic.h
@@ -174,8 +174,8 @@ class AlgebraicSolver : public SubtheorySolver {
   std::vector<Node> d_explanations; /**< explanations for assertions indexed by assertion id */
   TNodeSet d_inputAssertions;   /**< assertions in current context (for debugging purposes only) */
   NodeIdMap d_ids;              /**< map from assertions to ids */
-  double d_numSolved;
-  double d_numCalls;
+  uint64_t d_numSolved;
+  uint64_t d_numCalls;
 
   context::Context* d_ctx;
   QuickXPlain* d_quickXplain;   /**< separate quickXplain module as it can reuse the current SAT solver */