1 files changed, 8 insertions, 6 deletions
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index f0dc5d62e..b3f43baf1 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -43,6 +43,8 @@ private:
   PermissiveBackArithVarSet d_updatedBounds;
   PermissiveBackArithVarSet d_candidateBasics;
 
+  ArithVarMultiset d_pivotsInRound;
+
   Rational d_ZERO;
   DeltaRational d_DELTA_ZERO;
 
@@ -139,7 +141,7 @@ public:
    */
   Node updateInconsistentVars();
 private:
-  template <PreferenceFunction> Node searchForFeasibleSolution(uint32_t maxIterations);
+  Node searchForFeasibleSolution(uint32_t maxIterations);
 
   enum SearchPeriod {BeforeDiffSearch, DuringDiffSearch, AfterDiffSearch, DuringVarOrderSearch, AfterVarOrderSearch};
 
@@ -159,12 +161,12 @@ private:
    * - !lowerBound && a_ij < 0 && assignment(x_j) > lowerbound(x_j)
    *
    */
-  template <bool lowerBound, PreferenceFunction>  ArithVar selectSlack(ArithVar x_i);
-  template <PreferenceFunction pf> ArithVar selectSlackLowerBound(ArithVar x_i) {
-    return selectSlack<true, pf>(x_i);
+  template <bool lowerBound>  ArithVar selectSlack(ArithVar x_i, PreferenceFunction pf);
+  ArithVar selectSlackLowerBound(ArithVar x_i, PreferenceFunction pf = minVarOrder) {
+    return selectSlack<true>(x_i, pf);
   }
-  template <PreferenceFunction pf> ArithVar selectSlackUpperBound(ArithVar x_i) {
-    return selectSlack<false, pf>(x_i);
+  ArithVar selectSlackUpperBound(ArithVar x_i, PreferenceFunction pf = minVarOrder) {
+    return selectSlack<false>(x_i, pf);
   }
   /**
    * Returns the smallest basic variable whose assignment is not consistent