diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-07-19 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-07-19 08:01:00 -0700 |
| commit | de978ced7b754706efaf18ae588e18eb05624faf (patch) | |
| tree | 0180f1b83fe9a3492a754a91e1aa152024affc54 /src/sat/bsat/satInterA.c | |
| parent | 13f52980dae9821b3d7bec9ff6a0fa4e544607d7 (diff) | |
| download | abc-de978ced7b754706efaf18ae588e18eb05624faf.tar.gz abc-de978ced7b754706efaf18ae588e18eb05624faf.tar.bz2 abc-de978ced7b754706efaf18ae588e18eb05624faf.zip | |
Version abc80719
Diffstat (limited to 'src/sat/bsat/satInterA.c')
| -rw-r--r-- | src/sat/bsat/satInterA.c | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c index 5837e68f..82f4e034 100644 --- a/src/sat/bsat/satInterA.c +++ b/src/sat/bsat/satInterA.c @@ -809,8 +809,12 @@ int Inta_ManProcessRoots( Inta_Man_t * p ) if ( !Inta_ManEnqueue( p, pClause->pLits[0], pClause ) ) { // detected root level conflict - printf( "Error in Inta_ManProcessRoots(): Detected a root-level conflict too early!\n" ); - assert( 0 ); +// printf( "Error in Inta_ManProcessRoots(): Detected a root-level conflict too early!\n" ); +// assert( 0 ); + // detected root level conflict + Inta_ManProofTraceOne( p, pClause, p->pCnf->pEmpty ); + if ( p->fVerbose ) + printf( "Found root level conflict!\n" ); return 0; } } |