summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/bsat')
-rw-r--r--src/sat/bsat/satUtil.c5
1 files changed, 4 insertions, 1 deletions
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index d782386e..f1f03ce2 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 []