+++ src/lib/glucose/core/Solver.cc	2015-08-28 17:42:26.782504938 +0200
@@ -164,6 +164,23 @@ Solver::~Solver()
 {
 }
 
+void Solver::copyFrom(Solver &s)
+{
+	/* "copy" variables from s */
+	for (int i=0; i < s.nVars(); i++) {
+		newVar();
+	}
+
+	/* TODO copy clauses from s */
+	for (int i=0; i < s.nClauses(); i++) {
+		Clause &old_clause = s.ca[s.clauses[i]];
+		vec<Lit> lits;
+		for (int j=0; j < old_clause.size(); j++) {
+			lits.push(old_clause[j]);
+		}
+		addClause(lits);
+	}
+}
 
 /****************************************************************
  Set the incremental mode
+++ src/lib/glucose/core/Solver.h	2015-08-28 17:35:27.393544963 +0200
@@ -51,6 +51,8 @@ public:
     Solver();
     virtual ~Solver();
 
+	 void    copyFrom(Solver &s);
+
     // Problem specification:
     //
     Var     newVar    (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
