summaryrefslogtreecommitdiffstats
path: root/src/proof/cec/cecCec.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2020-08-12 19:32:42 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2020-08-12 19:32:42 -0700
commit850d39fec30b46b049717ae0a7a5743396b14ecd (patch)
treecbdd0b663fd4583bb7a9429a07cb1269eb15147d /src/proof/cec/cecCec.c
parentb74b7dfc2d2065eebc800c9165a3e15caeb4453d (diff)
downloadabc-850d39fec30b46b049717ae0a7a5743396b14ecd.tar.gz
abc-850d39fec30b46b049717ae0a7a5743396b14ecd.tar.bz2
abc-850d39fec30b46b049717ae0a7a5743396b14ecd.zip
Making &cec use precomputed simulation info.
Diffstat (limited to 'src/proof/cec/cecCec.c')
-rw-r--r--src/proof/cec/cecCec.c5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index ee45aa6c..d450cead 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -349,6 +349,11 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
Gia_ManStop( p );
return RetValue;
}
+ if ( pInit->vSimsPi )
+ {
+ p->vSimsPi = Vec_WrdDup(pInit->vSimsPi);
+ p->nSimWords = pInit->nSimWords;
+ }
// sweep for equivalences
Cec_ManFraSetDefaultParams( pParsFra );
pParsFra->nItersMax = 1000;