From 142eb96736ffd643885bacbcf9b82f219f86c707 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 24 Aug 2016 21:06:13 +0200
Subject: [PATCH] hopefully fixing cudd's min/maxAbstractRepresentative

Former-commit-id: 06564ba2c2a6facaa36d02c9cb5b4ac075b26097
---
 .../3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c     | 71 +++++++++----------
 1 file changed, 34 insertions(+), 37 deletions(-)

diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c
index 57c23d189..9ba2ab69a 100644
--- a/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c
+++ b/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c
@@ -1003,27 +1003,25 @@ cuddAddMinAbstractRepresentativeRecur(
     logicalZero = Cudd_Not(one);
     
     /* Cube is guaranteed to be a cube at this point. */
+    if (cuddIsConstant(cube)) {
+        return one;
+    }
     if (cuddIsConstant(f)) {
-        if (cuddIsConstant(cube)) {
-            return one;
-        } else {
-            res = cuddBddExistAbstractRepresentativeRecur(manager, f, cuddT(cube));
-            if (res == NULL) {
-                return(NULL);
-            }
-            cuddRef(res);
+        res = cuddBddExistAbstractRepresentativeRecur(manager, f, cuddT(cube));
+        if (res == NULL) {
+            return(NULL);
+        }
+        cuddRef(res);
             
-            // We build in the negation ourselves.
-            res1 = cuddUniqueInter(manager, (int) cube->index, one, Cudd_Not(res));
-            if (res1 == NULL) {
-                Cudd_IterDerefBdd(manager,res);
-                return(NULL);
-            }
-            res1 = Cudd_Not(res1);
-            cuddDeref(res);
-            return(res1);
-
+        // We build in the negation ourselves.
+        res1 = cuddUniqueInter(manager, (int) cube->index, one, Cudd_Not(res));
+        if (res1 == NULL) {
+            Cudd_IterDerefBdd(manager,res);
+            return(NULL);
         }
+        res1 = Cudd_Not(res1);
+        cuddDeref(res);
+        return(res1);
     }
     
     /* Abstract a variable that does not appear in f. */
@@ -1191,27 +1189,26 @@ cuddAddMaxAbstractRepresentativeRecur(
     logicalZero = Cudd_Not(one);
     
     /* Cube is guaranteed to be a cube at this point. */
+    if (cuddIsConstant(cube)) {
+        return one;
+    }
     if (cuddIsConstant(f)) {
-        if (cuddIsConstant(cube)) {
-            return one;
-        } else {
-            res = cuddBddExistAbstractRepresentativeRecur(manager, f, cuddT(cube));
-            if (res == NULL) {
-                return(NULL);
-            }
-            cuddRef(res);
-            
-            // We build in the negation ourselves.
-            res1 = cuddUniqueInter(manager, (int) cube->index, one, Cudd_Not(res));
-            if (res1 == NULL) {
-                Cudd_IterDerefBdd(manager,res);
-                return(NULL);
-            }
-            res1 = Cudd_Not(res1);
-            cuddDeref(res);
-            return(res1);
-            
+        res = cuddBddExistAbstractRepresentativeRecur(manager, f, cuddT(cube));
+        if (res == NULL) {
+            return(NULL);
+        }
+        cuddRef(res);
+        
+        // We build in the negation ourselves.
+        res1 = cuddUniqueInter(manager, (int) cube->index, one, Cudd_Not(res));
+        if (res1 == NULL) {
+            Cudd_IterDerefBdd(manager,res);
+            return(NULL);
         }
+        res1 = Cudd_Not(res1);
+        cuddDeref(res);
+        return(res1);
+            
     }
     
     /* Abstract a variable that does not appear in f. */