From 092c7be0ffb89d869e8eaeb04de12779ce96e8b9 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 5 Sep 2008 08:01:00 -0700
Subject: Version abc80905

---
 src/aig/ivy/ivyFraig.c | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'src/aig/ivy')

diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index c306c394..25f7a3ef 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -2226,7 +2226,7 @@ p->timeSatFail += clock() - clk;
 int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
 {
     int pLits[2], RetValue1, clk;
-//    int RetValue;
+    int RetValue;
 
     // make sure the nodes are not complemented
     assert( !Ivy_IsComplement(pNew) );
@@ -2261,8 +2261,8 @@ p->timeSat += clock() - clk;
     {
 p->timeSatUnsat += clock() - clk;
         pLits[0] = lit_neg( pLits[0] );
-//        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
-//        assert( RetValue );
+        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
+        assert( RetValue );
         // continue solving the other implication
         p->nSatCallsUnsat++;
     }
@@ -2533,6 +2533,7 @@ void Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t *
         Ivy_ObjSetFaninVec( pNode, vFanins );
     }
     Vec_PtrFree( vFrontier );
+    sat_solver_simplify( p->pSat );
 }
 
 /**Function*************************************************************
-- 
cgit v1.2.3