diff --git a/src/sat/glucose2/CGlucoseCore.h b/src/sat/glucose2/CGlucoseCore.h
index 281cab6bc..ca678ab30 100644
--- a/src/sat/glucose2/CGlucoseCore.h
+++ b/src/sat/glucose2/CGlucoseCore.h
@@ -338,7 +338,7 @@ inline CRef Solver::gatePropagateCheckFanout( Var v, Lit lfo ){
 				return Var2CRef(var(lfo));
 			
 			var2NodeData[var(lfo)].dir = sign(lfo);
-			uncheckedEnqueue2(~mkLit(var(lfo)), Var2CRef( var(lfo) ) );
+			uncheckedEnqueue(~mkLit(var(lfo)), Var2CRef( var(lfo) ) );
 		} else {
 			assert( l_True == value(faninLit) );
 
@@ -355,11 +355,11 @@ inline CRef Solver::gatePropagateCheckFanout( Var v, Lit lfo ){
 				if( l_True == value(faninLitP) )
 					return Var2CRef(var(lfo));
 
-				uncheckedEnqueue2( ~faninLitP, Var2CRef( var(lfo) ) );
+				uncheckedEnqueue( ~faninLitP, Var2CRef( var(lfo) ) );
 			}
 			else
 			if( l_True == value(faninLitP) )
-				uncheckedEnqueue2( mkLit(var(lfo)), Var2CRef( var(lfo) ) );
+				uncheckedEnqueue( mkLit(var(lfo)), Var2CRef( var(lfo) ) );
 		}
 	} else { // xor scope
 		// check value of the other fanin 
@@ -374,10 +374,10 @@ inline CRef Solver::gatePropagateCheckFanout( Var v, Lit lfo ){
 			return CRef_Undef;
 		else
 		if( l_Undef == val1 )
-			uncheckedEnqueue2( ~faninLitP ^ ( (l_True == val0) ^ (l_True == valo) ), Var2CRef( var(lfo) ) );
+			uncheckedEnqueue( ~faninLitP ^ ( (l_True == val0) ^ (l_True == valo) ), Var2CRef( var(lfo) ) );
 		else
 		if( l_Undef == valo )
-			uncheckedEnqueue2( ~mkLit( var(lfo), (l_True == val0) ^ (l_True == val1) ), Var2CRef( var(lfo) ) );
+			uncheckedEnqueue( ~mkLit( var(lfo), (l_True == val0) ^ (l_True == val1) ), Var2CRef( var(lfo) ) );
 		else
 		if( l_False  == (valo ^ (val0 == val1)) )
 			return Var2CRef(var(lfo));
@@ -398,19 +398,19 @@ inline CRef Solver::gatePropagateCheckThis( Var v ){
 				return CRef_Undef;
 
 			if( l_True == value(getFaninLit0(v)) )
-				uncheckedEnqueue2(~getFaninLit1( v ), Var2CRef( v ) );
+				uncheckedEnqueue(~getFaninLit1( v ), Var2CRef( v ) );
 			if( l_True == value(getFaninLit1(v)) )
-				uncheckedEnqueue2(~getFaninLit0( v ), Var2CRef( v ) );
+				uncheckedEnqueue(~getFaninLit0( v ), Var2CRef( v ) );
 		} else {
 			assert( l_True == value(v) );
 			if( l_False == value(getFaninLit0(v)) || l_False == value(getFaninLit1(v)) )
 				confl = Var2CRef(v);
 
 			if( l_Undef == value( getFaninLit0( v )) )
-				uncheckedEnqueue2( getFaninLit0( v ), Var2CRef( v ) );
+				uncheckedEnqueue( getFaninLit0( v ), Var2CRef( v ) );
 
 			if( l_Undef == value( getFaninLit1( v )) )
-				uncheckedEnqueue2( getFaninLit1( v ), Var2CRef( v ) );
+				uncheckedEnqueue( getFaninLit1( v ), Var2CRef( v ) );
 
 		}
 	} else { // xor scope
@@ -421,10 +421,10 @@ inline CRef Solver::gatePropagateCheckThis( Var v ){
 		if( l_Undef == val0 && l_Undef == val1 )
 			return CRef_Undef;
 		if( l_Undef == val0 )
-			uncheckedEnqueue2(~getFaninLit0( v ) ^ ( (l_True == val1) ^ (l_True == valo) ), Var2CRef( v ) );
+			uncheckedEnqueue(~getFaninLit0( v ) ^ ( (l_True == val1) ^ (l_True == valo) ), Var2CRef( v ) );
 		else
 		if( l_Undef == val1 )
-			uncheckedEnqueue2(~getFaninLit1( v ) ^ ( (l_True == val0) ^ (l_True == valo) ), Var2CRef( v ) );
+			uncheckedEnqueue(~getFaninLit1( v ) ^ ( (l_True == val0) ^ (l_True == valo) ), Var2CRef( v ) );
 		else
 		if( l_False == (valo ^ (val0 == val1)) )
 			return Var2CRef(v);
@@ -566,12 +566,17 @@ inline void Solver::markCone( Var v ){
 	Var var0, var1;
 	var0 = getFaninVar0(v);
 	var1 = getFaninVar1(v);
-	if( !isTwoFanin(v) )
+	if( !isTwoFanin(v) || (value(v) != l_Undef && level(v) == 0) )
 		return;
 	markCone( var0 );
 	markCone( var1 );
 }
 
+inline void Solver::markVar( Var v ){
+	var2TravId[v] = travId;
+	var2NodeData[v].sort = 0;
+}
+
 inline void Solver::inplace_sort( Var v ){
 	Lit w, next, prev;
 	prev= var2Fanout0[v];
diff --git a/src/sat/glucose2/Solver.h b/src/sat/glucose2/Solver.h
index 3aff6a31d..1be42e793 100644
--- a/src/sat/glucose2/Solver.h
+++ b/src/sat/glucose2/Solver.h
@@ -71,6 +71,7 @@ public:
     void sat_solver_set_var_fanin_lit(int, int, int);  
     void sat_solver_start_new_round();  
     void sat_solver_mark_cone(int);  
+    void sat_solver_mark_var(int);
     void sat_solver_set_jftr(int);
     int  sat_solver_jftr();
     void sat_solver_reset();
@@ -486,6 +487,7 @@ public:
 
     void setNewRound(){ travId ++ ; }
     void markCone( Var v );
+    void markVar( Var v );
     void setJust( int njftr ){ jftr = njftr; }
     bool isRoundWatch( Var v ) const { return travId==var2TravId[v]; }
     void justReset(){ jftr = 0; reset(); }
@@ -627,6 +629,7 @@ inline void     Solver::addVar(Var v) { while (v >= nVars()) newVar(); }
 inline void     Solver::sat_solver_set_var_fanin_lit(int v, int lit0, int lit1) { setVarFaninLits( Var(v), toLit(lit0), toLit(lit1) ); }
 inline void     Solver::sat_solver_start_new_round()  { setNewRound(); }
 inline void     Solver::sat_solver_mark_cone(int v) { markCone(v); }
+inline void     Solver::sat_solver_mark_var(int v) { markVar(v); }
 inline void     Solver::sat_solver_set_jftr( int njftr ){ setJust(njftr); }
 inline int      Solver::sat_solver_jftr(){ return jftr; }
 inline void     Solver::sat_solver_reset(){ justReset();  }