summaryrefslogtreecommitdiffstats
path: root/src/proof/pdr/pdrInt.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/pdr/pdrInt.h')
-rw-r--r--src/proof/pdr/pdrInt.h3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index 89b6f0d0..dae20f0c 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -82,6 +82,7 @@ struct Pdr_Man_t_
Vec_Wec_t * vVLits; // CNF literals
// data representation
int iOutCur; // current output
+ int nPrioShift;// priority shift
Vec_Ptr_t * vCexes; // counter-examples for each output
Vec_Ptr_t * vSolvers; // SAT solvers
Vec_Vec_t * vClauses; // clauses by timeframe
@@ -121,6 +122,8 @@ struct Pdr_Man_t_
int nQueCur;
int nQueMax;
int nQueLim;
+ int nXsimRuns;
+ int nXsimLits;
// runtime
abctime timeToStop;
abctime timeToStopOne;