diff --git a/src/sat/glucose2/Glucose2.cpp b/src/sat/glucose2/Glucose2.cpp
index aca86bf06..1ba55551f 100644
--- a/src/sat/glucose2/Glucose2.cpp
+++ b/src/sat/glucose2/Glucose2.cpp
@@ -154,6 +154,8 @@ Solver::Solver() :
   , trace_default_tag(~0)
   , trace_qhead(0)
 
+  , produceInnerModel(false)
+
   #ifdef CGLUCOSE_EXP
   //, jheap         (JustOrderLt(this))
   , jheap         (JustOrderLt2(this))
@@ -1579,7 +1581,7 @@ printf("c ==================================[ Search Statistics (every %6d confl
                 int i = 0, j = 0;
                 JustModel.push(toLit(0));
                 for (; i < trail.size(); i++) 
-                    if( isRoundWatch(var(trail[i])) && !isTwoFanin(var(trail[i])) )
+                    if( isRoundWatch(var(trail[i])) && (produceInnerModel || !isTwoFanin(var(trail[i])) ))
                         JustModel.push(trail[i]), j++;
                 JustModel[0] = toLit(j);
             }
diff --git a/src/sat/glucose2/Solver.h b/src/sat/glucose2/Solver.h
index d8d9955fa..e019c2fd3 100644
--- a/src/sat/glucose2/Solver.h
+++ b/src/sat/glucose2/Solver.h
@@ -495,6 +495,7 @@ public:
     //double justActivity(int v) const { return jdata[v].act_fanin;}
     int varPolarity(int v){ return polarity[v]? 1: 0;}
     vec<Lit> JustModel; // model obtained by justification enabled
+    bool produceInnerModel;
 
     int justUsage() const ;
     int solveLimited( int * , int nlits );