From dae3cd450bb7508fd8811f12c3d286579e87e366 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 17 Mar 2020 14:46:46 -0700
Subject: [PATCH] fix a bug in nex_creator, already fixed in debug branch
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
src/math/lp/nex_creator.cpp | 7 ++++++-
1 file changed, 6 insertions(+), 1 deletion(-)
diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp
index b2b7a4910..f9b1aeaed 100644
--- a/src/math/lp/nex_creator.cpp
+++ b/src/math/lp/nex_creator.cpp
@@ -156,7 +156,12 @@ bool nex_creator::gt_on_var_nex(const nex_var& a, const nex& b) const {
return b.get_degree() <= 1 && gt_on_var_nex(a, *b.to_mul()[0].e());
case expr_type::SUM:
SASSERT(b.size() > 1);
- return gt(&a, b.to_sum()[0]);
+ if(gt(&a, b.to_sum()[0]))
+ return true;
+ if (gt(b.to_sum()[0], &a ))
+ return false;
+ return true;
+
default:
UNREACHABLE();
return false;