diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-03 17:02:36 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-03 17:02:36 -0800 |
| commit | 6d088bc440fb6b7a5b3eb2c9ea7b9950a1698166 (patch) | |
| tree | 8f43756795458df7b4468a9eb4d959fa24bb9b40 /src/proof/pdr/pdrSat.c | |
| parent | e91abd6307e15d9d4a4985146025e12ae6780cff (diff) | |
| download | abc-6d088bc440fb6b7a5b3eb2c9ea7b9950a1698166.tar.gz abc-6d088bc440fb6b7a5b3eb2c9ea7b9950a1698166.tar.bz2 abc-6d088bc440fb6b7a5b3eb2c9ea7b9950a1698166.zip | |
Enabling new X-valued simulation in 'pdr'.
Diffstat (limited to 'src/proof/pdr/pdrSat.c')
| -rw-r--r-- | src/proof/pdr/pdrSat.c | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c index eb94a826..49b0448a 100644 --- a/src/proof/pdr/pdrSat.c +++ b/src/proof/pdr/pdrSat.c @@ -377,7 +377,14 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr p->tSatSat += clk; p->nCallsS++; if ( ppPred ) - *ppPred = Pdr_ManTernarySim( p, k, pCube ); + { + abctime clk = Abc_Clock(); + if ( p->pPars->fNewXSim ) + *ppPred = Txs_ManTernarySim( p->pTxs, k, pCube ); + else + *ppPred = Pdr_ManTernarySim( p, k, pCube ); + p->tTsim += Abc_Clock() - clk; + } RetValue = 0; } |