1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index a4dfb1fa4..bf5261439 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -182,6 +182,12 @@ void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){
     e = tmp;
     k = reverseRelationKind(k);
   }
+  //(ite (< x y) x y)
+  //(ite (x < y) x y)
+  //(ite (x - y < 0) x y)
+  // ----------------
+  // (ite (x - y < -c) )
+
   if(t == cleft && e == cright){
     // t == cleft && e == cright
     Assert( t == cleft );