Free the memory allocatated to the AIGs before SAT solving.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@919 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index 08a6ca463f5c5d86edd1f96aefaf46b65d7fea39..765b520be17ab6906d81443543f24aa166301a1d 100644 (file)
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -16,7 +16,8 @@
 #OPTIMIZE      = -O3 -march=native -fomit-frame-pointer # Maximum optimization
 #OPTIMIZE      = -O3 -march=native -DNDEBUG -DLESSBYTES_PERNODE
 OPTIMIZE      = -O3               # Maximum optimization
-CFLAGS_M32   = -m32 -g 
+CFLAGS_M32   = -g
+
 #-fno-inline
 CFLAGS_BASE   = $(OPTIMIZE)
 

diff --git a/src/to-sat/AIG/BBNodeManagerAIG.h b/src/to-sat/AIG/BBNodeManagerAIG.h
index 94f6f6d1efc3f62eae918a0cd229cc1685d9cc7e..25c323af2b8e18f994a4af0a2cd68cd11d15a502 100644 (file)
--- a/src/to-sat/AIG/BBNodeManagerAIG.h
+++ b/src/to-sat/AIG/BBNodeManagerAIG.h
@@ -85,9 +85,16 @@ public:
                 aigMgr->fAddStrash = 1;
         }
 
+        void stop()
+        {
+          if (aigMgr !=NULL)
+            Aig_ManStop(aigMgr);
+          aigMgr = NULL;
+        }
+
         ~BBNodeManagerAIG()
         {
-                Aig_ManStop(aigMgr);
+          stop();
         }
 
         BBNodeAIG getTrue()

diff --git a/src/to-sat/AIG/ToSATAIG.h b/src/to-sat/AIG/ToSATAIG.h
index 73a57e990df40029ec0def4c49fcd5c4d743b41d..d09176fdf9b3c3cd1daf188037725e9547e7a2fe 100644 (file)
--- a/src/to-sat/AIG/ToSATAIG.h
+++ b/src/to-sat/AIG/ToSATAIG.h
@@ -70,6 +70,10 @@ namespace BEEV
 
       mgr.toCNF(BBFormula, cnfData, nodeToSATVar);
 
+      // Free the memory in the AIGs.
+      BBFormula = BBNodeAIG(); // null node
+      mgr.stop();
+
       bm->GetRunTimes()->start(RunTimes::SendingToSAT);
 
       for (int i = 0; i < cnfData->nVars; i++)