diff options
| author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-03-30 13:53:18 -0700 |
|---|---|---|
| committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-03-30 13:53:18 -0700 |
| commit | 1cb140bb1143df405817ae62bde2dcd866fc282c (patch) | |
| tree | d964030340c4e659b9f5bf22c83b631691cbd277 /src/proof | |
| parent | ecf91190d6a1dab0691ad03f42c816ec2788722b (diff) | |
| download | abc-1cb140bb1143df405817ae62bde2dcd866fc282c.tar.gz abc-1cb140bb1143df405817ae62bde2dcd866fc282c.tar.bz2 abc-1cb140bb1143df405817ae62bde2dcd866fc282c.zip | |
%pdra: fixed bugs
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/pdr/pdrIncr.c | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index 8cc964e5..c59bfe1c 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -160,7 +160,8 @@ int IPdr_ManCheckClauses( Pdr_Man_t * p ) printf( "Cube[%d][%d] not inductive!\n", k, j ); } - assert( RetValue == 1 ); + if ( RetValue == -1 ) + return -1; } } |