From: trevor_hansen Date: Wed, 11 May 2011 01:28:38 +0000 (+0000) Subject: Bugfix. Maybe. Disable a comparison so that CNF conversion doesn't fail. This fixes... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=e0604823192d806132df0351d058d34c6256ed19;p=francis%2Fstp.git Bugfix. Maybe. Disable a comparison so that CNF conversion doesn't fail. This fixes the assertion error. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1318 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/extlib-abc/aig/cnf/cnfMap.c b/src/extlib-abc/aig/cnf/cnfMap.c index bf1445e..3a41f7e 100644 --- a/src/extlib-abc/aig/cnf/cnfMap.c +++ b/src/extlib-abc/aig/cnf/cnfMap.c @@ -122,8 +122,12 @@ void Cnf_DeriveMapping( Cnf_Man_t * p ) // Aig_ObjCollectSuper( pObj, vSuper ); // get the area flow of this cut // AreaFlow = Cnf_CutSuperAreaFlow( vSuper, pAreaFlows ); + + // Trevor: Always set the best one with fBest. + // otherwise CNF generation fails. Wrote to Alan + // seeking confirmation this was not dangerous. AreaFlow = AIG_INFINITY; - if ( AreaFlow >= (int)pCutBest->uSign ) + if (1 || AreaFlow >= (int)pCutBest->uSign ) { pAreaFlows[pObj->Id] = pCutBest->uSign; pCutBest->fBest = 1;