From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 29 Apr 2014 22:04:38 +0000 (-0400)
Subject: Fix for (user) context-dependence of arith TO_INT/IS_INT rewriting and rewrite-divk.
X-Git-Tag: cvc5-1.0.0~6944
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=99539e86f1b659a03b78c2bd9b3d1a55c93eaf71;p=cvc5.git

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 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) {