From 8c04d9501f414b6985f9125cac91e41455ff26f3 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Tue, 4 Dec 2012 18:35:44 -0800
Subject: Making 'scorr -c' applicable to seq benchmarks without constraints.
---
src/proof/ssw/sswConstr.c | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/proof/ssw/sswConstr.c b/src/proof/ssw/sswConstr.c
index 475ed70c..3dcf0a34 100644
--- a/src/proof/ssw/sswConstr.c
+++ b/src/proof/ssw/sswConstr.c
@@ -49,7 +49,7 @@ Aig_Man_t * Ssw_FramesWithConstraints( Aig_Man_t * p, int nFrames )
Aig_Man_t * pFrames;
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int i, f;
- assert( Saig_ManConstrNum(p) > 0 );
+// assert( Saig_ManConstrNum(p) > 0 );
assert( Aig_ManRegNum(p) > 0 );
assert( Aig_ManRegNum(p) < Aig_ManCiNum(p) );
// start the fraig package
@@ -106,7 +106,7 @@ int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
int i, RetValue;
if ( pvInits )
*pvInits = NULL;
- assert( p->nConstrs > 0 );
+// assert( p->nConstrs > 0 );
// derive the timeframes
pFrames = Ssw_FramesWithConstraints( p, nFrames );
// create CNF
@@ -275,12 +275,12 @@ void Ssw_ManRefineByConstrSim( Ssw_Man_t * p )
{
if ( i < Saig_ManPoNum(p->pAig) - Saig_ManConstrNum(p->pAig) )
{
- if ( pObj->fMarkB )
+ if ( pObj->fMarkB && Saig_ManConstrNum(p->pAig) )
Abc_Print( 1, "output %d failed in frame %d.\n", i, f );
}
else
{
- if ( pObj->fMarkB )
+ if ( pObj->fMarkB && Saig_ManConstrNum(p->pAig) )
Abc_Print( 1, "constraint %d failed in frame %d.\n", i, f );
}
}
--
cgit v1.2.3