From 99539e86f1b659a03b78c2bd9b3d1a55c93eaf71 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 29 Apr 2014 18:04:38 -0400
Subject: [PATCH] Fix for (user) context-dependence of arith TO_INT/IS_INT
 rewriting and rewrite-divk.

---
 src/theory/arith/theory_arith_private.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 0c8ca7507..b0e66b564 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1060,13 +1060,13 @@ namespace attr {
  * This attribute maps the child of a to_int / is_int to the
  * corresponding integer skolem.
  */
-typedef expr::Attribute<attr::ToIntegerTag, Node> ToIntegerAttr;
+typedef expr::CDAttribute<attr::ToIntegerTag, Node> ToIntegerAttr;
 
 /**
  * This attribute maps division-by-constant-k terms to a variable
  * used to eliminate them.
  */
-typedef expr::Attribute<attr::LinearIntDivTag, Node> LinearIntDivAttr;
+typedef expr::CDAttribute<attr::LinearIntDivTag, Node> LinearIntDivAttr;
 
 Node TheoryArithPrivate::ppRewriteTerms(TNode n) {
   if(Theory::theoryOf(n) != THEORY_ARITH) {
-- 
2.30.2