Changes to several APIs.

1 files changed, 22 insertions, 6 deletions

diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 31ae8dae..2f3a84db 100644
--- a/src/sat/bsat/satSolver.c
+++ b/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;
-    s->var_inc = Abc_Dbl2Word(1);
-    for ( i = 0; i < nVars; i++ )
+    if ( s->VarActType == 0 )
     {
-        int iVar = pVars ? pVars[i] : i;
-        s->activity[iVar] = Abc_Dbl2Word(nVars-i);
-        order_update( s, iVar );
+        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 );
 }
 
 //=================================================================================================