Integration with several commands.

2 files changed, 4 insertions, 1 deletions

diff --git a/src/proof/dch/dch.h b/src/proof/dch/dch.h
index 5d644643..07f6a1d2 100644
--- a/src/proof/dch/dch.h
+++ b/src/proof/dch/dch.h
@@ -52,6 +52,7 @@ struct Dch_Pars_t_
     int              fPower;        // uses power-aware rewriting
     int              fUseGia;       // uses GIA package 
     int              fUseCSat;      // uses circuit-based solver
+    int              fUseNew;       // uses new implementation
     int              fLightSynth;   // uses lighter version of synthesis
     int              fSkipRedSupp;  // skip choices with redundant support vars
     int              fVerbose;      // verbose stats
diff --git a/src/proof/dch/dchCore.c b/src/proof/dch/dchCore.c
index 0da65bee..eef53e73 100644
--- a/src/proof/dch/dchCore.c
+++ b/src/proof/dch/dchCore.c
@@ -90,7 +90,7 @@ Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars )
 {
     Dch_Man_t * p;
     Aig_Man_t * pResult;
-    abctime clk, clkTotal = Abc_Clock();
+    abctime clk, clk2 = Abc_Clock(), clkTotal = Abc_Clock();
     // reset random numbers
     Aig_ManRandom(1);
     // start the choicing manager
@@ -106,6 +106,8 @@ p->timeSimInit = Abc_Clock() - clk;
     // free memory ahead of time
 p->timeTotal = Abc_Clock() - clkTotal;
     Dch_ManStop( p );
+    //if ( pPars->fVerbose ) 
+        Abc_PrintTime( 1, "Old choice computation time", Abc_Clock() - clk2 );
     // create choices
     ABC_FREE( pAig->pTable );
     pResult = Dch_DeriveChoiceAig( pAig, pPars->fSkipRedSupp );