summaryrefslogtreecommitdiffstats
path: root/src/proof/pdr/pdr.h
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2016-05-25 13:47:38 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2016-05-25 13:47:38 -0700
commit1d26d58a17226230b40601c3dc40ef4851827a2e (patch)
tree847daf199197cc1f2f2f356458f579f60c8ebf9e /src/proof/pdr/pdr.h
parent58c81ec097d66abdd1ec77853cdcc95f842f12f2 (diff)
downloadabc-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.h1
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