Changes to several APIs.

src/aig/gia/giaMan.c

@@ -1315,18 +1315,21 @@ void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs )
     fprintf( pFile, "\n" );
     Gia_ManForEachAnd( p, pObj, i )
     {
+        int fSkip = 0;
         if ( vObjs )
         {
             Vec_IntForEachEntry( vObjs, iObj, k )
                 if ( iObj == i )
                     break;
             if ( k < Vec_IntSize(vObjs) )
-                continue;
+                fSkip = 1;
         }
-
+        if ( !fSkip )
+        {
             fprintf( pFile, "  and( %s,", Gia_ObjGetDumpName(NULL, 'n', i, nDigits) );
             fprintf( pFile, " %s,",       Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC0(pObj)? 'i':'n'), Gia_ObjFaninId0(pObj, i), nDigits) );
             fprintf( pFile, " %s );\n",   Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC1(pObj)? 'i':'n'), Gia_ObjFaninId1(pObj, i), nDigits) );
+        }
         if ( Vec_BitEntry(vInvs, i) )
         {
             fprintf( pFile, "  not( %s,", Gia_ObjGetDumpName(NULL, 'i', i, nDigits) );

src/base/acb/acb.h

@@ -416,6 +416,7 @@ static inline int Acb_ObjWhatFanin( Acb_Ntk_t * p, int iObj, int iFaninGiven )
 static inline void Acb_ObjAddFanin( Acb_Ntk_t * p, int iObj, int iFanin )
 {
     int * pFanins = Acb_ObjFanins( p, iObj );
+    assert( iFanin > 0 );
     assert( pFanins[ 1 + pFanins[0] ] == -1 );
     pFanins[ 1 + pFanins[0]++ ] = iFanin;
 }

src/sat/bsat/satSolver.c

@@ -217,16 +217,32 @@ static inline int  order_select(sat_solver* s, float random_var_freq) // selectv
 void sat_solver_set_var_activity(sat_solver* s, int * pVars, int nVars) 
 {
     int i;
-    assert( s->VarActType == 1 );
     for (i = 0; i < s->size; i++)
         s->activity[i] = 0;
+    if ( s->VarActType == 0 )
+    {
+        s->var_inc            = (1 <<  5);
+        s->var_decay          = -1;
+        for ( i = 0; i < nVars; i++ )
+        {
+            int iVar = pVars ? pVars[i] : i;
+            s->activity[iVar] = s->var_inc*(nVars-i);
+            if (s->orderpos[iVar] != -1)
+                order_update( s, iVar );
+        }
+    }
+    else if ( s->VarActType == 1 )
+    {
         s->var_inc = Abc_Dbl2Word(1);
         for ( i = 0; i < nVars; i++ )
         {
             int iVar = pVars ? pVars[i] : i;
             s->activity[iVar] = Abc_Dbl2Word(nVars-i);
+            if (s->orderpos[iVar] != -1)
                 order_update( s, iVar );
         }
+    }
+    else assert( 0 );
 }
 
 //=================================================================================================