summaryrefslogtreecommitdiffstats
path: root/src/opt/mfs/mfsResub.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/mfs/mfsResub.c')
-rw-r--r--src/opt/mfs/mfsResub.c8
1 files changed, 8 insertions, 0 deletions
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index 008b6863..8cd70dbf 100644
--- a/src/opt/mfs/mfsResub.c
+++ b/src/opt/mfs/mfsResub.c
@@ -99,9 +99,17 @@ int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
{
unsigned * pData;
int RetValue, iVar, i;
+ int clk = clock(), RetValue2 = Abc_NtkMfsTryResubOnceGia( p, pCands, nCands );
+p->timeGia += clock() - clk;
+
p->nSatCalls++;
RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
// assert( RetValue == l_False || RetValue == l_True );
+ if ( RetValue != l_Undef && RetValue2 != -1 )
+ {
+ assert( (RetValue == l_False) == (RetValue2 == 1) );
+ }
+
if ( RetValue == l_False )
return 1;
if ( RetValue != l_True )