From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 27 Jun 2013 19:34:32 +0000 (-0400)
Subject: Small fix for IS_INTEGER.
X-Git-Tag: cvc5-1.0.0~7287^2~81
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e6f4f9fbd3e2e3471f0df46959e3924368f31bdb;p=cvc5.git

Small fix for IS_INTEGER.
---

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index a01397973..f5b1d20ce 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -775,7 +775,7 @@ Node TheoryArithPrivate::ppRewriteTerms(TNode n) {
       Node node = intVar;
       return node;
     } else {
-      Node node = nm->mkNode(kind::EQUAL, node[0], intVar);
+      Node node = nm->mkNode(kind::EQUAL, n[0], intVar);
       return node;
     }
     Unreachable();