diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-03-26 18:42:47 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-03-26 18:42:47 -0700 |
| commit | dfb065fa553e54fe00891fbeefb866be2c6dfa9d (patch) | |
| tree | 4d48259db17b0d627c62021848cfe40172e50e61 /src/sat/bsat/satSolver.c | |
| parent | d010231043bc799ab7598e4ac779161a02001c17 (diff) | |
| download | abc-dfb065fa553e54fe00891fbeefb866be2c6dfa9d.tar.gz abc-dfb065fa553e54fe00891fbeefb866be2c6dfa9d.tar.bz2 abc-dfb065fa553e54fe00891fbeefb866be2c6dfa9d.zip | |
Fixing the dump of SAT solver into a CNF file.
Diffstat (limited to 'src/sat/bsat/satSolver.c')
| -rw-r--r-- | src/sat/bsat/satSolver.c | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 0e5c6b91..ab1203ea 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -401,6 +401,7 @@ static inline int sat_clause_compute_lbd( sat_solver* s, clause* c ) */ static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt) { + int fUseBinaryClauses = 1; int size; clause* c; int h; @@ -410,7 +411,7 @@ static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt) size = end - begin; // do not allocate memory for the two-literal problem clause - if ( size == 2 && !learnt ) + if ( fUseBinaryClauses && size == 2 && !learnt ) { veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(clause_from_lit(begin[1]))); veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(clause_from_lit(begin[0]))); |