Fix to bug 211. ArithVar is now typedefed to uint32_t.

1 files changed, 13 insertions, 3 deletions

diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 4ae0e44ef..f099e77b9 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -33,18 +33,28 @@ namespace theory {
 namespace arith {
 
 
-typedef uint64_t ArithVar;
+typedef uint32_t ArithVar;
 //static const ArithVar ARITHVAR_SENTINEL = std::numeric_limits<ArithVar>::max();
 #define ARITHVAR_SENTINEL std::numeric_limits<ArithVar>::max()
 
 struct ArithVarAttrID{};
-typedef expr::Attribute<ArithVarAttrID,ArithVar> ArithVarAttr;
+typedef expr::Attribute<ArithVarAttrID,uint64_t> ArithVarAttr;
+
+inline bool hasArithVar(TNode x){
+  return x.hasAttribute(ArithVarAttr());
+}
 
 inline ArithVar asArithVar(TNode x){
-  Assert(x.hasAttribute(ArithVarAttr()));
+  Assert(hasArithVar(x));
+  Assert(x.getAttribute(ArithVarAttr()) <= ARITHVAR_SENTINEL);
   return x.getAttribute(ArithVarAttr());
 }
 
+inline void setArithVar(TNode x, ArithVar a){
+  Assert(!hasArithVar(x));
+  return x.setAttribute(ArithVarAttr(), (uint64_t)a);
+}
+
 inline Node mkRationalNode(const Rational& q){
   return NodeManager::currentNM()->mkConst<Rational>(q);
 }