From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 31 May 2017 18:08:20 +0000 (-0500)
Subject: Minor fix to last commit.
X-Git-Tag: cvc5-1.0.0~5784
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b9f47b4c948e2aab68303a14903e60bee0a449b8;p=cvc5.git

Minor fix to last commit.
---

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 23b846946..250317b78 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1214,7 +1214,7 @@ Node TheoryArithPrivate::ppRewriteTerms(TNode n) {
     NodeMap::const_iterator it = d_int_div_skolem.find( rw );
     if( it==d_int_div_skolem.end() ){
       intVar = nm->mkSkolem("linearIntDiv", nm->integerType(), "the result of an intdiv-by-k term");
-      d_div_skolem[rw] = intVar;
+      d_int_div_skolem[rw] = intVar;
       Node lem;
       if (den.isConst()) {
         const Rational& rat = den.getConst<Rational>();