3 files changed, 8 insertions, 6 deletions
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