luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Bug fix for incorrect memory allocation in main SAT solver, leading to crashes in 'dsec' (correction to the previous fix).

This commit is contained in:
Alan Mishchenko 2012-01-23 12:21:29 -08:00
parent 3906e37c12
commit 14457af21a
2 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/aig/ivy/ivyFraig.c
View File

@ -2120,7 +2120,7 @@ int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pN
{
p->pSat = sat_solver_new();
sat_solver_setnvars( p->pSat, 1000 );
p->pSat->factors = ABC_CALLOC( double, 1000 );
p->pSat->factors = ABC_CALLOC( double, p->pSat->cap );
p->nSatVars = 1;
// var 0 is reserved for const1 node - add the clause
// pLits[0] = toLit( 0 );
@ -2272,7 +2272,7 @@ int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
{
p->pSat = sat_solver_new();
sat_solver_setnvars( p->pSat, 1000 );
p->pSat->factors = ABC_CALLOC( double, 1000 );
p->pSat->factors = ABC_CALLOC( double, p->pSat->cap );
p->nSatVars = 1;
// var 0 is reserved for const1 node - add the clause
// pLits[0] = toLit( 0 );

2
src/proof/cec/cecSolve.c
View File

@ -377,7 +377,7 @@ void Cec_ManSatSolverRecycle( Cec_ManSat_t * p )
}
p->pSat = sat_solver_new();
sat_solver_setnvars( p->pSat, 1000 );
p->pSat->factors = ABC_CALLOC( double, 1000 );
p->pSat->factors = ABC_CALLOC( double, p->pSat->cap );
// var 0 is not used
// var 1 is reserved for const0 node - add the clause
p->nSatVars = 1;