diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2018-03-25 18:19:06 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2018-03-25 18:19:06 -0700 |
| commit | a2d59be3f7f05c4757ade8b3b6f9fdf425de5cc0 (patch) | |
| tree | e56de4cf3568983deb75e90bd9a9cb8e17f29ee8 /src/sat | |
| parent | e639e8fd1ba990f782385b294a6cb5a21844f688 (diff) | |
| download | abc-a2d59be3f7f05c4757ade8b3b6f9fdf425de5cc0.tar.gz abc-a2d59be3f7f05c4757ade8b3b6f9fdf425de5cc0.tar.bz2 abc-a2d59be3f7f05c4757ade8b3b6f9fdf425de5cc0.zip | |
Integrating SAT-based CEX minimization (bug fix).
Diffstat (limited to 'src/sat')
| -rw-r--r-- | src/sat/bmc/bmcCexCare.c | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/src/sat/bmc/bmcCexCare.c b/src/sat/bmc/bmcCexCare.c index 8db92444..c274b04c 100644 --- a/src/sat/bmc/bmcCexCare.c +++ b/src/sat/bmc/bmcCexCare.c @@ -439,11 +439,7 @@ Abc_Cex_t * Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t Gia_ManStop( pGia ); return NULL; } - // verify and return - if ( !Bmc_CexVerify( pGia, pCex, pCexMin ) ) - printf( "Counter-example verification has failed.\n" ); - else if ( fCheck ) - printf( "Counter-example verification succeeded.\n" ); + // unfortunately, cannot verify - ternary simulation does not work Gia_ManStop( pGia ); return pCexMin; } |