Skip to content

A
abc
Commit de9fd0a5 by Alan Mishchenko
Options

Added sharing of counter-examples across multiple failed properties in 'bmc3 -a'.

parent b781c1c1
Showing with 2 additions and 1 deletions
src/sat/bmc/bmcBmc3.c
...@@ -1646,9 +1646,10 @@ nTimeSat += Abc_Clock() - clk2; ...@@ -1646,9 +1646,10 @@ nTimeSat += Abc_Clock() - clk2;
if ( p->pPars->fUseBridge ) if ( p->pPars->fUseBridge )
Gia_ManToBridgeResult( stdout, 0, pCexNew0, pCexNew0->iPo ); Gia_ManToBridgeResult( stdout, 0, pCexNew0, pCexNew0->iPo );
// remember solved output // remember solved output
Vec_PtrWriteEntry( p->vCexes, k, pCexNew ); Vec_PtrWriteEntry( p->vCexes, k, Abc_CexDup(pCexNew, pCexNew->nRegs) );
} }
Abc_CexFreeP( &pCexNew0 ); Abc_CexFreeP( &pCexNew0 );
Abc_CexFreeP( &pCexNew );
} }
else else
{ {
......
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