1 files changed, 18 insertions, 12 deletions
diff --git a/src/theory/arith/pseudoboolean_proc.cpp b/src/theory/arith/pseudoboolean_proc.cpp
index 230cfb7ca..1cdb90e20 100644
--- a/src/theory/arith/pseudoboolean_proc.cpp
+++ b/src/theory/arith/pseudoboolean_proc.cpp
@@ -15,10 +15,11 @@
  ** \todo document this file
  **/
 
+#include "theory/arith/pseudoboolean_proc.h"
+
 #include "base/output.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/normal_form.h"
-#include "theory/arith/pseudoboolean_proc.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
@@ -58,24 +59,30 @@ bool PseudoBooleanProcessor::decomposeAssertion(Node assertion, bool negated){
 
   Polynomial p = Polynomial::parsePolynomial(l);
   clear();
-  if(negated){
+  if (negated)
+  {
     // (not (>= p r))
     // (< p r)
     // (> (-p) (-r))
     // (>= (-p) (-r +1))
     d_off = (-r.getConst<Rational>());
 
-    if(d_off.constValue().isIntegral()){
-      d_off = d_off.constValue() + Rational(1) ;
-    }else{
-      d_off = Rational(d_off.constValue().ceiling());
+    if (d_off.value().isIntegral())
+    {
+      d_off = d_off.value() + Rational(1);
     }
-  }else{
+    else
+    {
+      d_off = Rational(d_off.value().ceiling());
+    }
+  }
+  else
+  {
     // (>= p r)
     d_off = r.getConst<Rational>();
-    d_off = Rational(d_off.constValue().ceiling());
+    d_off = Rational(d_off.value().ceiling());
   }
-  Assert(d_off.constValue().isIntegral());
+  Assert(d_off.value().isIntegral());
 
   int adj = negated ? -1 : 1;
   for(Polynomial::iterator i=p.begin(), end=p.end(); i != end; ++i){
@@ -247,8 +254,8 @@ void PseudoBooleanProcessor::learnGeqSub(Node geq){
     Debug("pbs::rewrites") << "failed " << std::endl;
     return;
   }
-  Assert(d_off.constValue().isIntegral());
-  Integer off = d_off.constValue().ceiling();
+  Assert(d_off.value().isIntegral());
+  Integer off = d_off.value().ceiling();
 
   // \sum pos >= \sum neg + off
 
@@ -323,4 +330,3 @@ void PseudoBooleanProcessor::clear() {
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
-