diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-29 18:04:38 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-29 21:03:55 -0400 |
| commit | 99539e86f1b659a03b78c2bd9b3d1a55c93eaf71 (patch) | |
| tree | 18c77a3173e2e29f5c8065657676f9b68bfc3eb6 /src | |
| parent | c95872d478a9ff1f207b8945dba558ae4547f054 (diff) | |
Fix for (user) context-dependence of arith TO_INT/IS_INT rewriting and rewrite-divk.
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 4 |
1 files 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) { |