summaryrefslogtreecommitdiffstats
path: root/src/opt/sfm/sfmSat.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2020-01-07 01:36:06 +0200
committerAlan Mishchenko <alanmi@berkeley.edu>2020-01-07 01:36:06 +0200
commit1485e63ae3cc36d2840b5c2d1d7da38a88ee8928 (patch)
tree9ba48d1d144f77a486fd9929ade266af8f650e1b /src/opt/sfm/sfmSat.c
parente1997b038a2d22abffa1215fbfb2209d6bf70c5c (diff)
downloadabc-1485e63ae3cc36d2840b5c2d1d7da38a88ee8928.tar.gz
abc-1485e63ae3cc36d2840b5c2d1d7da38a88ee8928.tar.bz2
abc-1485e63ae3cc36d2840b5c2d1d7da38a88ee8928.zip
Allowing nodes and boxes to have more than 6 inputs in mfs2 and &mfs.
Diffstat (limited to 'src/opt/sfm/sfmSat.c')
-rw-r--r--src/opt/sfm/sfmSat.c1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c
index 8bcb7f8a..6ccdd903 100644
--- a/src/opt/sfm/sfmSat.c
+++ b/src/opt/sfm/sfmSat.c
@@ -167,6 +167,7 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
sat_solver_setnvars( p->pSat, nVars + 1 );
pLits[0] = Abc_Var2Lit( Sfm_ObjSatVar(p, p->iPivotNode), 0 ); // F = 1
pLits[1] = Abc_Var2Lit( nVars, 0 ); // iNewLit
+ assert( Vec_IntSize(p->vDivIds) <= 6 );
while ( 1 )
{
// find onset minterm