diff options
| author | Tim King <taking@cs.nyu.edu> | 2012-11-05 23:52:22 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2012-11-05 23:52:22 +0000 |
| commit | 08c6ab35a95c006969c9c966f01c6fd9ba9c8af1 (patch) | |
| tree | 16ab48b8e36539855ff7cf793f3ea5cf3fef3bd6 /src/theory/arith/arith_static_learner.cpp | |
| parent | 44ee91efd25f0c64e1ef5d932280935f20403512 (diff) | |
Fix to the context dependent static learning code.
Diffstat (limited to 'src/theory/arith/arith_static_learner.cpp')
| -rw-r--r-- | src/theory/arith/arith_static_learner.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index af2f0c9bc..5b8d3befc 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -262,8 +262,8 @@ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){ } if (d_maxMap.find(n[1]) != d_maxMap.end() && d_maxMap.find(n[2]) != d_maxMap.end()) { - const DeltaRational& first = d_minMap[n[1]]; - const DeltaRational& second = d_minMap[n[2]]; + const DeltaRational& first = d_maxMap[n[1]]; + const DeltaRational& second = d_maxMap[n[2]]; DeltaRational max = std::max(first, second); CDNodeToMinMaxMap::const_iterator maxFind = d_maxMap.find(n); if (maxFind == d_maxMap.end() || (*maxFind).second > max) { |