diff options
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/pdr/pdr.h | 1 | ||||
| -rw-r--r-- | src/proof/pdr/pdrCore.c | 1 | ||||
| -rw-r--r-- | src/proof/pdr/pdrSat.c | 2 |
3 files changed, 4 insertions, 0 deletions
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index e4b764a1..3dffac17 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -63,6 +63,7 @@ struct Pdr_Par_t_ int fSolveAll; // do not stop when found a SAT output int fStoreCex; // enable storing counter-examples in MO mode int fUseBridge; // use bridge interface + int fUsePropOut; // use property output int nFailOuts; // the number of failed outputs int nDropOuts; // the number of timed out outputs int nProveOuts; // the number of proved outputs diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 8e81795b..5b619f4b 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -61,6 +61,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ) pPars->fMonoCnf = 0; // monolythic CNF pPars->fDumpInv = 0; // dump inductive invariant pPars->fShortest = 0; // forces bug traces to be shortest + pPars->fUsePropOut = 1; // use property output pPars->fVerbose = 0; // verbose output pPars->fVeryVerbose = 0; // very verbose output pPars->fNotVerbose = 0; // not printing line-by-line progress diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c index f3681adb..2e6130aa 100644 --- a/src/proof/pdr/pdrSat.c +++ b/src/proof/pdr/pdrSat.c @@ -179,6 +179,8 @@ void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k ) sat_solver * pSat; Aig_Obj_t * pObj; int Lit, RetValue, i; + if ( !p->pPars->fUsePropOut ) + return; pSat = Pdr_ManSolver(p, k); Saig_ManForEachPo( p->pAig, pObj, i ) { |