Fix to the context dependent static learning code.

diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index af2f0c9bcc1ff3aa984d11946616451c0019f145..5b8d3befc22bead85275e64b517fd2b745531e78 100644 (file)
--- 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) {