5 files changed, 41 insertions, 14 deletions
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 466f8626f..e6ef6fdc2 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -56,6 +56,7 @@ libarith_la_SOURCES = \
 	pure_update_simplex.cpp \
 	theory_arith.h \
 	theory_arith.cpp \
+	theory_arith_private_forward.h \
 	theory_arith_private.h \
 	theory_arith_private.cpp \
 	dio_solver.h \
diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h
index 0d24fa099..27ac6ccd2 100644
--- a/src/theory/arith/error_set.h
+++ b/src/theory/arith/error_set.h
@@ -29,6 +29,22 @@
 
 #include "util/statistics_registry.h"
 //#include <boost/heap/d_ary_heap.hpp>
+
+#if CVC4_GCC_HAS_PB_DS_BUG
+   // Unfortunate bug in some older GCCs (e.g., v4.2):
+   //   http://gcc.gnu.org/bugzilla/show_bug.cgi?id=36612
+   // Requires some header-hacking to work around
+#  define __throw_container_error inline __throw_container_error
+#  define __throw_insert_error inline __throw_insert_error
+#  define __throw_join_error inline __throw_join_error
+#  define __throw_resize_error inline __throw_resize_error
+#  include <ext/pb_ds/exception.hpp>
+#  undef __throw_container_error
+#  undef __throw_insert_error
+#  undef __throw_join_error
+#  undef __throw_resize_error
+#endif /* CVC4_GCC_HAS_PB_DS_BUG */
+
 #include <ext/pb_ds/priority_queue.hpp>
 
 #include <vector>
@@ -87,10 +103,10 @@ public:
 //
 // typedef FocusSet::handle_type FocusSetHandle;
 
-typedef  __gnu_pbds::priority_queue<
+typedef CVC4_PB_DS_NAMESPACE::priority_queue<
   ArithVar,
   ComparatorPivotRule,
-  __gnu_pbds::pairing_heap_tag> FocusSet;
+  CVC4_PB_DS_NAMESPACE::pairing_heap_tag> FocusSet;
 
 typedef FocusSet::point_iterator FocusSetHandle;
 
diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h
index 0dafa83ff..51514bcfb 100644
--- a/src/theory/arith/fc_simplex.h
+++ b/src/theory/arith/fc_simplex.h
@@ -146,9 +146,11 @@ private:
   LinearEqualityModule::UpdatePreferenceFunction selectLeavingFunction(ArithVar x){
     bool useBlands = d_leavingCountSinceImprovement.isKey(x) &&
       d_leavingCountSinceImprovement[x] >= s_maxDegeneratePivotsBeforeBlandsOnEntering;
-    return useBlands ?
-      &LinearEqualityModule::preferWitness<false>:
-      &LinearEqualityModule::preferWitness<true>;
+    if(useBlands) {
+      return &LinearEqualityModule::preferWitness<false>;
+    } else {
+      return &LinearEqualityModule::preferWitness<true>;
+    }
   }
 
   bool debugDualLike(WitnessImprovement w, std::ostream& out,
@@ -183,9 +185,12 @@ private:
   UpdateInfo selectUpdateForPrimal(ArithVar basic, bool useBlands){
     TimerStat::CodeTimer codeTimer(d_statistics.d_selectUpdateForPrimal);
 
-    LinearEqualityModule::UpdatePreferenceFunction upf = useBlands ?
-      &LinearEqualityModule::preferWitness<false>:
-      &LinearEqualityModule::preferWitness<true>;
+    LinearEqualityModule::UpdatePreferenceFunction upf;
+    if(useBlands) {
+      upf = &LinearEqualityModule::preferWitness<false>;
+    } else {
+      upf = &LinearEqualityModule::preferWitness<true>;
+    }
 
     LinearEqualityModule::VarPreferenceFunction bpf = useBlands ?
       &LinearEqualityModule::minVarOrder :
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index ef00807f7..b6949c526 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -674,9 +674,12 @@ WitnessImprovement SumOfInfeasibilitiesSPD::soiRound() {
   Assert(d_soiVar != ARITHVAR_SENTINEL);
 
   bool useBlands = degeneratePivotsInARow() >= s_maxDegeneratePivotsBeforeBlandsOnLeaving;
-  LinearEqualityModule::UpdatePreferenceFunction upf = useBlands ?
-    &LinearEqualityModule::preferWitness<false>:
-    &LinearEqualityModule::preferWitness<true>;
+  LinearEqualityModule::UpdatePreferenceFunction upf;
+  if(useBlands) {
+    upf = &LinearEqualityModule::preferWitness<false>;
+  } else {
+    upf = &LinearEqualityModule::preferWitness<true>;
+  }
 
   LinearEqualityModule::VarPreferenceFunction bpf = useBlands ?
     &LinearEqualityModule::minVarOrder :
diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h
index 1a6becccb..006839a55 100644
--- a/src/theory/arith/soi_simplex.h
+++ b/src/theory/arith/soi_simplex.h
@@ -122,9 +122,11 @@ private:
   LinearEqualityModule::UpdatePreferenceFunction selectLeavingFunction(ArithVar x){
     bool useBlands = d_leavingCountSinceImprovement.isKey(x) &&
       d_leavingCountSinceImprovement[x] >= s_maxDegeneratePivotsBeforeBlandsOnEntering;
-    return useBlands ?
-      &LinearEqualityModule::preferWitness<false>:
-      &LinearEqualityModule::preferWitness<true>;
+    if(useBlands) {
+      return &LinearEqualityModule::preferWitness<false>;
+    } else {
+      return &LinearEqualityModule::preferWitness<true>;
+    }
   }
 
   bool debugSOI(WitnessImprovement w, std::ostream& out, int instance) const;