diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-06-03 13:22:24 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-06-03 13:22:24 -0700 |
| commit | 93c785e80250f4e7f4637d3d9317a5cf2e278b69 (patch) | |
| tree | 3a2064f5a8ac25ab24850d658b68cf59eaafc2e5 /src/proof | |
| parent | e33d6e8d9d8f84c2f06bd251d459e758714aed57 (diff) | |
| download | abc-93c785e80250f4e7f4637d3d9317a5cf2e278b69.tar.gz abc-93c785e80250f4e7f4637d3d9317a5cf2e278b69.tar.bz2 abc-93c785e80250f4e7f4637d3d9317a5cf2e278b69.zip | |
Small changes for today's experiments.
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/acec/acecPolyn.c | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/proof/acec/acecPolyn.c b/src/proof/acec/acecPolyn.c index 2f98df73..be601405 100644 --- a/src/proof/acec/acecPolyn.c +++ b/src/proof/acec/acecPolyn.c @@ -311,8 +311,8 @@ void Gia_PolynBuildOne( Pln_Man_t * p, int iMono ) Vec_IntAppendMinus( p->vTempC[0], vConst, 0 ); Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[2] ); // C * y - //if ( !p->pGia->vXors || Vec_IntFind(p->pGia->vXors, iDriver) > 0 ) - { + //if ( !p->pGia->vXors || Vec_IntFind(p->pGia->vXors, iDriver) == -1 || Vec_IntFind(p->pGia->vXors, iDriver) == 5 ) + { vConst = Hsh_VecReadEntry( p->pHashC, iConst ); Vec_IntAppendMinus2x( p->vTempC[0], vConst ); Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[3] ); // -C * x * y |