diff --git a/include/sharpSAT/instance.h b/include/sharpSAT/instance.h
index 1cf3996..2486f3d 100644
--- a/include/sharpSAT/instance.h
+++ b/include/sharpSAT/instance.h
@@ -133,6 +133,9 @@ class Instance {
   //! Literal-related data, indexed by LiteralID.
   LiteralIndexedVector<Literal> literals_;
 
+  //! Used in implicitBCP...
+  LiteralIndexedVector<unsigned char> viewed_lits_;
+
   /*!
    * Non-unit non-binary clauses, in which a literal appears.
    *
diff --git a/src/instance.cpp b/src/instance.cpp
index d8af7ec..472ae43 100644
--- a/src/instance.cpp
+++ b/src/instance.cpp
@@ -137,6 +137,8 @@ void Instance::compactVariables() {
   occurrence_lists_.resize(variables_.size());
   literals_.clear();
   literals_.resize(variables_.size());
+  viewed_lits_.clear();
+  viewed_lits_.resize(variables_.size(),0);
   literal_values_.clear();
   literal_values_.resize(variables_.size(), TriValue::X_TRI);
 
@@ -305,6 +307,9 @@ void Instance::initialize(
 
   literals_.clear();
   literals_.resize(nVars + 1);
+
+  viewed_lits_.clear();
+  viewed_lits_.resize(nVars + 1,0);
 }
 
 
diff --git a/src/solver.cpp b/src/solver.cpp
index bf0f439..585e0b3 100644
--- a/src/solver.cpp
+++ b/src/solver.cpp
@@ -492,9 +492,7 @@ bool Solver::BCP(size_t start_at_stack_ofs) {
 
 // this is IBCP 30.08
 bool Solver::implicitBCP() {
-	static vector<LiteralID> test_lits(num_variables());
-	static LiteralIndexedVector<unsigned char> viewed_lits(num_variables() + 1,
-			0);
+	vector<LiteralID> test_lits;
 
 	unsigned stack_ofs = stack_.top().literal_stack_ofs();
 	unsigned num_curr_lits = 0;
@@ -505,9 +503,9 @@ bool Solver::implicitBCP() {
 			for (auto cl_ofs : occurrence_lists_[it->neg()])
 				if (!isSatisfied(cl_ofs)) {
 					for (auto lt = beginOf(cl_ofs); *lt != SENTINEL_LIT; lt++)
-						if (isActive(*lt) && !viewed_lits[lt->neg()]) {
+						if (isActive(*lt) && !viewed_lits_[lt->neg()]) {
 							test_lits.push_back(lt->neg());
-							viewed_lits[lt->neg()] = true;
+							viewed_lits_[lt->neg()] = true;
 
 						}
 				}
@@ -515,7 +513,7 @@ bool Solver::implicitBCP() {
 		num_curr_lits = literal_stack_.size() - stack_ofs;
 		stack_ofs = literal_stack_.size();
 		for (auto jt = test_lits.begin(); jt != test_lits.end(); jt++)
-			viewed_lits[*jt] = false;
+			viewed_lits_[*jt] = false;
 
 		vector<float> scores;
 		scores.clear();