Commit 4af39856 by Alan Mishchenko

Returning multiple counter-examples.

parent 3b9e363e
......@@ -342,9 +342,10 @@ int Bmc_ChainTest( Gia_Man_t * p, int nFrameMax, int nConfMax, int fVerbose, int
vOutputs = Bmc_ChainFindFailedOutputs( pNew, pvCexes ? *pvCexes : NULL );
assert( Vec_IntFind(vOutputs, pCex->iPo) >= 0 );
// save the counter-example
//Abc_CexFree( pCex );
if ( pvCexes )
Vec_PtrPush( *pvCexes, pCex );
else
Abc_CexFree( pCex );
clkSat += Abc_Clock() - clk2;
// remove them from the AIG
clk2 = Abc_Clock();
......
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