diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-05-31 13:08:20 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-05-31 13:08:20 -0500 |
| commit | b9f47b4c948e2aab68303a14903e60bee0a449b8 (patch) | |
| tree | 8f8db43e71fe90640cbbef01e25db35c4b6b026e /src/theory | |
| parent | 97f67691287a001412dbb2ddb4a372f204b27498 (diff) | |
Minor fix to last commit.
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
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>(); |