Improvements to inductive generalization in IC3/PDR by Zyad Hassan.

1 files changed, 3 insertions, 0 deletions

diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index 529a161f..b73a54df 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -49,6 +49,7 @@ struct Pdr_Par_t_
     int nTimeOut;         // timeout in seconds
     int nTimeOutGap;      // approximate timeout in seconds since the last change
     int nTimeOutOne;      // approximate timeout in seconds per one output
+    int nRandomSeed;      // value to seed the SAT solver with
     int fTwoRounds;       // use two rounds for generalization
     int fMonoCnf;         // monolythic CNF
     int fDumpInv;         // dump inductive invariant
@@ -57,6 +58,8 @@ struct Pdr_Par_t_
     int fShiftStart;      // allows clause pushing to start from an intermediate frame
     int fReuseProofOblig; // reuses proof-obligationgs in the last timeframe
     int fSkipGeneral;     // skips expensive generalization step
+    int fSkipDown;        // skips the application of down
+    int fCtgs;            // handle CTGs in down
     int fVerbose;         // verbose output`
     int fVeryVerbose;     // very verbose output
     int fNotVerbose;      // not printing line by line progress