2 files changed, 17 insertions, 15 deletions
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index f1cac9044..4acf86d43 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -615,10 +615,10 @@ bool Constraint::wellFormedFarkasProof() const {
   ConstraintCP antecedent = d_database->d_antecedents[p];
   if(antecedent  == NullConstraint) { return false; }
 
-#ifdef CVC4_PROOF
+#if IS_PROOFS_BUILD
   if(!PROOF_ON()){ return cr.d_farkasCoefficients == RationalVectorCPSentinel; }
   Assert(PROOF_ON());
-  
+
   if(cr.d_farkasCoefficients == RationalVectorCPSentinel){ return false; }
   if(cr.d_farkasCoefficients->size() < 2){ return false; }
 
@@ -717,9 +717,9 @@ bool Constraint::wellFormedFarkasProof() const {
     (lhs.isNull() || Constant::isMember(lhs) && Constant(lhs).isZero() ) &&
     rhs.sgn() < 0;
 
-#else
+#else  /* IS_PROOFS_BUILD */
   return true;
-#endif
+#endif /* IS_PROOFS_BUILD */
 }
 
 ConstraintP Constraint::makeNegation(ArithVar v, ConstraintType t, const DeltaRational& r){
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 0e0b35020..877546da8 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -88,6 +88,8 @@
 #include "theory/arith/constraint_forward.h"
 #include "theory/arith/callbacks.h"
 
+#include "util/configuration_private.h"
+
 #include <vector>
 #include <list>
 #include <set>
@@ -299,17 +301,17 @@ struct ConstraintRule {
    * There is no requirement that the proof is minimal.
    * We do however use all of the constraints by requiring non-zero coefficients.
    */
-#ifdef CVC4_PROOF
+#if IS_PROOFS_BUILD
   RationalVectorCP d_farkasCoefficients;
-#endif
+#endif /* IS_PROOFS_BUILD */
   ConstraintRule()
     : d_constraint(NullConstraint)
     , d_proofType(NoAP)
     , d_antecedentEnd(AntecedentIdSentinel)
   {
-#ifdef CVC4_PROOF
+#if IS_PROOFS_BUILD
     d_farkasCoefficients = RationalVectorCPSentinel;
-#endif
+#endif /* IS_PROOFS_BUILD */
   }
 
   ConstraintRule(ConstraintP con, ArithProofType pt)
@@ -317,18 +319,18 @@ struct ConstraintRule {
     , d_proofType(pt)
     , d_antecedentEnd(AntecedentIdSentinel)
   {
-#ifdef CVC4_PROOF
+#if IS_PROOFS_BUILD
     d_farkasCoefficients = RationalVectorCPSentinel;
-#endif
+#endif /* IS_PROOFS_BUILD */
   }
   ConstraintRule(ConstraintP con, ArithProofType pt, AntecedentId antecedentEnd)
     : d_constraint(con)
     , d_proofType(pt)
     , d_antecedentEnd(antecedentEnd)
   {
-#ifdef CVC4_PROOF
+#if IS_PROOFS_BUILD
     d_farkasCoefficients = RationalVectorCPSentinel;
-#endif
+#endif /* IS_PROOFS_BUILD */
   }
 
   ConstraintRule(ConstraintP con, ArithProofType pt, AntecedentId antecedentEnd, RationalVectorCP coeffs)
@@ -337,11 +339,11 @@ struct ConstraintRule {
     , d_antecedentEnd(antecedentEnd)
   {
     Assert(PROOF_ON() || coeffs == RationalVectorCPSentinel);
-#ifdef CVC4_PROOF
+#if IS_PROOFS_BUILD
     d_farkasCoefficients = coeffs;
-#endif
+#endif /* IS_PROOFS_BUILD */
   }
-  
+
   void print(std::ostream& out) const;
   void debugPrint() const;
 }; /* class ConstraintRule */