From 15096acfc11a251641ec640704dcab3d431a8b22 Mon Sep 17 00:00:00 2001
From: skimo <skimo>
Date: Tue, 22 Jun 2004 06:49:36 +0000
Subject: [PATCH] remove reduced relations

---
 ev_operations.c | 39 +++++++++++++++++++++++++--------------
 1 file changed, 25 insertions(+), 14 deletions(-)

diff --git a/ev_operations.c b/ev_operations.c
index d0a8cae..c4ffbd6 100644
--- a/ev_operations.c
+++ b/ev_operations.c
@@ -491,22 +491,33 @@ you_lose:   	/* OK, lets not do it */
 	    free_evalue_refs(&(p->arr[0]));
 	    evalue_set_si(e, 0, 1);
 	    free(p);
-	} else if (value_notzero_p(p->arr[0].d)) {
-	    if (value_zero_p(p->arr[0].x.n)) {
-		value_clear(e->d);
-		memcpy(e,&p->arr[1],sizeof(evalue));
-		if (p->size == 3)
-		    free_evalue_refs(&(p->arr[2]));
-	    } else {
-		if (p->size == 3) {
+	} else {
+	    int reduced = 0;
+	    evalue *m;
+	    m = &p->arr[0];
+	    /* Relation was reduced by means of an identical 
+	     * inequality => remove 
+	     */
+	    if (value_zero_p(m->d) && !EVALUE_IS_ZERO(m->x.p->arr[1]))
+		reduced = 1;
+
+	    if (reduced || value_notzero_p(p->arr[0].d)) {
+		if (value_zero_p(p->arr[0].x.n)) {
 		    value_clear(e->d);
-		    memcpy(e,&p->arr[2],sizeof(evalue));
-		} else
-		    evalue_set_si(e, 0, 1);
-		free_evalue_refs(&(p->arr[1]));
+		    memcpy(e,&p->arr[1],sizeof(evalue));
+		    if (p->size == 3)
+			free_evalue_refs(&(p->arr[2]));
+		} else {
+		    if (p->size == 3) {
+			value_clear(e->d);
+			memcpy(e,&p->arr[2],sizeof(evalue));
+		    } else
+			evalue_set_si(e, 0, 1);
+		    free_evalue_refs(&(p->arr[1]));
+		}
+		free_evalue_refs(&(p->arr[0]));
+		free(p);
 	    }
-	    free_evalue_refs(&(p->arr[0]));
-	    free(p);
 	}
     }
     return;
-- 
2.11.4.GIT