summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-07-11 09:05:20 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2012-07-11 09:05:20 -0700
commit8dc61f1f201f651c7e781cc7b5d34f78ebefce08 (patch)
tree82ff3c21cedd81cc617c570310ee0b3e2fd630dd /src
parent63dab64574e2ec843220a2a4458bf387fff9c94f (diff)
downloadabc-8dc61f1f201f651c7e781cc7b5d34f78ebefce08.tar.gz
abc-8dc61f1f201f651c7e781cc7b5d34f78ebefce08.tar.bz2
abc-8dc61f1f201f651c7e781cc7b5d34f78ebefce08.zip
Enabling refinement in &gla_refine even if CEX is invalid.
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaAbsGla.c4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 6248fc2a..1553be5f 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -246,8 +246,8 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose
if ( !Gia_ManVerifyCex( pAbs, pCex, 0 ) )
{
Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is invalid.\n" );
- Gia_ManStop( pAbs );
- return -1;
+// Gia_ManStop( pAbs );
+// return -1;
}
// else
// Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is correct.\n" );