diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index d782386e9..f1f03ce26 100644
--- a/src/sat/bsat/satUtil.c
+++ b/src/sat/bsat/satUtil.c
@@ -61,7 +61,10 @@ void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncrement )
 
   Synopsis    [Write the clauses in the solver into a file in DIMACS format.]
 
-  Description []
+  Description [This procedure by default does not print binary clauses. To enable 
+  printing of binary clauses, please set fUseBinaryClauses to 0 in the body of 
+  procedure sat_solver_clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
+  in file "satSolver.c".]
                
   SideEffects []