diff --git a/src/sat/glucose/Glucose.cpp b/src/sat/glucose/Glucose.cpp
index cfb388de6..d878e0d17 100644
--- a/src/sat/glucose/Glucose.cpp
+++ b/src/sat/glucose/Glucose.cpp
@@ -1124,7 +1124,7 @@ lbool Solver::search(int nof_conflicts)
             return l_False;
           }
             // Perform clause database reduction !
-            if(conflicts>=curRestart* nbclausesbeforereduce) 
+            if(conflicts>=curRestart* nbclausesbeforereduce && learnts.size()>0) 
               {
                   
                 assert(learnts.size()>0);