summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2013-11-01 11:22:04 -0400
committerAlan Mishchenko <alanmi@berkeley.edu>2013-11-01 11:22:04 -0400
commit7b6e7181e0c1b4a4e4bc8552eabb7ee2adf2b4ca (patch)
tree721dbdf06bd20dc48408df012f0a5a98c7cb6aa0 /src/proof
parente4ab09d7711e2126d8df05002d81b3cc8a849f35 (diff)
downloadabc-7b6e7181e0c1b4a4e4bc8552eabb7ee2adf2b4ca.tar.gz
abc-7b6e7181e0c1b4a4e4bc8552eabb7ee2adf2b4ca.tar.bz2
abc-7b6e7181e0c1b4a4e4bc8552eabb7ee2adf2b4ca.zip
Sweeper assertion.
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/ssc/sscSat.c1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/proof/ssc/sscSat.c b/src/proof/ssc/sscSat.c
index ca0933ec..c029a541 100644
--- a/src/proof/ssc/sscSat.c
+++ b/src/proof/ssc/sscSat.c
@@ -349,6 +349,7 @@ int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl )
{
int pLitsSat[2], RetValue;
abctime clk;
+ assert( iRepr != iNode );
assert( iRepr < iNode );
// if ( p->nTimeOut )
// sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() );