summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat/satSolver.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2017-12-06 11:18:43 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2017-12-06 11:18:43 -0800
commit67181d0446de9f0b0b5df685701ceb420373790f (patch)
treede5e34447189f050bf3cbf9f6403fec1b6b40514 /src/sat/bsat/satSolver.c
parentc4322a0afd740d85fe850e0811d629627a062403 (diff)
downloadabc-67181d0446de9f0b0b5df685701ceb420373790f.tar.gz
abc-67181d0446de9f0b0b5df685701ceb420373790f.tar.bz2
abc-67181d0446de9f0b0b5df685701ceb420373790f.zip
An improvement to 'twoexact' and 'lutexact'.
Diffstat (limited to 'src/sat/bsat/satSolver.c')
-rw-r--r--src/sat/bsat/satSolver.c3
1 files changed, 1 insertions, 2 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 96b03e62..31ae8dae 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1716,12 +1716,11 @@ void sat_solver_rollback( sat_solver* s )
int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
{
- int fVerbose = 0;
lit *i,*j;
int maxvar;
lit last;
assert( begin < end );
- if ( fVerbose )
+ if ( s->fPrintClause )
{
for ( i = begin; i < end; i++ )
printf( "%s%d ", (*i)&1 ? "!":"", (*i)>>1 );