summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat/satProof2.h
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-08-27 13:49:53 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2012-08-27 13:49:53 -0700
commitc25f5dee05c24c146680c555176b827d0008a444 (patch)
treef8e5bd5913b96e61ba8d542bb9bededf549db110 /src/sat/bsat/satProof2.h
parent1ba1e6574cb4421f8a7c5984aa199e4efa62c3bf (diff)
downloadabc-c25f5dee05c24c146680c555176b827d0008a444.tar.gz
abc-c25f5dee05c24c146680c555176b827d0008a444.tar.bz2
abc-c25f5dee05c24c146680c555176b827d0008a444.zip
Bug fix in &gla.
Diffstat (limited to 'src/sat/bsat/satProof2.h')
-rw-r--r--src/sat/bsat/satProof2.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/sat/bsat/satProof2.h b/src/sat/bsat/satProof2.h
index 25ad0d07..b82d9590 100644
--- a/src/sat/bsat/satProof2.h
+++ b/src/sat/bsat/satProof2.h
@@ -290,6 +290,7 @@ static inline Vec_Int_t * Prf_ManUnsatCore( Prf_Man_t * p )
int i, Entry;
assert( p->iFirst >= 0 );
assert( p->pInfo == NULL );
+ assert( Prf_ManSize(p) > 0 );
vCore = Vec_IntAlloc( 64 * p->nWords );
p->pInfo = Prf_ManClauseInfo( p, Prf_ManSize(p)-1 );
if ( p->vId2Pr == NULL )