2 files changed, 8 insertions, 0 deletions
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index a3f353c2..22ae765d 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -73,6 +73,8 @@ struct Saig_ParBmc_t_
     int         nDropOuts;      // the number of dropped outputs
     abctime     timeLastSolved; // the time when the last output was solved
     int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
+    int         RunId;          // BMC id in this run 
+    int(*pFuncStop)(int);       // callback to terminate
 };
 
  
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index ccd0bb90..34fdf45f 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1533,6 +1533,12 @@ clkOther += Abc_Clock() - clk2;
                     Abc_Print( 1, "Reached timeout (%d seconds).\n",  pPars->nTimeOut );
                 goto finish;
             }
+            if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
+            {
+                if ( !pPars->fSilent )
+                    Abc_Print( 1, "Bmc3 got callbacks.\n" );
+                goto finish;
+            }
             // skip solved outputs
             if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
                 continue;