- Merges queue-interrogation branch into the trunk. This branch adds extra phases of looking for additional conflicts during and after the heuristic pivoting stage. (For the expected performance gain, comparing jobs 1676 and 1643 gives a rough idea.)

1 files changed, 3 insertions, 2 deletions

diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 544f49a06..c6bc3c434 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -150,9 +150,9 @@ public:
 private:
   template <PreferenceFunction> Node searchForFeasibleSolution(uint32_t maxIterations);
 
-  enum SearchPeriod {BeforeDiffSearch, AfterDiffSearch, DuringVarOrderSearch};
+  enum SearchPeriod {BeforeDiffSearch, DuringDiffSearch, AfterDiffSearch, DuringVarOrderSearch};
 
-  Node findConflictOnTheQueue(SearchPeriod period);
+  Node findConflictOnTheQueue(SearchPeriod period, bool returnFirst = true);
 
 
   /**
@@ -270,6 +270,7 @@ private:
 
     IntStat d_attemptBeforeDiffSearch, d_successBeforeDiffSearch;
     IntStat d_attemptAfterDiffSearch, d_successAfterDiffSearch;
+    IntStat d_attemptDuringDiffSearch, d_successDuringDiffSearch;
     IntStat d_attemptDuringVarOrderSearch, d_successDuringVarOrderSearch;
 
     IntStat d_delayedConflicts;