diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-11-17 11:49:30 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-11-17 11:49:30 -0800 |
| commit | a28dd33df07b9b4932cf32855005f4cdc68316c9 (patch) | |
| tree | 00bae804c57f44056dfc3bbb9e01b045d95719e8 /src/opt | |
| parent | 5a10c8ad01b62a6760e4cf8720800acb1fab8554 (diff) | |
| download | abc-a28dd33df07b9b4932cf32855005f4cdc68316c9.tar.gz abc-a28dd33df07b9b4932cf32855005f4cdc68316c9.tar.bz2 abc-a28dd33df07b9b4932cf32855005f4cdc68316c9.zip | |
Integrating mfs2 package to work with boxes.
Diffstat (limited to 'src/opt')
| -rw-r--r-- | src/opt/sfm/sfmSat.c | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c index f61ee798..0d5bbca2 100644 --- a/src/opt/sfm/sfmSat.c +++ b/src/opt/sfm/sfmSat.c @@ -91,7 +91,8 @@ int Sfm_NtkWindowToSolver( Sfm_Ntk_t * p ) if ( Vec_IntSize(vClause) == 0 ) break; RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) ); - assert( RetValue ); + if ( RetValue == 0 ) + return 0; } } if ( Vec_IntSize(p->vTfo) > 0 ) @@ -126,7 +127,8 @@ int Sfm_NtkWindowToSolver( Sfm_Ntk_t * p ) if ( Vec_IntSize(vClause) == 0 ) break; RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) ); - assert( RetValue ); + if ( RetValue == 0 ) + return 0; } } // create XOR clauses for the roots |