diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-08-02 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-08-02 08:01:00 -0700 |
| commit | cbb7ff8642236fbc21576dec7b57b9e4cb7e60ef (patch) | |
| tree | ae99229ba649fe84e3f1a895570c38601b4b68e4 /src/aig/int | |
| parent | 582a059e34d913ed52dfc18049e407055ebd7879 (diff) | |
| download | abc-cbb7ff8642236fbc21576dec7b57b9e4cb7e60ef.tar.gz abc-cbb7ff8642236fbc21576dec7b57b9e4cb7e60ef.tar.bz2 abc-cbb7ff8642236fbc21576dec7b57b9e4cb7e60ef.zip | |
Version abc80802
Diffstat (limited to 'src/aig/int')
| -rw-r--r-- | src/aig/int/intM114.c | 2 | ||||
| -rw-r--r-- | src/aig/int/intM114p.c | 5 |
2 files changed, 5 insertions, 2 deletions
diff --git a/src/aig/int/intM114.c b/src/aig/int/intM114.c index f92ba179..dbf078e2 100644 --- a/src/aig/int/intM114.c +++ b/src/aig/int/intM114.c @@ -206,7 +206,7 @@ int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward ) int * pGlobalVars; int clk, status, RetValue; int i, Var; - assert( p->pInterNew == NULL ); +// assert( p->pInterNew == NULL ); // derive the SAT solver pSat = Inter_ManDeriveSatSolver( p->pInter, p->pCnfInter, p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, p->vVarsAB, fUseBackward ); diff --git a/src/aig/int/intM114p.c b/src/aig/int/intM114p.c index 69c643ae..77776f7e 100644 --- a/src/aig/int/intM114p.c +++ b/src/aig/int/intM114p.c @@ -322,6 +322,9 @@ Aig_Man_t * Inter_ManpInterpolateM114( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Ptr_t * vInters; int * pLits, * pClauses, * pVars; int nLits, nVars, i, k, iVar; + int nClauses; + + nClauses = M114p_SolverProofClauseNum(s); assert( M114p_SolverProofIsReady(s) ); @@ -346,7 +349,7 @@ Aig_Man_t * Inter_ManpInterpolateM114( M114p_Solver_t s, Vec_Int_t * vMapRoots, } } Vec_PtrPush( vInters, pInter ); - } + } // assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) ); // process learned clauses |