1 files changed, 13 insertions, 11 deletions
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 */