Fix for (user) context-dependence of arith TO_INT/IS_INT rewriting and rewrite-divk.

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 0c8ca7507b4e78c2c0a7052f318febc708912029..b0e66b564cde6e8039b19aa9def666e8c59217b9 100644 (file)
--- 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) {