diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-05-25 13:47:38 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-05-25 13:47:38 -0700 |
commit | 1d26d58a17226230b40601c3dc40ef4851827a2e (patch) | |
tree | 847daf199197cc1f2f2f356458f579f60c8ebf9e /src/proof/pdr/pdr.h | |
parent | 58c81ec097d66abdd1ec77853cdcc95f842f12f2 (diff) | |
download | abc-1d26d58a17226230b40601c3dc40ef4851827a2e.tar.gz abc-1d26d58a17226230b40601c3dc40ef4851827a2e.tar.bz2 abc-1d26d58a17226230b40601c3dc40ef4851827a2e.zip |
Adding switch 'pdr -o' to control using property output in induction.
Diffstat (limited to 'src/proof/pdr/pdr.h')
-rw-r--r-- | src/proof/pdr/pdr.h | 1 |
1 files changed, 1 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 |