From 5fbe218ff8c9a150d2898eae4f454961274ef4eb Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Thu, 9 Mar 2017 22:57:20 -0800
Subject: [PATCH] Improvements to ternary simulation.

---
 abclib.dsp               | 4 ++++
 src/proof/pdr/pdrTsim3.c | 6 +++---
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/abclib.dsp b/abclib.dsp
index 48a3463e8..227cdf8aa 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -5403,6 +5403,10 @@ SOURCE=.\src\proof\pdr\pdrTsim2.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\proof\pdr\pdrTsim3.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\proof\pdr\pdrUtil.c
 # End Source File
 # End Group
diff --git a/src/proof/pdr/pdrTsim3.c b/src/proof/pdr/pdrTsim3.c
index c08223221..ebd1a7026 100644
--- a/src/proof/pdr/pdrTsim3.c
+++ b/src/proof/pdr/pdrTsim3.c
@@ -187,14 +187,14 @@ printf( "%d %d %d \n", Vec_IntSize(p->vCiObjs), Vec_IntSize(p->vFosPre), Vec_Int
 ***********************************************************************/
 Pdr_Set_t * Txs3_ManTernarySim( Txs3_Man_t * p, int k, Pdr_Set_t * pCube )
 {
-    int fTryNew = 1;
-    int fUseLit = 1;
+//    int fTryNew = 1;
+//    int fUseLit = 1;
     int fVerbose = 0;
     sat_solver * pSat;
     Pdr_Set_t * pRes;
     Gia_Obj_t * pObj;
     Vec_Int_t * vVar2Ids, * vLits;
-    int i, Lit, LitAux, Var, Value, RetValue, nCoreLits, * pCoreLits, nLits;
+    int i, Lit, LitAux, Var, Value, RetValue, nCoreLits, * pCoreLits;//, nLits;
 //    if ( k == 0 )
 //        fVerbose = 1;
     // collect CO objects