diff options
Diffstat (limited to 'src/aig/ssw/sswSat.c')
| -rw-r--r-- | src/aig/ssw/sswSat.c | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/src/aig/ssw/sswSat.c b/src/aig/ssw/sswSat.c index 90752baa..264b39d1 100644 --- a/src/aig/ssw/sswSat.c +++ b/src/aig/ssw/sswSat.c @@ -68,8 +68,11 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) } //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); - RetValue = sat_solver_simplify(p->pSat); - assert( RetValue != 0 ); + if ( p->pSat->qtail != p->pSat->qhead ) + { + RetValue = sat_solver_simplify(p->pSat); + assert( RetValue != 0 ); + } clk = clock(); RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, @@ -114,8 +117,11 @@ p->timeSatUndec += clock() - clk; if ( pNew->fPhase ) pLits[1] = lit_neg( pLits[1] ); } - RetValue = sat_solver_simplify(p->pSat); - assert( RetValue != 0 ); + if ( p->pSat->qtail != p->pSat->qhead ) + { + RetValue = sat_solver_simplify(p->pSat); + assert( RetValue != 0 ); + } clk = clock(); RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, |