Commit 8dc61f1f by Alan Mishchenko

Enabling refinement in &gla_refine even if CEX is invalid.

parent 63dab645
...@@ -246,8 +246,8 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose ...@@ -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 ) ) if ( !Gia_ManVerifyCex( pAbs, pCex, 0 ) )
{ {
Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is invalid.\n" ); Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is invalid.\n" );
Gia_ManStop( pAbs ); // Gia_ManStop( pAbs );
return -1; // return -1;
} }
// else // else
// Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is correct.\n" ); // Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is correct.\n" );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment