From d098dfe326e175b058212b098c75dadd3e4df256 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@microsoft.com>
Date: Sat, 9 Jan 2016 01:35:30 -0800
Subject: [PATCH] dev(lp): fix infeasibility evidence check

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
---
 src/util/lp/lar_solver.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 3f50a7996..2591a9fe7 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -451,7 +451,7 @@ public:
             if (kind == GE || kind == GT) n_of_G++;
             else if (kind == LE || kind == LT) n_of_L++;
         }
-        the_kind_of_sum = n_of_G? GE : LE;
+        the_kind_of_sum = n_of_G? GE : (n_of_L? LE : EQ);
         if (strict)
             the_kind_of_sum = static_cast<lconstraint_kind>((static_cast<int>(the_kind_of_sum)/2));