From 08c6ab35a95c006969c9c966f01c6fd9ba9c8af1 Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 5 Nov 2012 23:52:22 +0000 Subject: [PATCH] Fix to the context dependent static learning code. --- src/theory/arith/arith_static_learner.cpp | 4 ++-- 1 file 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) { -- 2.30.2