From 1cb140bb1143df405817ae62bde2dcd866fc282c Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Thu, 30 Mar 2017 13:53:18 -0700 Subject: %pdra: fixed bugs --- src/proof/pdr/pdrIncr.c | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/proof') 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; } } -- cgit v1.2.3