From f5cb9d6448a9c1d450fd9f578c18b7b51c290fd4 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sat, 16 Sep 2017 12:37:27 -0700
Subject: Bug fix in Glucose integration.

---
 src/sat/glucose/Glucose.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/sat/glucose/Glucose.cpp')

diff --git a/src/sat/glucose/Glucose.cpp b/src/sat/glucose/Glucose.cpp
index 8d520474..2a67d903 100644
--- a/src/sat/glucose/Glucose.cpp
+++ b/src/sat/glucose/Glucose.cpp
@@ -209,7 +209,7 @@ Var Solver::newVar(bool sign, bool dvar)
     //activity .push(0);
     activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0);
     seen     .push(0);
-    permDiff  .push(0);
+    permDiff .push(0);
     polarity .push(sign);
     decision .push();
     trail    .capacity(v+1);
@@ -226,7 +226,7 @@ bool Solver::addClause_(vec<Lit>& ps)
 
     if ( 0 ) {
         for ( int i = 0; i < ps.size(); i++ )
-            printf( "%d ", toInt(ps[i]) );
+            printf( "%s%d ", (toInt(ps[i]) & 1) ? "-":"", toInt(ps[i]) >> 1 );
         printf( "\n" );
     }
 
-- 
cgit v1.2.3