summaryrefslogtreecommitdiffstats
path: root/src/proof/ssc
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2013-11-01 13:48:17 -0400
committerAlan Mishchenko <alanmi@berkeley.edu>2013-11-01 13:48:17 -0400
commit74893bf3d4d26570f4e5dbc6ed9562d808e05f2c (patch)
treea8c1b60c3a6942e73fd5c27c9e352e6f7dc69c43 /src/proof/ssc
parenta564e2ab8184f330e87da811cedfd3faf2ee4041 (diff)
downloadabc-74893bf3d4d26570f4e5dbc6ed9562d808e05f2c.tar.gz
abc-74893bf3d4d26570f4e5dbc6ed9562d808e05f2c.tar.bz2
abc-74893bf3d4d26570f4e5dbc6ed9562d808e05f2c.zip
Sweeper internal verification.
Diffstat (limited to 'src/proof/ssc')
-rw-r--r--src/proof/ssc/sscCore.c2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c
index 0fb16103..caad8d48 100644
--- a/src/proof/ssc/sscCore.c
+++ b/src/proof/ssc/sscCore.c
@@ -225,7 +225,7 @@ int Ssc_PerformVerification( Gia_Man_t * p0, Gia_Man_t * p1, Gia_Man_t * pC )
int Status;
Cec_ParCec_t ParsCec, * pPars = &ParsCec;
// derive the OR of constraint outputs
- Gia_Man_t * pCond = Gia_ManDupAndOr( pC, 1, 0 );
+ Gia_Man_t * pCond = Gia_ManDupAndOr( pC, Gia_ManPoNum(p0), 1, 0 );
// derive F = F & !OR(c0, c1, c2, ...)
Gia_Man_t * p0c = Gia_ManMiter( p0, pCond, 0, 0, 0, 1, 0 );
// derive F = F & !OR(c0, c1, c2, ...)