Fixing a use after free bug in Polynomial::denominatorLCM.

diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index d7c580395d791294be05877d1777f15a76ba871a..ec396b24e57d714af5076f794ed01c86c9bd9032 100644 (file)
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -528,14 +528,13 @@ Integer Polynomial::numeratorGCD() const {
 
 Integer Polynomial::denominatorLCM() const {
   Integer tmp(1);
-  for(iterator i=begin(), e=end(); i!=e; ++i){
-    const Constant& c = (*i).getConstant();
-    tmp = tmp.lcm(c.getValue().getDenominator());
+  for (iterator i = begin(), e = end(); i != e; ++i) {
+    const Integer denominator = (*i).getConstant().getValue().getDenominator();
+    tmp = tmp.lcm(denominator);
   }
   return tmp;
 }
 
-
 Constant Polynomial::getCoefficient(const VarList& vl) const{
   //TODO improve to binary search...
   for(iterator iter=begin(), myend=end(); iter != myend; ++iter){

diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index fecb06811634914982d93dec6c762ab86968c765..66f878b1a95699d541164c2bdec65b24ef34f430 100644 (file)
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -30,7 +30,8 @@ namespace arith {
 
 
 SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc)
-  : d_conflictVariables()
+    : d_pivots(0),
+      d_conflictVariables()
   , d_linEq(linEq)
   , d_variables(d_linEq.getVariables())
   , d_tableau(d_linEq.getTableau())
@@ -43,7 +44,6 @@ SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq,
   , d_zero(0)
   , d_posOne(1)
   , d_negOne(-1)
-  , d_pivots(0)
 {
   d_heuristicRule = options::arithErrorSelectionRule();
   d_errorSet.setSelectionRule(d_heuristicRule);