Skip to content

A
abc
Commit 57b51411 by Alan Mishchenko
Options

Sweeper assertion.

parent 7b6e7181
Showing with 2 additions and 0 deletions
src/proof/ssc/sscSat.c
...@@ -350,6 +350,8 @@ int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl ) ...@@ -350,6 +350,8 @@ int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl )
int pLitsSat[2], RetValue; int pLitsSat[2], RetValue;
abctime clk; abctime clk;
assert( iRepr != iNode ); assert( iRepr != iNode );
if ( iRepr > iNode )
return l_Undef;
assert( iRepr < iNode ); assert( iRepr < iNode );
// if ( p->nTimeOut ) // if ( p->nTimeOut )
// sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() ); // sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment