5 files changed, 18 insertions, 8 deletions
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index f1338864..9e829182 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -224,8 +224,8 @@ static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int fir
     sat_solver_setnvars(pSat, pCnf->nVars);
     if ( RunId >= 0 )
     {
-        pSat->RunId = RunId;
-        pSat->pFuncStop = Wla_CallBackToStop;
+        sat_solver_set_runid( pSat, RunId );
+        sat_solver_set_stop_func( pSat, Wla_CallBackToStop );
     }
 
     for (i = 0; i < pCnf->nClauses; i++) 
diff --git a/src/proof/pdr/pdrCnf.c b/src/proof/pdr/pdrCnf.c
index e0f1641c..3b28c3c8 100644
--- a/src/proof/pdr/pdrCnf.c
+++ b/src/proof/pdr/pdrCnf.c
@@ -370,8 +370,8 @@ static inline sat_solver * Pdr_ManNewSolver1( sat_solver * pSat, Pdr_Man_t * p,
     }
     pSat = (sat_solver *)Cnf_DataWriteIntoSolverInt( pSat, p->pCnf1, 1, fInit );
     sat_solver_set_runtime_limit( pSat, p->timeToStop );
-    pSat->RunId = p->pPars->RunId;
-    pSat->pFuncStop = p->pPars->pFuncStop;
+    sat_solver_set_runid( pSat, p->pPars->RunId );
+    sat_solver_set_stop_func( pSat, p->pPars->pFuncStop );
     return pSat;
 }
 
@@ -420,8 +420,8 @@ static inline sat_solver * Pdr_ManNewSolver2( sat_solver * pSat, Pdr_Man_t * p,
 //    pSat = sat_solver_new();
     sat_solver_setnvars( pSat, 500 );
     sat_solver_set_runtime_limit( pSat, p->timeToStop );
-    pSat->RunId = p->pPars->RunId;
-    pSat->pFuncStop = p->pPars->pFuncStop;
+    sat_solver_set_runid( pSat, p->pPars->RunId );
+    sat_solver_set_stop_func( pSat, p->pPars->pFuncStop );
     return pSat;
 }
 
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 7e5218d0..21c713b8 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -1296,7 +1296,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                 if ( p->timeToStop && Abc_Clock() > p->timeToStop )
                     Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOut, iFrame );
                 else
-                    Abc_Print( 1, "Reached conflict limit (%d) in frame.\n",  p->pPars->nConfLimit, iFrame );
+                    Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n",  p->pPars->nConfLimit, iFrame );
             }
             p->pPars->iFrame = iFrame;
             return -1;
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index ea6b24af..6b0d58ec 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -32,7 +32,7 @@
 #include "misc/hash/hashInt.h"
 #include "aig/gia/giaAig.h"
 
-//#define PDR_USE_SATOKO 1
+#define PDR_USE_SATOKO 1
 
 #ifndef PDR_USE_SATOKO
     #include "sat/bsat/satSolver.h"
@@ -53,6 +53,8 @@
     #define sat_solver_solve(s,b,e,c,x,y,z)  satoko_solve_assumptions_limit(s,b,e-b,(int)c)
     #define sat_solver_var_value             satoko_read_cex_varvalue
     #define sat_solver_set_runtime_limit     satoko_set_runtime_limit
+    #define sat_solver_set_runid             satoko_set_runid           
+    #define sat_solver_set_stop_func         satoko_set_stop_func          
     #define sat_solver_compress(s)             
 #endif
 
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index f62f3117..e82f17a4 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -330,6 +330,14 @@ static inline int sat_solver_count_usedvars(sat_solver* s)
         }
     return nVars;
 }
+static void sat_solver_set_runid( sat_solver *s, int id )               
+{ 
+    s->RunId      = id;  
+}
+static void sat_solver_set_stop_func( sat_solver *s, int (*fnct)(int) ) 
+{ 
+    s->pFuncStop = fnct; 
+}
 
 static inline int sat_solver_add_const( sat_solver * pSat, int iVar, int fCompl )
 {