diff options
| author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-04-16 22:03:47 -0700 |
|---|---|---|
| committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-04-16 22:03:47 -0700 |
| commit | 38e5c8c9e6eaa5fa97e85ced24970e0628afcdf9 (patch) | |
| tree | 731b8b8c8403aa1fbd046813113e6ab54c8f45ea /src/base/wlc/wlcAbs.c | |
| parent | fea18c2d42273f1cf100472328ba1c267ba096b3 (diff) | |
| download | abc-38e5c8c9e6eaa5fa97e85ced24970e0628afcdf9.tar.gz abc-38e5c8c9e6eaa5fa97e85ced24970e0628afcdf9.tar.bz2 abc-38e5c8c9e6eaa5fa97e85ced24970e0628afcdf9.zip | |
%pdra: added an option for disabling incremental solving
Diffstat (limited to 'src/base/wlc/wlcAbs.c')
| -rw-r--r-- | src/base/wlc/wlcAbs.c | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index c56d1262..d0ef1f07 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -1530,7 +1530,8 @@ int Wla_ManSolveInt( Wla_Man_t * pWla, Aig_Man_t * pAig ) RetValue = IPdr_ManSolveInt( pPdr, pWla->pPars->fCheckClauses, pWla->pPars->fPushClauses ); pPdr->tTotal += Abc_Clock() - clk; pWla->tPdr += pPdr->tTotal; - pWla->vClauses = IPdr_ManSaveClauses( pPdr, 0 ); + if ( pWla->pPars->fLoadTrace) + pWla->vClauses = IPdr_ManSaveClauses( pPdr, 0 ); Pdr_ManStop( pPdr ); |