From: Tim King <taking@cs.nyu.edu>
Date: Mon, 5 Nov 2012 23:52:22 +0000 (+0000)
Subject: Fix to the context dependent static learning code.
X-Git-Tag: cvc5-1.0.0~7648
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=08c6ab35a95c006969c9c966f01c6fd9ba9c8af1;p=cvc5.git

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 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) {