summaryrefslogtreecommitdiffstats
path: root/src/proof/pdr/pdrTsim3.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2017-03-09 22:57:20 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2017-03-09 22:57:20 -0800
commit5fbe218ff8c9a150d2898eae4f454961274ef4eb (patch)
tree70a2648fd4528f5c2a0178239e0555f04b6b00ad /src/proof/pdr/pdrTsim3.c
parentd877074d8ff6c23b4c14b1c46bfab1b6560ef8b6 (diff)
downloadabc-5fbe218ff8c9a150d2898eae4f454961274ef4eb.tar.gz
abc-5fbe218ff8c9a150d2898eae4f454961274ef4eb.tar.bz2
abc-5fbe218ff8c9a150d2898eae4f454961274ef4eb.zip
Improvements to ternary simulation.
Diffstat (limited to 'src/proof/pdr/pdrTsim3.c')
-rw-r--r--src/proof/pdr/pdrTsim3.c6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/proof/pdr/pdrTsim3.c b/src/proof/pdr/pdrTsim3.c
index c0822322..ebd1a702 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