diff --git a/polly/lib/External/isl/GIT_HEAD_ID b/polly/lib/External/isl/GIT_HEAD_ID
index 8ab3716e9b34..e49f3f3884c7 100644
--- a/polly/lib/External/isl/GIT_HEAD_ID
+++ b/polly/lib/External/isl/GIT_HEAD_ID
@@ -1 +1 @@
-isl-0.17.1-57-g1879898
+isl-0.17.1-84-g72ffe88
diff --git a/polly/lib/External/isl/doc/Makefile.am b/polly/lib/External/isl/doc/Makefile.am
index a2def5a6783a..1d61dd7775a4 100644
--- a/polly/lib/External/isl/doc/Makefile.am
+++ b/polly/lib/External/isl/doc/Makefile.am
@@ -9,7 +9,9 @@ CLEANFILES = \
 	manual.out \
 	manual.blg \
 	manual.log \
-	manual.brf
+	manual.brf \
+	manual.bcf \
+	manual.run.xml
 
 if GENERATE_DOC
 export TEXINPUTS := $(srcdir):$(TEXINPUTS)
diff --git a/polly/lib/External/isl/doc/Makefile.in b/polly/lib/External/isl/doc/Makefile.in
index c66b1fad8bcd..3fb01043fc2a 100644
--- a/polly/lib/External/isl/doc/Makefile.in
+++ b/polly/lib/External/isl/doc/Makefile.in
@@ -283,7 +283,9 @@ CLEANFILES = \
 	manual.out \
 	manual.blg \
 	manual.log \
-	manual.brf
+	manual.brf \
+	manual.bcf \
+	manual.run.xml
 
 all: all-am
 
diff --git a/polly/lib/External/isl/doc/manual.pdf b/polly/lib/External/isl/doc/manual.pdf
index 9c6c0241c34e..fd8bb1e72c05 100644
Binary files a/polly/lib/External/isl/doc/manual.pdf and b/polly/lib/External/isl/doc/manual.pdf differ
diff --git a/polly/lib/External/isl/doc/user.pod b/polly/lib/External/isl/doc/user.pod
index 8491cbe8fd2c..97d2e2e67039 100644
--- a/polly/lib/External/isl/doc/user.pod
+++ b/polly/lib/External/isl/doc/user.pod
@@ -3457,6 +3457,12 @@ be created.
 	__isl_give isl_printer *isl_printer_to_str(isl_ctx *ctx);
 	__isl_null isl_printer *isl_printer_free(
 		__isl_take isl_printer *printer);
+
+C<isl_printer_to_file> prints to the given file, while
+C<isl_printer_to_str> prints to a string that can be extracted
+using the following function.
+
+	#include <isl/printer.h>
 	__isl_give char *isl_printer_get_str(
 		__isl_keep isl_printer *printer);
 
@@ -8189,6 +8195,9 @@ Several node types have their own functions for querying
 	isl_schedule_node_band_set_ast_build_options(
 		__isl_take isl_schedule_node *node,
 		__isl_take isl_union_set *options);
+	__isl_give isl_set *
+	isl_schedule_node_band_get_ast_isolate_option(
+		__isl_keep isl_schedule_node *node);
 
 The function C<isl_schedule_node_band_get_space> returns the space
 of the partial schedule of the band.
@@ -8217,6 +8226,9 @@ may return C<isl_ast_loop_error> if an error occurs.
 The AST build options govern how an AST is generated for
 the individual schedule dimensions during AST generation.
 See L</"AST Generation Options (Schedule Tree)">.
+The isolate option for the given node can be extracted from these
+AST build options using the function
+C<isl_schedule_node_band_get_ast_isolate_option>.
 
 	#include <isl/schedule_node.h>
 	__isl_give isl_set *
@@ -8498,6 +8510,8 @@ using the following function.
 The resulting outer band node contains the first C<pos> dimensions of
 the schedule of C<node> while the inner band contains the remaining dimensions.
 The schedules of the two band nodes live in anonymous spaces.
+The loop AST generation type options and the isolate option
+are split over the the two band nodes.
 
 A band node can be moved down to the leaves of the subtree rooted
 at the band node using the following function.
diff --git a/polly/lib/External/isl/include/isl/schedule_node.h b/polly/lib/External/isl/include/isl/schedule_node.h
index 0ddc81f36190..51b31f9a4f0d 100644
--- a/polly/lib/External/isl/include/isl/schedule_node.h
+++ b/polly/lib/External/isl/include/isl/schedule_node.h
@@ -110,6 +110,8 @@ __isl_give isl_union_set *isl_schedule_node_band_get_ast_build_options(
 	__isl_keep isl_schedule_node *node);
 __isl_give isl_schedule_node *isl_schedule_node_band_set_ast_build_options(
 	__isl_take isl_schedule_node *node, __isl_take isl_union_set *options);
+__isl_give isl_set *isl_schedule_node_band_get_ast_isolate_option(
+	__isl_keep isl_schedule_node *node);
 unsigned isl_schedule_node_band_n_member(__isl_keep isl_schedule_node *node);
 __isl_export
 isl_bool isl_schedule_node_band_member_get_coincident(
diff --git a/polly/lib/External/isl/isl_ast_build.c b/polly/lib/External/isl/isl_ast_build.c
index 9418006fd145..bc208e19cc2c 100644
--- a/polly/lib/External/isl/isl_ast_build.c
+++ b/polly/lib/External/isl/isl_ast_build.c
@@ -2387,9 +2387,6 @@ enum isl_ast_loop_type isl_ast_build_get_loop_type(
 __isl_give isl_ast_build *isl_ast_build_extract_isolated(
 	__isl_take isl_ast_build *build)
 {
-	isl_space *space, *space2;
-	isl_union_set *options;
-	int n, n2;
 	isl_set *isolated;
 
 	if (!build)
@@ -2403,27 +2400,7 @@ __isl_give isl_ast_build *isl_ast_build_extract_isolated(
 	if (!build)
 		return NULL;
 
-	options = isl_schedule_node_band_get_ast_build_options(build->node);
-
-	space = isl_multi_aff_get_space(build->internal2input);
-	space = isl_space_range(space);
-	space2 = isl_set_get_space(build->domain);
-	if (isl_space_is_wrapping(space2))
-		space2 = isl_space_range(isl_space_unwrap(space2));
-	n2 = isl_space_dim(space2, isl_dim_set);
-	n = isl_space_dim(space, isl_dim_set);
-	if (n < n2)
-		isl_die(isl_ast_build_get_ctx(build), isl_error_internal,
-			"total input space dimension cannot be smaller "
-			"than dimension of innermost band",
-			space = isl_space_free(space));
-	space = isl_space_drop_dims(space, isl_dim_set, n - n2, n2);
-	space = isl_space_map_from_domain_and_range(space, space2);
-	space = isl_space_wrap(space);
-	space = isl_space_set_tuple_name(space, isl_dim_set, "isolate");
-	isolated = isl_union_set_extract_set(options, space);
-	isl_union_set_free(options);
-
+	isolated = isl_schedule_node_band_get_ast_isolate_option(build->node);
 	isolated = isl_set_flatten(isolated);
 	isolated = isl_set_preimage_multi_aff(isolated,
 				    isl_multi_aff_copy(build->internal2input));
diff --git a/polly/lib/External/isl/isl_coalesce.c b/polly/lib/External/isl/isl_coalesce.c
index 1d9ef14a760e..b7f2f90c5733 100644
--- a/polly/lib/External/isl/isl_coalesce.c
+++ b/polly/lib/External/isl/isl_coalesce.c
@@ -3,6 +3,7 @@
  * Copyright 2010      INRIA Saclay
  * Copyright 2012-2013 Ecole Normale Superieure
  * Copyright 2014      INRIA Rocquencourt
+ * Copyright 2016      Sven Verdoolaege
  *
  * Use of this software is governed by the MIT license
  *
@@ -15,6 +16,7 @@
  * B.P. 105 - 78153 Le Chesnay, France
  */
 
+#include <isl_ctx_private.h>
 #include "isl_map_private.h"
 #include <isl_seq.h>
 #include <isl/options.h>
@@ -23,6 +25,7 @@
 #include <isl_local_space_private.h>
 #include <isl_vec_private.h>
 #include <isl_aff_private.h>
+#include <isl_equalities.h>
 
 #define STATUS_ERROR		-1
 #define STATUS_REDUNDANT	 1
@@ -176,6 +179,36 @@ struct isl_coalesce_info {
 	int *ineq;
 };
 
+/* Are all non-redundant constraints of the basic map represented by "info"
+ * either valid or cut constraints with respect to the other basic map?
+ */
+static int all_valid_or_cut(struct isl_coalesce_info *info)
+{
+	int i;
+
+	for (i = 0; i < 2 * info->bmap->n_eq; ++i) {
+		if (info->eq[i] == STATUS_REDUNDANT)
+			continue;
+		if (info->eq[i] == STATUS_VALID)
+			continue;
+		if (info->eq[i] == STATUS_CUT)
+			continue;
+		return 0;
+	}
+
+	for (i = 0; i < info->bmap->n_ineq; ++i) {
+		if (info->ineq[i] == STATUS_REDUNDANT)
+			continue;
+		if (info->ineq[i] == STATUS_VALID)
+			continue;
+		if (info->ineq[i] == STATUS_CUT)
+			continue;
+		return 0;
+	}
+
+	return 1;
+}
+
 /* Compute the hash of the (apparent) affine hull of info->bmap (with
  * the existentially quantified variables removed) and store it
  * in info->hash.
@@ -356,8 +389,8 @@ static int number_of_constraints_increases(int i, int j,
  * is assumed to be the same, the actual definitions may be different.
  * We only copy the definition from one of the basic map if it is
  * the same as that of the other basic map.  Otherwise, we mark
- * the integer division as unknown and schedule for the basic map
- * to be simplified in an attempt to recover the integer division definition.
+ * the integer division as unknown and simplify the basic map
+ * in an attempt to recover the integer division definition.
  */
 static enum isl_change fuse(int i, int j, struct isl_coalesce_info *info,
 	__isl_keep isl_mat *extra, int detect_equalities, int check_number)
@@ -368,6 +401,7 @@ static enum isl_change fuse(int i, int j, struct isl_coalesce_info *info,
 	unsigned total = isl_basic_map_total_dim(info[i].bmap);
 	unsigned extra_rows = extra ? extra->n_row : 0;
 	unsigned n_eq, n_ineq;
+	int simplify = 0;
 
 	if (j < i)
 		return fuse(j, i, info, extra, detect_equalities, check_number);
@@ -391,7 +425,7 @@ static enum isl_change fuse(int i, int j, struct isl_coalesce_info *info,
 				1 + 1 + total);
 		} else {
 			isl_int_set_si(fused->div[l][0], 0);
-			info[i].simplify = 1;
+			simplify = 1;
 		}
 	}
 
@@ -405,7 +439,11 @@ static enum isl_change fuse(int i, int j, struct isl_coalesce_info *info,
 	if (detect_equalities)
 		fused = isl_basic_map_detect_inequality_pairs(fused, NULL);
 	fused = isl_basic_map_gauss(fused, NULL);
-	ISL_F_SET(fused, ISL_BASIC_MAP_FINAL);
+	if (simplify || info[j].simplify) {
+		fused = isl_basic_map_simplify(fused);
+		info[i].simplify = 0;
+	}
+	fused = isl_basic_map_finalize(fused);
 	if (ISL_F_ISSET(info[i].bmap, ISL_BASIC_MAP_RATIONAL) &&
 	    ISL_F_ISSET(info[j].bmap, ISL_BASIC_MAP_RATIONAL))
 		ISL_F_SET(fused, ISL_BASIC_MAP_RATIONAL);
@@ -421,7 +459,6 @@ static enum isl_change fuse(int i, int j, struct isl_coalesce_info *info,
 		return isl_change_none;
 	}
 
-	info[i].simplify |= info[j].simplify;
 	isl_basic_map_free(info[i].bmap);
 	info[i].bmap = fused;
 	isl_tab_free(info[i].tab);
@@ -698,14 +735,210 @@ static enum isl_change check_adj_ineq(int i, int j,
 	return isl_change_none;
 }
 
+/* Given an affine transformation matrix "T", does row "row" represent
+ * anything other than a unit vector (possibly shifted by a constant)
+ * that is not involved in any of the other rows?
+ *
+ * That is, if a constraint involves the variable corresponding to
+ * the row, then could its preimage by "T" have any coefficients
+ * that are different from those in the original constraint?
+ */
+static int not_unique_unit_row(__isl_keep isl_mat *T, int row)
+{
+	int i, j;
+	int len = T->n_col - 1;
+
+	i = isl_seq_first_non_zero(T->row[row] + 1, len);
+	if (i < 0)
+		return 1;
+	if (!isl_int_is_one(T->row[row][1 + i]) &&
+	    !isl_int_is_negone(T->row[row][1 + i]))
+		return 1;
+
+	j = isl_seq_first_non_zero(T->row[row] + 1 + i + 1, len - (i + 1));
+	if (j >= 0)
+		return 1;
+
+	for (j = 1; j < T->n_row; ++j) {
+		if (j == row)
+			continue;
+		if (!isl_int_is_zero(T->row[j][1 + i]))
+			return 1;
+	}
+
+	return 0;
+}
+
+/* Does inequality constraint "ineq" of "bmap" involve any of
+ * the variables marked in "affected"?
+ * "total" is the total number of variables, i.e., the number
+ * of entries in "affected".
+ */
+static int is_affected(__isl_keep isl_basic_map *bmap, int ineq, int *affected,
+	int total)
+{
+	int i;
+
+	for (i = 0; i < total; ++i) {
+		if (!affected[i])
+			continue;
+		if (!isl_int_is_zero(bmap->ineq[ineq][1 + i]))
+			return 1;
+	}
+
+	return 0;
+}
+
+/* Given the compressed version of inequality constraint "ineq"
+ * of info->bmap in "v", check if the constraint can be tightened,
+ * where the compression is based on an equality constraint valid
+ * for info->tab.
+ * If so, add the tightened version of the inequality constraint
+ * to info->tab.  "v" may be modified by this function.
+ *
+ * That is, if the compressed constraint is of the form
+ *
+ *	m f() + c >= 0
+ *
+ * with 0 < c < m, then it is equivalent to
+ *
+ *	f() >= 0
+ *
+ * This means that c can also be subtracted from the original,
+ * uncompressed constraint without affecting the integer points
+ * in info->tab.  Add this tightened constraint as an extra row
+ * to info->tab to make this information explicitly available.
+ */
+static __isl_give isl_vec *try_tightening(struct isl_coalesce_info *info,
+	int ineq, __isl_take isl_vec *v)
+{
+	isl_ctx *ctx;
+	int r;
+
+	if (!v)
+		return NULL;
+
+	ctx = isl_vec_get_ctx(v);
+	isl_seq_gcd(v->el + 1, v->size - 1, &ctx->normalize_gcd);
+	if (isl_int_is_zero(ctx->normalize_gcd) ||
+	    isl_int_is_one(ctx->normalize_gcd)) {
+		return v;
+	}
+
+	v = isl_vec_cow(v);
+	if (!v)
+		return NULL;
+
+	isl_int_fdiv_r(v->el[0], v->el[0], ctx->normalize_gcd);
+	if (isl_int_is_zero(v->el[0]))
+		return v;
+
+	if (isl_tab_extend_cons(info->tab, 1) < 0)
+		return isl_vec_free(v);
+
+	isl_int_sub(info->bmap->ineq[ineq][0],
+		    info->bmap->ineq[ineq][0], v->el[0]);
+	r = isl_tab_add_ineq(info->tab, info->bmap->ineq[ineq]);
+	isl_int_add(info->bmap->ineq[ineq][0],
+		    info->bmap->ineq[ineq][0], v->el[0]);
+
+	if (r < 0)
+		return isl_vec_free(v);
+
+	return v;
+}
+
+/* Tighten the constraints on the facet represented by info->tab.
+ * In particular, on input, info->tab represents the result
+ * of replacing constraint k of info->bmap, i.e., f_k >= 0,
+ * by the adjacent equality, i.e., f_k + 1 = 0.
+ *
+ * Compute a variable compression from the equality constraint f_k + 1 = 0
+ * and use it to tighten the other constraints of info->bmap,
+ * updating info->tab (and leaving info->bmap untouched).
+ * The compression handles essentially two cases, one where a variable
+ * is assigned a fixed value and can therefore be eliminated, and one
+ * where one variable is a shifted multiple of some other variable and
+ * can therefore be replaced by that multiple.
+ * Gaussian elimination would also work for the first case, but for
+ * the second case, the effectiveness would depend on the order
+ * of the variables.
+ * After compression, some of the constraints may have coefficients
+ * with a common divisor.  If this divisor does not divide the constant
+ * term, then the constraint can be tightened.
+ * The tightening is performed on the tableau info->tab by introducing
+ * extra (temporary) constraints.
+ *
+ * Only constraints that are possibly affected by the compression are
+ * considered.  In particular, if the constraint only involves variables
+ * that are directly mapped to a distinct set of other variables, then
+ * no common divisor can be introduced and no tightening can occur.
+ */
+static isl_stat tighten_on_relaxed_facet(struct isl_coalesce_info *info,
+	int k)
+{
+	unsigned total;
+	isl_ctx *ctx;
+	isl_vec *v = NULL;
+	isl_mat *T;
+	int i;
+	int *affected;
+
+	ctx = isl_basic_map_get_ctx(info->bmap);
+	total = isl_basic_map_total_dim(info->bmap);
+	isl_int_add_ui(info->bmap->ineq[k][0], info->bmap->ineq[k][0], 1);
+	T = isl_mat_sub_alloc6(ctx, info->bmap->ineq, k, 1, 0, 1 + total);
+	T = isl_mat_variable_compression(T, NULL);
+	isl_int_sub_ui(info->bmap->ineq[k][0], info->bmap->ineq[k][0], 1);
+	if (!T)
+		return isl_stat_error;
+	if (T->n_col == 0) {
+		isl_mat_free(T);
+		return isl_stat_ok;
+	}
+
+	affected = isl_alloc_array(ctx, int, total);
+	if (!affected)
+		goto error;
+
+	for (i = 0; i < total; ++i)
+		affected[i] = not_unique_unit_row(T, 1 + i);
+
+	for (i = 0; i < info->bmap->n_ineq; ++i) {
+		if (i == k)
+			continue;
+		if (!is_affected(info->bmap, i, affected, total))
+			continue;
+		v = isl_vec_alloc(ctx, 1 + total);
+		if (!v)
+			goto error;
+		isl_seq_cpy(v->el, info->bmap->ineq[i], 1 + total);
+		v = isl_vec_mat_product(v, isl_mat_copy(T));
+		v = try_tightening(info, i, v);
+		isl_vec_free(v);
+		if (!v)
+			goto error;
+	}
+
+	isl_mat_free(T);
+	free(affected);
+	return isl_stat_ok;
+error:
+	isl_mat_free(T);
+	free(affected);
+	return isl_stat_error;
+}
+
 /* Basic map "i" has an inequality "k" that is adjacent to some equality
  * of basic map "j".  All the other inequalities are valid for "j".
  * Check if basic map "j" forms an extension of basic map "i".
  *
  * In particular, we relax constraint "k", compute the corresponding
  * facet and check whether it is included in the other basic map.
- * If so, we know that relaxing the constraint extends the basic
- * map with exactly the other basic map (we already know that this
+ * Before testing for inclusion, the constraints on the facet
+ * are tightened to increase the chance of an inclusion being detected.
+ * If the facet is included, we know that relaxing the constraint extends
+ * the basic map with exactly the other basic map (we already know that this
  * other basic map is included in the extension, because there
  * were no "cut" inequalities in "i") and we can replace the
  * two basic maps by this extension.
@@ -738,6 +971,8 @@ static enum isl_change is_adj_eq_extension(int i, int j, int k,
 	snap2 = isl_tab_snap(info[i].tab);
 	if (isl_tab_select_facet(info[i].tab, n_eq + k) < 0)
 		return isl_change_error;
+	if (tighten_on_relaxed_facet(&info[i], k) < 0)
+		return isl_change_error;
 	super = contains(&info[j], info[i].tab);
 	if (super < 0)
 		return isl_change_error;
@@ -1141,16 +1376,14 @@ error:
 	return isl_change_error;
 }
 
-/* Given a pair of basic maps i and j such that j sticks out
- * of i at n cut constraints, each time by at most one,
- * try to compute wrapping constraints and replace the two
- * basic maps by a single basic map.
- * The other constraints of i are assumed to be valid for j.
- *
- * For each cut constraint t(x) >= 0 of i, we add the relaxed version
- * t(x) + 1 >= 0, along with wrapping constraints for all constraints
+/* Given a cut constraint t(x) >= 0 of basic map i, stored in row "w"
+ * of wrap.mat, replace it by its relaxed version t(x) + 1 >= 0, and
+ * add wrapping constraints to wrap.mat for all constraints
  * of basic map j that bound the part of basic map j that sticks out
  * of the cut constraint.
+ * "set_i" is the underlying set of basic map i.
+ * If any wrapping fails, then wraps->mat.n_row is reset to zero.
+ *
  * In particular, we first intersect basic map j with t(x) + 1 = 0.
  * If the result is empty, then t(x) >= 0 was actually a valid constraint
  * (with respect to the integer points), so we add t(x) >= 0 instead.
@@ -1163,12 +1396,106 @@ error:
  * therefore be more relaxed compared to the original constraint.
  * Since the original constraint is valid for basic map j, so is
  * the wrapped constraint.
+ */
+static isl_stat wrap_in_facet(struct isl_wraps *wraps, int w,
+	struct isl_coalesce_info *info_j, __isl_keep isl_set *set_i,
+	struct isl_tab_undo *snap)
+{
+	isl_int_add_ui(wraps->mat->row[w][0], wraps->mat->row[w][0], 1);
+	if (isl_tab_add_eq(info_j->tab, wraps->mat->row[w]) < 0)
+		return isl_stat_error;
+	if (isl_tab_detect_redundant(info_j->tab) < 0)
+		return isl_stat_error;
+
+	if (info_j->tab->empty)
+		isl_int_sub_ui(wraps->mat->row[w][0], wraps->mat->row[w][0], 1);
+	else if (add_wraps(wraps, info_j, wraps->mat->row[w], set_i) < 0)
+		return isl_stat_error;
+
+	if (isl_tab_rollback(info_j->tab, snap) < 0)
+		return isl_stat_error;
+
+	return isl_stat_ok;
+}
+
+/* Given a pair of basic maps i and j such that j sticks out
+ * of i at n cut constraints, each time by at most one,
+ * try to compute wrapping constraints and replace the two
+ * basic maps by a single basic map.
+ * The other constraints of i are assumed to be valid for j.
+ * "set_i" is the underlying set of basic map i.
+ * "wraps" has been initialized to be of the right size.
+ *
+ * For each cut constraint t(x) >= 0 of i, we add the relaxed version
+ * t(x) + 1 >= 0, along with wrapping constraints for all constraints
+ * of basic map j that bound the part of basic map j that sticks out
+ * of the cut constraint.
  *
  * If any wrapping fails, i.e., if we cannot wrap to touch
  * the union, then we give up.
  * Otherwise, the pair of basic maps is replaced by their union.
  */
-static enum isl_change wrap_in_facets(int i, int j, int *cuts, int n,
+static enum isl_change try_wrap_in_facets(int i, int j,
+	struct isl_coalesce_info *info, struct isl_wraps *wraps,
+	__isl_keep isl_set *set_i)
+{
+	int k, l, w;
+	unsigned total;
+	struct isl_tab_undo *snap;
+
+	total = isl_basic_map_total_dim(info[i].bmap);
+
+	snap = isl_tab_snap(info[j].tab);
+
+	wraps->mat->n_row = 0;
+
+	for (k = 0; k < info[i].bmap->n_eq; ++k) {
+		for (l = 0; l < 2; ++l) {
+			if (info[i].eq[2 * k + l] != STATUS_CUT)
+				continue;
+			w = wraps->mat->n_row++;
+			if (l == 0)
+				isl_seq_neg(wraps->mat->row[w],
+					    info[i].bmap->eq[k], 1 + total);
+			else
+				isl_seq_cpy(wraps->mat->row[w],
+					    info[i].bmap->eq[k], 1 + total);
+			if (wrap_in_facet(wraps, w, &info[j], set_i, snap) < 0)
+				return isl_change_error;
+
+			if (!wraps->mat->n_row)
+				return isl_change_none;
+		}
+	}
+
+	for (k = 0; k < info[i].bmap->n_ineq; ++k) {
+		if (info[i].ineq[k] != STATUS_CUT)
+			continue;
+		w = wraps->mat->n_row++;
+		isl_seq_cpy(wraps->mat->row[w],
+			    info[i].bmap->ineq[k], 1 + total);
+		if (wrap_in_facet(wraps, w, &info[j], set_i, snap) < 0)
+			return isl_change_error;
+
+		if (!wraps->mat->n_row)
+			return isl_change_none;
+	}
+
+	return fuse(i, j, info, wraps->mat, 0, 1);
+}
+
+/* Given a pair of basic maps i and j such that j sticks out
+ * of i at n cut constraints, each time by at most one,
+ * try to compute wrapping constraints and replace the two
+ * basic maps by a single basic map.
+ * The other constraints of i are assumed to be valid for j.
+ *
+ * The core computation is performed by try_wrap_in_facets.
+ * This function simply extracts an underlying set representation
+ * of basic map i and initializes the data structure for keeping
+ * track of wrapping constraints.
+ */
+static enum isl_change wrap_in_facets(int i, int j, int n,
 	struct isl_coalesce_info *info)
 {
 	enum isl_change change = isl_change_none;
@@ -1178,8 +1505,6 @@ static enum isl_change wrap_in_facets(int i, int j, int *cuts, int n,
 	isl_set *set_i = NULL;
 	unsigned total = isl_basic_map_total_dim(info[i].bmap);
 	int max_wrap;
-	int k, w;
-	struct isl_tab_undo *snap;
 
 	if (isl_tab_extend_cons(info[j].tab, 1) < 0)
 		return isl_change_error;
@@ -1194,36 +1519,7 @@ static enum isl_change wrap_in_facets(int i, int j, int *cuts, int n,
 	if (!set_i || !wraps.mat)
 		goto error;
 
-	snap = isl_tab_snap(info[j].tab);
-
-	wraps.mat->n_row = 0;
-
-	for (k = 0; k < n; ++k) {
-		w = wraps.mat->n_row++;
-		isl_seq_cpy(wraps.mat->row[w],
-			    info[i].bmap->ineq[cuts[k]], 1 + total);
-		isl_int_add_ui(wraps.mat->row[w][0], wraps.mat->row[w][0], 1);
-		if (isl_tab_add_eq(info[j].tab, wraps.mat->row[w]) < 0)
-			goto error;
-		if (isl_tab_detect_redundant(info[j].tab) < 0)
-			goto error;
-
-		if (info[j].tab->empty)
-			isl_int_sub_ui(wraps.mat->row[w][0],
-					wraps.mat->row[w][0], 1);
-		else if (add_wraps(&wraps, &info[j],
-				    wraps.mat->row[w], set_i) < 0)
-			goto error;
-
-		if (isl_tab_rollback(info[j].tab, snap) < 0)
-			goto error;
-
-		if (!wraps.mat->n_row)
-			break;
-	}
-
-	if (k == n)
-		change = fuse(i, j, info, wraps.mat, 0, 1);
+	change = try_wrap_in_facets(i, j, info, &wraps, set_i);
 
 	wraps_free(&wraps);
 	isl_set_free(set_i);
@@ -1235,8 +1531,22 @@ error:
 	return isl_change_error;
 }
 
-/* Given two basic sets i and j such that i has no cut equalities,
- * check if relaxing all the cut inequalities of i by one turns
+/* Return the effect of inequality "ineq" on the tableau "tab",
+ * after relaxing the constant term of "ineq" by one.
+ */
+static enum isl_ineq_type type_of_relaxed(struct isl_tab *tab, isl_int *ineq)
+{
+	enum isl_ineq_type type;
+
+	isl_int_add_ui(ineq[0], ineq[0], 1);
+	type = isl_tab_ineq_type(tab, ineq);
+	isl_int_sub_ui(ineq[0], ineq[0], 1);
+
+	return type;
+}
+
+/* Given two basic sets i and j,
+ * check if relaxing all the cut constraints of i by one turns
  * them into valid constraint for j and check if we can wrap in
  * the bits that are sticking out.
  * If so, replace the pair by their union.
@@ -1297,56 +1607,59 @@ error:
 static enum isl_change can_wrap_in_set(int i, int j,
 	struct isl_coalesce_info *info)
 {
-	enum isl_change change = isl_change_none;
-	int k, m;
+	int k, l;
 	int n;
-	int *cuts = NULL;
-	isl_ctx *ctx;
+	unsigned total;
 
 	if (ISL_F_ISSET(info[i].bmap, ISL_BASIC_MAP_RATIONAL) ||
 	    ISL_F_ISSET(info[j].bmap, ISL_BASIC_MAP_RATIONAL))
 		return isl_change_none;
 
-	n = count(info[i].ineq, info[i].bmap->n_ineq, STATUS_CUT);
+	n = count(info[i].eq, 2 * info[i].bmap->n_eq, STATUS_CUT);
+	n += count(info[i].ineq, info[i].bmap->n_ineq, STATUS_CUT);
 	if (n == 0)
 		return isl_change_none;
 
-	ctx = isl_basic_map_get_ctx(info[i].bmap);
-	cuts = isl_alloc_array(ctx, int, n);
-	if (!cuts)
-		return isl_change_error;
+	total = isl_basic_map_total_dim(info[i].bmap);
+	for (k = 0; k < info[i].bmap->n_eq; ++k) {
+		for (l = 0; l < 2; ++l) {
+			enum isl_ineq_type type;
 
-	for (k = 0, m = 0; m < n; ++k) {
+			if (info[i].eq[2 * k + l] != STATUS_CUT)
+				continue;
+
+			if (l == 0)
+				isl_seq_neg(info[i].bmap->eq[k],
+					    info[i].bmap->eq[k], 1 + total);
+			type = type_of_relaxed(info[j].tab,
+					    info[i].bmap->eq[k]);
+			if (l == 0)
+				isl_seq_neg(info[i].bmap->eq[k],
+					    info[i].bmap->eq[k], 1 + total);
+			if (type == isl_ineq_error)
+				return isl_change_error;
+			if (type != isl_ineq_redundant)
+				return isl_change_none;
+		}
+	}
+
+	for (k = 0; k < info[i].bmap->n_ineq; ++k) {
 		enum isl_ineq_type type;
 
 		if (info[i].ineq[k] != STATUS_CUT)
 			continue;
 
-		isl_int_add_ui(info[i].bmap->ineq[k][0],
-				info[i].bmap->ineq[k][0], 1);
-		type = isl_tab_ineq_type(info[j].tab, info[i].bmap->ineq[k]);
-		isl_int_sub_ui(info[i].bmap->ineq[k][0],
-				info[i].bmap->ineq[k][0], 1);
+		type = type_of_relaxed(info[j].tab, info[i].bmap->ineq[k]);
 		if (type == isl_ineq_error)
-			goto error;
+			return isl_change_error;
 		if (type != isl_ineq_redundant)
-			break;
-		cuts[m] = k;
-		++m;
+			return isl_change_none;
 	}
 
-	if (m == n)
-		change = wrap_in_facets(i, j, cuts, n, info);
-
-	free(cuts);
-
-	return change;
-error:
-	free(cuts);
-	return isl_change_error;
+	return wrap_in_facets(i, j, n, info);
 }
 
-/* Check if either i or j has only cut inequalities that can
+/* Check if either i or j has only cut constraints that can
  * be used to wrap in (a facet of) the other basic set.
  * if so, replace the pair by their union.
  */
@@ -1354,13 +1667,11 @@ static enum isl_change check_wrap(int i, int j, struct isl_coalesce_info *info)
 {
 	enum isl_change change = isl_change_none;
 
-	if (!any(info[i].eq, 2 * info[i].bmap->n_eq, STATUS_CUT))
-		change = can_wrap_in_set(i, j, info);
+	change = can_wrap_in_set(i, j, info);
 	if (change != isl_change_none)
 		return change;
 
-	if (!any(info[j].eq, 2 * info[j].bmap->n_eq, STATUS_CUT))
-		change = can_wrap_in_set(j, i, info);
+	change = can_wrap_in_set(j, i, info);
 	return change;
 }
 
@@ -1368,6 +1679,10 @@ static enum isl_change check_wrap(int i, int j, struct isl_coalesce_info *info)
  * to inequality.  Make sure that only one of the basic maps has
  * such an equality and that the other basic map has exactly one
  * inequality adjacent to an equality.
+ * If the other basic map does not have such an inequality, then
+ * check if all its constraints are either valid or cut constraints
+ * and, if so, try wrapping in the first map into the second.
+ *
  * We call the basic map that has the inequality "i" and the basic
  * map that has the equality "j".
  * If "i" has any "cut" (in)equality, then relaxing the inequality
@@ -1392,11 +1707,15 @@ static enum isl_change check_adj_eq(int i, int j,
 
 	/* j has an equality adjacent to an inequality in i */
 
+	if (count(info[i].ineq, info[i].bmap->n_ineq, STATUS_ADJ_EQ) != 1) {
+		if (all_valid_or_cut(&info[i]))
+			return can_wrap_in_set(i, j, info);
+		return isl_change_none;
+	}
 	if (any(info[i].eq, 2 * info[i].bmap->n_eq, STATUS_CUT))
 		return isl_change_none;
 	any_cut = any(info[i].ineq, info[i].bmap->n_ineq, STATUS_CUT);
-	if (count(info[i].ineq, info[i].bmap->n_ineq, STATUS_ADJ_EQ) != 1 ||
-	    any(info[j].ineq, info[j].bmap->n_ineq, STATUS_ADJ_EQ) ||
+	if (any(info[j].ineq, info[j].bmap->n_ineq, STATUS_ADJ_EQ) ||
 	    any(info[i].ineq, info[i].bmap->n_ineq, STATUS_ADJ_INEQ) ||
 	    any(info[j].ineq, info[j].bmap->n_ineq, STATUS_ADJ_INEQ))
 		/* ADJ EQ TOO MANY */
@@ -1507,12 +1826,57 @@ unbounded:
 	return change;
 }
 
+/* Initialize the "eq" and "ineq" fields of "info".
+ */
+static void init_status(struct isl_coalesce_info *info)
+{
+	info->eq = info->ineq = NULL;
+}
+
+/* Set info->eq to the positions of the equalities of info->bmap
+ * with respect to the basic map represented by "tab".
+ * If info->eq has already been computed, then do not compute it again.
+ */
+static void set_eq_status_in(struct isl_coalesce_info *info,
+	struct isl_tab *tab)
+{
+	if (info->eq)
+		return;
+	info->eq = eq_status_in(info->bmap, tab);
+}
+
+/* Set info->ineq to the positions of the inequalities of info->bmap
+ * with respect to the basic map represented by "tab".
+ * If info->ineq has already been computed, then do not compute it again.
+ */
+static void set_ineq_status_in(struct isl_coalesce_info *info,
+	struct isl_tab *tab)
+{
+	if (info->ineq)
+		return;
+	info->ineq = ineq_status_in(info->bmap, info->tab, tab);
+}
+
+/* Free the memory allocated by the "eq" and "ineq" fields of "info".
+ * This function assumes that init_status has been called on "info" first,
+ * after which the "eq" and "ineq" fields may or may not have been
+ * assigned a newly allocated array.
+ */
+static void clear_status(struct isl_coalesce_info *info)
+{
+	free(info->eq);
+	free(info->ineq);
+}
+
 /* Check if the union of the given pair of basic maps
  * can be represented by a single basic map.
  * If so, replace the pair by the single basic map and return
  * isl_change_drop_first, isl_change_drop_second or isl_change_fuse.
  * Otherwise, return isl_change_none.
  * The two basic maps are assumed to live in the same local space.
+ * The "eq" and "ineq" fields of info[i] and info[j] are assumed
+ * to have been initialized by the caller, either to NULL or
+ * to valid information.
  *
  * We first check the effect of each constraint of one basic map
  * on the other basic map.
@@ -1590,15 +1954,12 @@ unbounded:
  * corresponding to the basic maps.  When the basic maps are dropped
  * or combined, the tableaus are modified accordingly.
  */
-static enum isl_change coalesce_local_pair(int i, int j,
+static enum isl_change coalesce_local_pair_reuse(int i, int j,
 	struct isl_coalesce_info *info)
 {
 	enum isl_change change = isl_change_none;
 
-	info[i].eq = info[i].ineq = NULL;
-	info[j].eq = info[j].ineq = NULL;
-
-	info[i].eq = eq_status_in(info[i].bmap, info[j].tab);
+	set_eq_status_in(&info[i], info[j].tab);
 	if (info[i].bmap->n_eq && !info[i].eq)
 		goto error;
 	if (any(info[i].eq, 2 * info[i].bmap->n_eq, STATUS_ERROR))
@@ -1606,7 +1967,7 @@ static enum isl_change coalesce_local_pair(int i, int j,
 	if (any(info[i].eq, 2 * info[i].bmap->n_eq, STATUS_SEPARATE))
 		goto done;
 
-	info[j].eq = eq_status_in(info[j].bmap, info[i].tab);
+	set_eq_status_in(&info[j], info[i].tab);
 	if (info[j].bmap->n_eq && !info[j].eq)
 		goto error;
 	if (any(info[j].eq, 2 * info[j].bmap->n_eq, STATUS_ERROR))
@@ -1614,7 +1975,7 @@ static enum isl_change coalesce_local_pair(int i, int j,
 	if (any(info[j].eq, 2 * info[j].bmap->n_eq, STATUS_SEPARATE))
 		goto done;
 
-	info[i].ineq = ineq_status_in(info[i].bmap, info[i].tab, info[j].tab);
+	set_ineq_status_in(&info[i], info[j].tab);
 	if (info[i].bmap->n_ineq && !info[i].ineq)
 		goto error;
 	if (any(info[i].ineq, info[i].bmap->n_ineq, STATUS_ERROR))
@@ -1622,7 +1983,7 @@ static enum isl_change coalesce_local_pair(int i, int j,
 	if (any(info[i].ineq, info[i].bmap->n_ineq, STATUS_SEPARATE))
 		goto done;
 
-	info[j].ineq = ineq_status_in(info[j].bmap, info[j].tab, info[i].tab);
+	set_ineq_status_in(&info[j], info[i].tab);
 	if (info[j].bmap->n_ineq && !info[j].ineq)
 		goto error;
 	if (any(info[j].ineq, info[j].bmap->n_ineq, STATUS_ERROR))
@@ -1661,19 +2022,30 @@ static enum isl_change coalesce_local_pair(int i, int j,
 	}
 
 done:
-	free(info[i].eq);
-	free(info[j].eq);
-	free(info[i].ineq);
-	free(info[j].ineq);
+	clear_status(&info[i]);
+	clear_status(&info[j]);
 	return change;
 error:
-	free(info[i].eq);
-	free(info[j].eq);
-	free(info[i].ineq);
-	free(info[j].ineq);
+	clear_status(&info[i]);
+	clear_status(&info[j]);
 	return isl_change_error;
 }
 
+/* Check if the union of the given pair of basic maps
+ * can be represented by a single basic map.
+ * If so, replace the pair by the single basic map and return
+ * isl_change_drop_first, isl_change_drop_second or isl_change_fuse.
+ * Otherwise, return isl_change_none.
+ * The two basic maps are assumed to live in the same local space.
+ */
+static enum isl_change coalesce_local_pair(int i, int j,
+	struct isl_coalesce_info *info)
+{
+	init_status(&info[i]);
+	init_status(&info[j]);
+	return coalesce_local_pair_reuse(i, j, info);
+}
+
 /* Shift the integer division at position "div" of the basic map
  * represented by "info" by "shift".
  *
@@ -1805,75 +2177,233 @@ static int same_divs(__isl_keep isl_basic_map *bmap1,
 	return 1;
 }
 
-/* Does "bmap" contain the basic map represented by the tableau "tab"
- * after expanding the divs of "bmap" to match those of "tab"?
+/* Expand info->tab in the same way info->bmap was expanded in
+ * isl_basic_map_expand_divs using the expansion "exp" and
+ * update info->ineq with respect to the redundant constraints
+ * in the resulting tableau.
+ * In particular, introduce extra variables corresponding
+ * to the extra integer divisions and add the div constraints
+ * that were added to info->bmap after info->tab was created
+ * from the original info->bmap.
+ * info->ineq was computed without a tableau and therefore
+ * does not take into account the redundant constraints
+ * in the tableau.  Mark them here.
+ */
+static isl_stat expand_tab(struct isl_coalesce_info *info, int *exp)
+{
+	unsigned total, pos, n_div;
+	int extra_var;
+	int i, n, j, n_ineq;
+	unsigned n_eq;
+
+	total = isl_basic_map_dim(info->bmap, isl_dim_all);
+	n_div = isl_basic_map_dim(info->bmap, isl_dim_div);
+	pos = total - n_div;
+	extra_var = total - info->tab->n_var;
+	n = n_div - extra_var;
+
+	if (isl_tab_extend_vars(info->tab, extra_var) < 0)
+		return isl_stat_error;
+	if (isl_tab_extend_cons(info->tab, 2 * extra_var) < 0)
+		return isl_stat_error;
+
+	i = 0;
+	for (j = 0; j < n_div; ++j) {
+		if (i < n && exp[i] == j) {
+			++i;
+			continue;
+		}
+		if (isl_tab_insert_var(info->tab, pos + j) < 0)
+			return isl_stat_error;
+	}
+
+	n_ineq = info->tab->n_con - info->tab->n_eq;
+	for (i = n_ineq; i < info->bmap->n_ineq; ++i)
+		if (isl_tab_add_ineq(info->tab, info->bmap->ineq[i]) < 0)
+			return isl_stat_error;
+
+	n_eq = info->bmap->n_eq;
+	for (i = 0; i < info->bmap->n_ineq; ++i) {
+		if (isl_tab_is_redundant(info->tab, n_eq + i))
+			info->ineq[i] = STATUS_REDUNDANT;
+	}
+
+	return isl_stat_ok;
+}
+
+/* Check if the union of the basic maps represented by info[i] and info[j]
+ * can be represented by a single basic map,
+ * after expanding the divs of info[i] to match those of info[j].
+ * If so, replace the pair by the single basic map and return
+ * isl_change_drop_first, isl_change_drop_second or isl_change_fuse.
+ * Otherwise, return isl_change_none.
+ *
+ * The caller has already checked for info[j] being a subset of info[i].
+ * If some of the divs of info[j] are unknown, then the expanded info[i]
+ * will not have the corresponding div constraints.  The other patterns
+ * therefore cannot apply.  Skip the computation in this case.
+ *
  * The expansion is performed using the divs "div" and expansion "exp"
  * computed by the caller.
- * Then we check if all constraints of the expanded "bmap" are valid for "tab".
+ * info[i].bmap has already been expanded and the result is passed in
+ * as "bmap".
+ * The "eq" and "ineq" fields of info[i] reflect the status of
+ * the constraints of the expanded "bmap" with respect to info[j].tab.
+ * However, inequality constraints that are redundant in info[i].tab
+ * have not yet been marked as such because no tableau was available.
+ *
+ * Replace info[i].bmap by "bmap" and expand info[i].tab as well,
+ * updating info[i].ineq with respect to the redundant constraints.
+ * Then try and coalesce the expanded info[i] with info[j],
+ * reusing the information in info[i].eq and info[i].ineq.
+ * If this does not result in any coalescing or if it results in info[j]
+ * getting dropped (which should not happen in practice, since the case
+ * of info[j] being a subset of info[i] has already been checked by
+ * the caller), then revert info[i] to its original state.
  */
-static int contains_with_expanded_divs(__isl_keep isl_basic_map *bmap,
-	struct isl_tab *tab, __isl_keep isl_mat *div, int *exp)
+static enum isl_change coalesce_expand_tab_divs(__isl_take isl_basic_map *bmap,
+	int i, int j, struct isl_coalesce_info *info, __isl_keep isl_mat *div,
+	int *exp)
 {
-	int superset = 0;
-	int *eq_i = NULL;
-	int *ineq_i = NULL;
+	isl_bool known;
+	isl_basic_map *bmap_i;
+	struct isl_tab_undo *snap;
+	enum isl_change change = isl_change_none;
 
+	known = isl_basic_map_divs_known(info[j].bmap);
+	if (known < 0 || !known) {
+		clear_status(&info[i]);
+		isl_basic_map_free(bmap);
+		return known < 0 ? isl_change_error : isl_change_none;
+	}
+
+	bmap_i = info[i].bmap;
+	info[i].bmap = isl_basic_map_copy(bmap);
+	snap = isl_tab_snap(info[i].tab);
+	if (!info[i].bmap || expand_tab(&info[i], exp) < 0)
+		change = isl_change_error;
+
+	init_status(&info[j]);
+	if (change == isl_change_none)
+		change = coalesce_local_pair_reuse(i, j, info);
+	else
+		clear_status(&info[i]);
+	if (change != isl_change_none && change != isl_change_drop_second) {
+		isl_basic_map_free(bmap_i);
+	} else {
+		isl_basic_map_free(info[i].bmap);
+		info[i].bmap = bmap_i;
+
+		if (isl_tab_rollback(info[i].tab, snap) < 0)
+			change = isl_change_error;
+	}
+
+	isl_basic_map_free(bmap);
+	return change;
+}
+
+/* Check if the union of "bmap" and the basic map represented by info[j]
+ * can be represented by a single basic map,
+ * after expanding the divs of "bmap" to match those of info[j].
+ * If so, replace the pair by the single basic map and return
+ * isl_change_drop_first, isl_change_drop_second or isl_change_fuse.
+ * Otherwise, return isl_change_none.
+ *
+ * In particular, check if the expanded "bmap" contains the basic map
+ * represented by the tableau info[j].tab.
+ * The expansion is performed using the divs "div" and expansion "exp"
+ * computed by the caller.
+ * Then we check if all constraints of the expanded "bmap" are valid for
+ * info[j].tab.
+ *
+ * If "i" is not equal to -1, then "bmap" is equal to info[i].bmap.
+ * In this case, the positions of the constraints of info[i].bmap
+ * with respect to the basic map represented by info[j] are stored
+ * in info[i].
+ *
+ * If the expanded "bmap" does not contain the basic map
+ * represented by the tableau info[j].tab and if "i" is not -1,
+ * i.e., if the original "bmap" is info[i].bmap, then expand info[i].tab
+ * as well and check if that results in coalescing.
+ */
+static enum isl_change coalesce_with_expanded_divs(
+	__isl_keep isl_basic_map *bmap, int i, int j,
+	struct isl_coalesce_info *info, __isl_keep isl_mat *div, int *exp)
+{
+	enum isl_change change = isl_change_none;
+	struct isl_coalesce_info info_local, *info_i;
+
+	info_i = i >= 0 ? &info[i] : &info_local;
+	init_status(info_i);
 	bmap = isl_basic_map_copy(bmap);
 	bmap = isl_basic_map_expand_divs(bmap, isl_mat_copy(div), exp);
 
 	if (!bmap)
 		goto error;
 
-	eq_i = eq_status_in(bmap, tab);
-	if (bmap->n_eq && !eq_i)
+	info_i->eq = eq_status_in(bmap, info[j].tab);
+	if (bmap->n_eq && !info_i->eq)
 		goto error;
-	if (any(eq_i, 2 * bmap->n_eq, STATUS_ERROR))
+	if (any(info_i->eq, 2 * bmap->n_eq, STATUS_ERROR))
 		goto error;
-	if (any(eq_i, 2 * bmap->n_eq, STATUS_SEPARATE))
+	if (any(info_i->eq, 2 * bmap->n_eq, STATUS_SEPARATE))
 		goto done;
 
-	ineq_i = ineq_status_in(bmap, NULL, tab);
-	if (bmap->n_ineq && !ineq_i)
+	info_i->ineq = ineq_status_in(bmap, NULL, info[j].tab);
+	if (bmap->n_ineq && !info_i->ineq)
 		goto error;
-	if (any(ineq_i, bmap->n_ineq, STATUS_ERROR))
+	if (any(info_i->ineq, bmap->n_ineq, STATUS_ERROR))
 		goto error;
-	if (any(ineq_i, bmap->n_ineq, STATUS_SEPARATE))
+	if (any(info_i->ineq, bmap->n_ineq, STATUS_SEPARATE))
 		goto done;
 
-	if (all(eq_i, 2 * bmap->n_eq, STATUS_VALID) &&
-	    all(ineq_i, bmap->n_ineq, STATUS_VALID))
-		superset = 1;
+	if (all(info_i->eq, 2 * bmap->n_eq, STATUS_VALID) &&
+	    all(info_i->ineq, bmap->n_ineq, STATUS_VALID)) {
+		drop(&info[j]);
+		change = isl_change_drop_second;
+	}
+
+	if (change == isl_change_none && i != -1)
+		return coalesce_expand_tab_divs(bmap, i, j, info, div, exp);
 
 done:
 	isl_basic_map_free(bmap);
-	free(eq_i);
-	free(ineq_i);
-	return superset;
+	clear_status(info_i);
+	return change;
 error:
 	isl_basic_map_free(bmap);
-	free(eq_i);
-	free(ineq_i);
-	return -1;
+	clear_status(info_i);
+	return isl_change_error;
 }
 
-/* Does "bmap_i" contain the basic map represented by "info_j"
- * after aligning the divs of "bmap_i" to those of "info_j".
+/* Check if the union of "bmap_i" and the basic map represented by info[j]
+ * can be represented by a single basic map,
+ * after aligning the divs of "bmap_i" to match those of info[j].
+ * If so, replace the pair by the single basic map and return
+ * isl_change_drop_first, isl_change_drop_second or isl_change_fuse.
+ * Otherwise, return isl_change_none.
+ *
+ * In particular, check if "bmap_i" contains the basic map represented by
+ * info[j] after aligning the divs of "bmap_i" to those of info[j].
  * Note that this can only succeed if the number of divs of "bmap_i"
- * is smaller than (or equal to) the number of divs of "info_j".
+ * is smaller than (or equal to) the number of divs of info[j].
  *
  * We first check if the divs of "bmap_i" are all known and form a subset
- * of those of "bmap_j".  If so, we pass control over to
- * contains_with_expanded_divs.
+ * of those of info[j].bmap.  If so, we pass control over to
+ * coalesce_with_expanded_divs.
+ *
+ * If "i" is not equal to -1, then "bmap" is equal to info[i].bmap.
  */
-static int contains_after_aligning_divs(__isl_keep isl_basic_map *bmap_i,
-	struct isl_coalesce_info *info_j)
+static enum isl_change coalesce_after_aligning_divs(
+	__isl_keep isl_basic_map *bmap_i, int i, int j,
+	struct isl_coalesce_info *info)
 {
 	int known;
 	isl_mat *div_i, *div_j, *div;
 	int *exp1 = NULL;
 	int *exp2 = NULL;
 	isl_ctx *ctx;
-	int subset;
+	enum isl_change change;
 
 	known = isl_basic_map_divs_known(bmap_i);
 	if (known < 0 || !known)
@@ -1882,7 +2412,7 @@ static int contains_after_aligning_divs(__isl_keep isl_basic_map *bmap_i,
 	ctx = isl_basic_map_get_ctx(bmap_i);
 
 	div_i = isl_basic_map_get_divs(bmap_i);
-	div_j = isl_basic_map_get_divs(info_j->bmap);
+	div_j = isl_basic_map_get_divs(info[j].bmap);
 
 	if (!div_i || !div_j)
 		goto error;
@@ -1897,10 +2427,10 @@ static int contains_after_aligning_divs(__isl_keep isl_basic_map *bmap_i,
 		goto error;
 
 	if (div->n_row == div_j->n_row)
-		subset = contains_with_expanded_divs(bmap_i,
-							info_j->tab, div, exp1);
+		change = coalesce_with_expanded_divs(bmap_i,
+							i, j, info, div, exp1);
 	else
-		subset = 0;
+		change = isl_change_none;
 
 	isl_mat_free(div);
 
@@ -1910,43 +2440,18 @@ static int contains_after_aligning_divs(__isl_keep isl_basic_map *bmap_i,
 	free(exp2);
 	free(exp1);
 
-	return subset;
+	return change;
 error:
 	isl_mat_free(div_i);
 	isl_mat_free(div_j);
 	free(exp1);
 	free(exp2);
-	return -1;
-}
-
-/* Check if the basic map "j" is a subset of basic map "i",
- * if "i" has fewer divs that "j".
- * If so, remove basic map "j".
- *
- * If the two basic maps have the same number of divs, then
- * they must necessarily be different.  Otherwise, we would have
- * called coalesce_local_pair.  We therefore don't try anything
- * in this case.
- */
-static int coalesced_subset(int i, int j, struct isl_coalesce_info *info)
-{
-	int superset;
-
-	if (info[i].bmap->n_div >= info[j].bmap->n_div)
-		return 0;
-
-	superset = contains_after_aligning_divs(info[i].bmap, &info[j]);
-	if (superset < 0)
-		return -1;
-	if (superset)
-		drop(&info[j]);
-
-	return superset;
+	return isl_change_error;
 }
 
 /* Check if basic map "j" is a subset of basic map "i" after
  * exploiting the extra equalities of "j" to simplify the divs of "i".
- * If so, remove basic map "j".
+ * If so, remove basic map "j" and return isl_change_drop_second.
  *
  * If "j" does not have any equalities or if they are the same
  * as those of "i", then we cannot exploit them to simplify the divs.
@@ -1961,16 +2466,17 @@ static int coalesced_subset(int i, int j, struct isl_coalesce_info *info)
  * "i" still has more divs than "j", then there is no way we can
  * align the divs of "i" to those of "j".
  */
-static int coalesced_subset_with_equalities(int i, int j,
+static enum isl_change coalesce_subset_with_equalities(int i, int j,
 	struct isl_coalesce_info *info)
 {
 	isl_basic_map *hull_i, *hull_j, *bmap_i;
-	int equal, empty, subset;
+	int equal, empty;
+	enum isl_change change;
 
 	if (info[j].bmap->n_eq == 0)
-		return 0;
+		return isl_change_none;
 	if (info[i].bmap->n_div == 0)
-		return 0;
+		return isl_change_none;
 
 	hull_i = isl_basic_map_copy(info[i].bmap);
 	hull_i = isl_basic_map_plain_affine_hull(hull_i);
@@ -1984,33 +2490,35 @@ static int coalesced_subset_with_equalities(int i, int j,
 
 	if (equal < 0 || equal || empty < 0 || empty) {
 		isl_basic_map_free(hull_j);
-		return equal < 0 || empty < 0 ? -1 : 0;
+		if (equal < 0 || empty < 0)
+			return isl_change_error;
+		return isl_change_none;
 	}
 
 	bmap_i = isl_basic_map_copy(info[i].bmap);
 	bmap_i = isl_basic_map_intersect(bmap_i, hull_j);
 	if (!bmap_i)
-		return -1;
+		return isl_change_error;
 
 	if (bmap_i->n_div > info[j].bmap->n_div) {
 		isl_basic_map_free(bmap_i);
-		return 0;
+		return isl_change_none;
 	}
 
-	subset = contains_after_aligning_divs(bmap_i, &info[j]);
+	change = coalesce_after_aligning_divs(bmap_i, -1, j, info);
 
 	isl_basic_map_free(bmap_i);
 
-	if (subset < 0)
-		return -1;
-	if (subset)
-		drop(&info[j]);
-
-	return subset;
+	return change;
 }
 
-/* Check if one of the basic maps is a subset of the other and, if so,
- * drop the subset.
+/* Check if the union of and the basic maps represented by info[i] and info[j]
+ * can be represented by a single basic map, by aligning or equating
+ * their integer divisions.
+ * If so, replace the pair by the single basic map and return
+ * isl_change_drop_first, isl_change_drop_second or isl_change_fuse.
+ * Otherwise, return isl_change_none.
+ *
  * Note that we only perform any test if the number of divs is different
  * in the two basic maps.  In case the number of divs is the same,
  * we have already established that the divs are different
@@ -2019,26 +2527,28 @@ static int coalesced_subset_with_equalities(int i, int j,
  * the number of divs of basic map j, then we check if j is a subset of i
  * and vice versa.
  */
-static enum isl_change check_coalesce_subset(int i, int j,
+static enum isl_change coalesce_divs(int i, int j,
 	struct isl_coalesce_info *info)
 {
-	int changed;
+	enum isl_change change = isl_change_none;
 
-	changed = coalesced_subset(i, j, info);
-	if (changed < 0 || changed)
-		return changed < 0 ? isl_change_error : isl_change_drop_second;
+	if (info[i].bmap->n_div < info[j].bmap->n_div)
+		change = coalesce_after_aligning_divs(info[i].bmap, i, j, info);
+	if (change != isl_change_none)
+		return change;
 
-	changed = coalesced_subset(j, i, info);
-	if (changed < 0 || changed)
-		return changed < 0 ? isl_change_error : isl_change_drop_first;
+	if (info[j].bmap->n_div < info[i].bmap->n_div)
+		change = coalesce_after_aligning_divs(info[j].bmap, j, i, info);
+	if (change != isl_change_none)
+		return invert_change(change);
 
-	changed = coalesced_subset_with_equalities(i, j, info);
-	if (changed < 0 || changed)
-		return changed < 0 ? isl_change_error : isl_change_drop_second;
+	change = coalesce_subset_with_equalities(i, j, info);
+	if (change != isl_change_none)
+		return change;
 
-	changed = coalesced_subset_with_equalities(j, i, info);
-	if (changed < 0 || changed)
-		return changed < 0 ? isl_change_error : isl_change_drop_first;
+	change = coalesce_subset_with_equalities(j, i, info);
+	if (change != isl_change_none)
+		return invert_change(change);
 
 	return isl_change_none;
 }
@@ -2455,7 +2965,7 @@ static enum isl_change coalesce_pair(int i, int j,
 			return change;
 	}
 
-	change = check_coalesce_subset(i, j, info);
+	change = coalesce_divs(i, j, info);
 	if (change != isl_change_none)
 		return change;
 
diff --git a/polly/lib/External/isl/isl_convex_hull.c b/polly/lib/External/isl/isl_convex_hull.c
index 5795e66df466..1c732b39eacb 100644
--- a/polly/lib/External/isl/isl_convex_hull.c
+++ b/polly/lib/External/isl/isl_convex_hull.c
@@ -79,6 +79,11 @@ int isl_basic_set_constraint_is_redundant(struct isl_basic_set **bset,
  * constraints.  If the minimal value along the normal of a constraint
  * is the same if the constraint is removed, then the constraint is redundant.
  *
+ * Since some constraints may be mutually redundant, sort the constraints
+ * first such that constraints that involve existentially quantified
+ * variables are considered for removal before those that do not.
+ * The sorting is also need for the use in map_simple_hull.
+ *
  * Alternatively, we could have intersected the basic map with the
  * corresponding equality and then checked if the dimension was that
  * of a facet.
@@ -99,6 +104,7 @@ __isl_give isl_basic_map *isl_basic_map_remove_redundancies(
 	if (bmap->n_ineq <= 1)
 		return bmap;
 
+	bmap = isl_basic_map_sort_constraints(bmap);
 	tab = isl_tab_from_basic_map(bmap, 0);
 	if (isl_tab_detect_implicit_equalities(tab) < 0)
 		goto error;
@@ -2399,11 +2405,12 @@ static __isl_give isl_basic_map *cached_simple_hull(__isl_take isl_map *map,
  * by only (translates of) the constraints in the constituents of map.
  * Translation is only allowed if "shift" is set.
  *
- * Sort the constraints before removing redundant constraints
+ * The constraints are sorted while removing redundant constraints
  * in order to indicate a preference of which constraints should
  * be preserved.  In particular, pairs of constraints that are
  * sorted together are preferred to either both be preserved
- * or both be removed.
+ * or both be removed.  The sorting is performed inside
+ * isl_basic_map_remove_redundancies.
  *
  * The result of the computation is stored in map->cached_simple_hull[shift]
  * such that it can be reused in subsequent calls.  The cache is cleared
@@ -2444,7 +2451,6 @@ static __isl_give isl_basic_map *map_simple_hull(__isl_take isl_map *map,
 	hull = isl_basic_map_overlying_set(bset, model);
 
 	hull = isl_basic_map_intersect(hull, affine_hull);
-	hull = isl_basic_map_sort_constraints(hull);
 	hull = isl_basic_map_remove_redundancies(hull);
 
 	if (hull) {
diff --git a/polly/lib/External/isl/isl_schedule_band.c b/polly/lib/External/isl/isl_schedule_band.c
index c25d773864b4..f0d912173915 100644
--- a/polly/lib/External/isl/isl_schedule_band.c
+++ b/polly/lib/External/isl/isl_schedule_band.c
@@ -907,6 +907,57 @@ error:
 	return NULL;
 }
 
+/* Return the "isolate" option associated to "band", assuming
+ * it at appears at schedule depth "depth".
+ *
+ * The isolate option is of the form
+ *
+ *	isolate[[flattened outer bands] -> band]
+ */
+__isl_give isl_set *isl_schedule_band_get_ast_isolate_option(
+	__isl_keep isl_schedule_band *band, int depth)
+{
+	isl_space *space;
+	isl_set *isolate;
+
+	if (!band)
+		return NULL;
+
+	space = isl_schedule_band_get_space(band);
+	space = isl_space_from_range(space);
+	space = isl_space_add_dims(space, isl_dim_in, depth);
+	space = isl_space_wrap(space);
+	space = isl_space_set_tuple_name(space, isl_dim_set, "isolate");
+
+	isolate = isl_union_set_extract_set(band->ast_build_options, space);
+
+	return isolate;
+}
+
+/* Replace the option "drop" in the AST build options by "add".
+ * That is, remove "drop" and add "add".
+ */
+__isl_give isl_schedule_band *isl_schedule_band_replace_ast_build_option(
+	__isl_take isl_schedule_band *band, __isl_take isl_set *drop,
+	__isl_take isl_set *add)
+{
+	isl_union_set *options;
+
+	band = isl_schedule_band_cow(band);
+	if (!band)
+		return NULL;
+
+	options = band->ast_build_options;
+	options = isl_union_set_subtract(options, isl_union_set_from_set(drop));
+	options = isl_union_set_union(options, isl_union_set_from_set(add));
+	band->ast_build_options = options;
+
+	if (!band->ast_build_options)
+		return isl_schedule_band_free(band);
+
+	return band;
+}
+
 /* Multiply the partial schedule of "band" with the factors in "mv".
  * Replace the result by its greatest integer part to ensure
  * that the schedule is always integral.
@@ -1117,8 +1168,7 @@ error:
  * We apply the transformation even if "n" is zero to ensure consistent
  * behavior with respect to changes in the schedule space.
  *
- * The loop AST generation types for the isolated part become
- * meaningless after dropping dimensions, so we remove them.
+ * The caller is responsible for updating the isolate option.
  */
 __isl_give isl_schedule_band *isl_schedule_band_drop(
 	__isl_take isl_schedule_band *band, int pos, int n)
@@ -1144,8 +1194,10 @@ __isl_give isl_schedule_band *isl_schedule_band_drop(
 	if (band->loop_type)
 		for (i = pos + n; i < band->n; ++i)
 			band->loop_type[i - n] = band->loop_type[i];
-	free(band->isolate_loop_type);
-	band->isolate_loop_type = NULL;
+	if (band->isolate_loop_type)
+		for (i = pos + n; i < band->n; ++i)
+			band->isolate_loop_type[i - n] =
+						    band->isolate_loop_type[i];
 
 	band->n -= n;
 
diff --git a/polly/lib/External/isl/isl_schedule_band.h b/polly/lib/External/isl/isl_schedule_band.h
index bc58fbf58545..dcf16eb5d49c 100644
--- a/polly/lib/External/isl/isl_schedule_band.h
+++ b/polly/lib/External/isl/isl_schedule_band.h
@@ -80,6 +80,11 @@ __isl_give isl_union_set *isl_schedule_band_get_ast_build_options(
 	__isl_keep isl_schedule_band *band);
 __isl_give isl_schedule_band *isl_schedule_band_set_ast_build_options(
 	__isl_take isl_schedule_band *band, __isl_take isl_union_set *options);
+__isl_give isl_set *isl_schedule_band_get_ast_isolate_option(
+	__isl_keep isl_schedule_band *band, int depth);
+__isl_give isl_schedule_band *isl_schedule_band_replace_ast_build_option(
+	__isl_take isl_schedule_band *band, __isl_take isl_set *drop,
+	__isl_take isl_set *add);
 
 int isl_schedule_band_n_member(__isl_keep isl_schedule_band *band);
 isl_bool isl_schedule_band_member_get_coincident(
diff --git a/polly/lib/External/isl/isl_schedule_node.c b/polly/lib/External/isl/isl_schedule_node.c
index 61ee92493f92..a636d744722d 100644
--- a/polly/lib/External/isl/isl_schedule_node.c
+++ b/polly/lib/External/isl/isl_schedule_node.c
@@ -1670,6 +1670,20 @@ error:
 	return NULL;
 }
 
+/* Return the "isolate" option associated to band node "node".
+ */
+__isl_give isl_set *isl_schedule_node_band_get_ast_isolate_option(
+	__isl_keep isl_schedule_node *node)
+{
+	int depth;
+
+	if (!node)
+		return NULL;
+
+	depth = isl_schedule_node_get_schedule_depth(node);
+	return isl_schedule_tree_band_get_ast_isolate_option(node->tree, depth);
+}
+
 /* Make sure that that spaces of "node" and "mv" are the same.
  * Return -1 on error, reporting the error to the user.
  */
@@ -1945,14 +1959,18 @@ __isl_give isl_schedule_node *isl_schedule_node_band_sink(
 /* Split "node" into two nested band nodes, one with the first "pos"
  * dimensions and one with the remaining dimensions.
  * The schedules of the two band nodes live in anonymous spaces.
+ * The loop AST generation type options and the isolate option
+ * are split over the the two band nodes.
  */
 __isl_give isl_schedule_node *isl_schedule_node_band_split(
 	__isl_take isl_schedule_node *node, int pos)
 {
+	int depth;
 	isl_schedule_tree *tree;
 
+	depth = isl_schedule_node_get_schedule_depth(node);
 	tree = isl_schedule_node_get_tree(node);
-	tree = isl_schedule_tree_band_split(tree, pos);
+	tree = isl_schedule_tree_band_split(tree, pos, depth);
 	return isl_schedule_node_graft_tree(node, tree);
 }
 
diff --git a/polly/lib/External/isl/isl_schedule_tree.c b/polly/lib/External/isl/isl_schedule_tree.c
index 4a5b67e23583..b764edd80735 100644
--- a/polly/lib/External/isl/isl_schedule_tree.c
+++ b/polly/lib/External/isl/isl_schedule_tree.c
@@ -1284,6 +1284,22 @@ error:
 	return NULL;
 }
 
+/* Return the "isolate" option associated to the band tree root of "tree",
+ * which is assumed to appear at schedule depth "depth".
+ */
+__isl_give isl_set *isl_schedule_tree_band_get_ast_isolate_option(
+	__isl_keep isl_schedule_tree *tree, int depth)
+{
+	if (!tree)
+		return NULL;
+
+	if (tree->type != isl_schedule_node_band)
+		isl_die(isl_schedule_tree_get_ctx(tree), isl_error_invalid,
+			"not a band node", return NULL);
+
+	return isl_schedule_band_get_ast_isolate_option(tree->band, depth);
+}
+
 /* Return the context of the context tree root.
  */
 __isl_give isl_set *isl_schedule_tree_context_get_context(
@@ -2164,14 +2180,95 @@ error:
 	return NULL;
 }
 
+/* Given an isolate AST generation option "isolate" for a band of size pos + n,
+ * return the corresponding option for a band covering the first "pos"
+ * members.
+ *
+ * The input isolate option is of the form
+ *
+ *	isolate[[flattened outer bands] -> [pos; n]]
+ *
+ * The output isolate option is of the form
+ *
+ *	isolate[[flattened outer bands] -> [pos]]
+ */
+static __isl_give isl_set *isolate_initial(__isl_keep isl_set *isolate,
+	int pos, int n)
+{
+	isl_id *id;
+	isl_map *map;
+
+	isolate = isl_set_copy(isolate);
+	id = isl_set_get_tuple_id(isolate);
+	map = isl_set_unwrap(isolate);
+	map = isl_map_project_out(map, isl_dim_out, pos, n);
+	isolate = isl_map_wrap(map);
+	isolate = isl_set_set_tuple_id(isolate, id);
+
+	return isolate;
+}
+
+/* Given an isolate AST generation option "isolate" for a band of size pos + n,
+ * return the corresponding option for a band covering the final "n"
+ * members within a band covering the first "pos" members.
+ *
+ * The input isolate option is of the form
+ *
+ *	isolate[[flattened outer bands] -> [pos; n]]
+ *
+ * The output isolate option is of the form
+ *
+ *	isolate[[flattened outer bands; pos] -> [n]]
+ *
+ *
+ * The range is first split into
+ *
+ *	isolate[[flattened outer bands] -> [[pos] -> [n]]]
+ *
+ * and then the first pos members are moved to the domain
+ *
+ *	isolate[[[flattened outer bands] -> [pos]] -> [n]]
+ *
+ * after which the domain is flattened to obtain the desired output.
+ */
+static __isl_give isl_set *isolate_final(__isl_keep isl_set *isolate,
+	int pos, int n)
+{
+	isl_id *id;
+	isl_space *space;
+	isl_multi_aff *ma1, *ma2;
+	isl_map *map;
+
+	isolate = isl_set_copy(isolate);
+	id = isl_set_get_tuple_id(isolate);
+	map = isl_set_unwrap(isolate);
+	space = isl_space_range(isl_map_get_space(map));
+	ma1 = isl_multi_aff_project_out_map(isl_space_copy(space),
+						   isl_dim_set, pos, n);
+	ma2 = isl_multi_aff_project_out_map(space, isl_dim_set, 0, pos);
+	ma1 = isl_multi_aff_range_product(ma1, ma2);
+	map = isl_map_apply_range(map, isl_map_from_multi_aff(ma1));
+	map = isl_map_uncurry(map);
+	map = isl_map_flatten_domain(map);
+	isolate = isl_map_wrap(map);
+	isolate = isl_set_set_tuple_id(isolate, id);
+
+	return isolate;
+}
+
 /* Split the band root node of "tree" into two nested band nodes,
  * one with the first "pos" dimensions and
  * one with the remaining dimensions.
+ * The tree is itself positioned at schedule depth "depth".
+ *
+ * The loop AST generation type options and the isolate option
+ * are split over the the two band nodes.
  */
 __isl_give isl_schedule_tree *isl_schedule_tree_band_split(
-	__isl_take isl_schedule_tree *tree, int pos)
+	__isl_take isl_schedule_tree *tree, int pos, int depth)
 {
 	int n;
+	isl_set *isolate, *tree_isolate, *child_isolate;
 	isl_schedule_tree *child;
 
 	if (!tree)
@@ -2192,8 +2289,16 @@ __isl_give isl_schedule_tree *isl_schedule_tree_band_split(
 	if (!tree || !child)
 		goto error;
 
+	isolate = isl_schedule_tree_band_get_ast_isolate_option(tree, depth);
+	tree_isolate = isolate_initial(isolate, pos, n - pos);
+	child_isolate = isolate_final(isolate, pos, n - pos);
 	child->band = isl_schedule_band_drop(child->band, 0, pos);
+	child->band = isl_schedule_band_replace_ast_build_option(child->band,
+					isl_set_copy(isolate), child_isolate);
 	tree->band = isl_schedule_band_drop(tree->band, pos, n - pos);
+	tree->band = isl_schedule_band_replace_ast_build_option(tree->band,
+					isl_set_copy(isolate), tree_isolate);
+	isl_set_free(isolate);
 	if (!child->band || !tree->band)
 		goto error;
 
diff --git a/polly/lib/External/isl/isl_schedule_tree.h b/polly/lib/External/isl/isl_schedule_tree.h
index c996b721186e..9bb32c40b7c3 100644
--- a/polly/lib/External/isl/isl_schedule_tree.h
+++ b/polly/lib/External/isl/isl_schedule_tree.h
@@ -142,6 +142,8 @@ __isl_give isl_union_set *isl_schedule_tree_band_get_ast_build_options(
 	__isl_keep isl_schedule_tree *tree);
 __isl_give isl_schedule_tree *isl_schedule_tree_band_set_ast_build_options(
 	__isl_take isl_schedule_tree *tree, __isl_take isl_union_set *options);
+__isl_give isl_set *isl_schedule_tree_band_get_ast_isolate_option(
+	__isl_keep isl_schedule_tree *tree, int depth);
 __isl_give isl_set *isl_schedule_tree_context_get_context(
 	__isl_keep isl_schedule_tree *tree);
 __isl_give isl_union_set *isl_schedule_tree_domain_get_domain(
@@ -230,7 +232,7 @@ __isl_give isl_schedule_tree *isl_schedule_tree_band_shift(
 	__isl_take isl_schedule_tree *tree,
 	__isl_take isl_multi_union_pw_aff *shift);
 __isl_give isl_schedule_tree *isl_schedule_tree_band_split(
-	__isl_take isl_schedule_tree *tree, int pos);
+	__isl_take isl_schedule_tree *tree, int pos, int depth);
 __isl_give isl_schedule_tree *isl_schedule_tree_band_gist(
 	__isl_take isl_schedule_tree *tree, __isl_take isl_union_set *context);
 
diff --git a/polly/lib/External/isl/isl_test.c b/polly/lib/External/isl/isl_test.c
index 3d6720a30885..3f2b93f28f99 100644
--- a/polly/lib/External/isl/isl_test.c
+++ b/polly/lib/External/isl/isl_test.c
@@ -1839,6 +1839,31 @@ struct {
 	},
 	{ 1, "[n] -> { [a,b] : (exists e : 1 <= a <= 7e and 9e <= b <= n) or "
 				"(0 <= a <= b <= n) }" },
+	{ 1, "{ [a, b] : 0 <= a <= 2 and b >= 0 and "
+		"((0 < b <= 13) or (2*floor((a + b)/2) >= -5 + a + 2b)) }" },
+	{ 1, "{ [a] : (2 <= a <= 5) or (a mod 2 = 1 and 1 <= a <= 5) }" },
+	{ 1, "{ [a, b, c] : (b = -1 + a and 0 < a <= 3 and "
+				"9*floor((-4a + 2c)/9) <= -3 - 4a + 2c) or "
+			"(exists (e0 = floor((-16 + 2c)/9): a = 4 and "
+				"b = 3 and 9e0 <= -19 + 2c)) }" },
+	{ 0, "{ [a, b, c] : (b <= 2 and b <= -2 + a) or "
+			"(b = -1 + a and 0 < a <= 3 and "
+				"9*floor((-4a + 2c)/9) <= -3 - 4a + 2c) or "
+			"(exists (e0 = floor((-16 + 2c)/9): a = 4 and "
+				"b = 3 and 9e0 <= -19 + 2c)) }" },
+	{ 1, "{ [y, x] : (x - y) mod 3 = 2 and 2 <= y <= 200 and 0 <= x <= 2;"
+		"[1, 0] }" },
+	{ 1, "{ [x, y] : (x - y) mod 3 = 2 and 2 <= y <= 200 and 0 <= x <= 2;"
+		"[0, 1] }" },
+	{ 1, "{ [1, y] : -1 <= y <= 1; [x, -x] : 0 <= x <= 1 }" },
+	{ 1, "{ [1, y] : 0 <= y <= 1; [x, -x] : 0 <= x <= 1 }" },
+	{ 1, "{ [x, y] : 0 <= x <= 10 and x - 4*floor(x/4) <= 1 and y <= 0; "
+	       "[x, y] : 0 <= x <= 10 and x - 4*floor(x/4) > 1 and y <= 0; "
+	       "[x, y] : 0 <= x <= 10 and x - 5*floor(x/5) <= 1 and 0 < y; "
+	       "[x, y] : 0 <= x <= 10 and x - 5*floor(x/5) > 1 and 0 < y }" },
+	{ 1, "{ [x, 0] : 0 <= x <= 10 and x mod 2 = 0; "
+	       "[x, 0] : 0 <= x <= 10 and x mod 2 = 1; "
+	       "[x, y] : 0 <= x <= 10 and 1 <= y <= 10 }" },
 };
 
 /* A specialized coalescing test case that would result
diff --git a/polly/lib/External/isl/test_inputs/codegen/correlation.c b/polly/lib/External/isl/test_inputs/codegen/correlation.c
index 25d99e193113..f821db6c2687 100644
--- a/polly/lib/External/isl/test_inputs/codegen/correlation.c
+++ b/polly/lib/External/isl/test_inputs/codegen/correlation.c
@@ -1,53 +1,53 @@
 for (int c0 = 0; c0 < m; c0 += 32)
   for (int c1 = (n >= 32 && m >= c0 + 2) || (m == 1 && c0 == 0) ? 0 : 32 * n - 32 * floord(31 * n + 31, 32); c1 <= ((n <= -1 && c0 == 0) || (m == 1 && n >= 0 && c0 == 0) ? max(0, n - 1) : n); c1 += 32)
     for (int c2 = c0; c2 <= (m >= 2 && c0 + 31 >= m && n >= c1 && c1 + 31 >= n ? 2 * m - 3 : (m >= 2 * c0 + 63 && c1 <= -32 && n >= c1 && c1 + 31 >= n) || (m >= c0 + 32 && 2 * c0 + 62 >= m && n >= c1 && c1 + 31 >= n) || (n >= 0 && c0 >= 32 && m >= 2 * c0 + 63 && c1 == n) || (m >= 63 && n >= 32 && c0 == 0 && c1 == n) ? 2 * c0 + 61 : m - 1); c2 += 32) {
-      if (c1 >= n) {
-        if (c0 == 0 && c1 == 0)
+      if (m >= 2) {
+        if (n <= 0 && c0 == 0 && c1 == 0)
           for (int c5 = 0; c5 <= min(31, m - c2 - 1); c5 += 1)
             S_14(c2 + c5);
-        if (c1 == n)
-          for (int c3 = max(0, (c2 / 2) - c0 + 1); c3 <= min(31, m - c0 - 1); c3 += 1)
+        if (n >= 0 && c1 == n) {
+          for (int c3 = max(0, (c2 / 2) - c0 + 1); c3 <= min(31, m - c0 - 2); c3 += 1)
             for (int c5 = max(0, c0 - c2 + c3); c5 <= min(31, 2 * c0 - c2 + 2 * c3 - 1); c5 += 1)
               S_29(-c0 + c2 - c3 + c5, c0 + c3);
-      } else if (c1 >= 0 && m >= c2 + 1) {
-        for (int c3 = 0; c3 <= min(min(31, m - c0 - 2), -c0 + c2 + 30); c3 += 1) {
-          for (int c4 = 0; c4 <= min(31, n - c1 - 1); c4 += 1) {
-            if (c0 == 0 && c2 == 0 && c3 == 0) {
-              if (c1 == 0 && c4 == 0)
-                S_14(0);
-              S_19(c1 + c4, 0);
-            }
-            for (int c5 = max(0, c0 - c2 + c3 + 1); c5 <= min(31, m - c2 - 1); c5 += 1) {
-              if (c0 == 0 && c1 == 0 && c3 == 0 && c4 == 0)
-                S_14(c2 + c5);
-              if (c0 == 0 && c3 == 0)
-                S_19(c1 + c4, c2 + c5);
-              S_27(c0 + c3, c2 + c5, c1 + c4);
+        } else if (n >= c1 + 1 && c1 >= 0 && c1 + 31 >= n && c2 >= m) {
+          for (int c3 = max(0, (c2 / 2) - c0 + 1); c3 <= min(31, m - c0 - 2); c3 += 1)
+            for (int c5 = 0; c5 <= min(31, 2 * c0 - c2 + 2 * c3 - 1); c5 += 1)
+              S_29(-c0 + c2 - c3 + c5, c0 + c3);
+        } else if (c1 <= -32 && n >= c1 && c1 + 31 >= n) {
+          for (int c3 = max(0, (c2 / 2) - c0 + 1); c3 <= min(31, m - c0 - 2); c3 += 1)
+            for (int c5 = max(0, c0 - c2 + c3); c5 <= min(31, 2 * c0 - c2 + 2 * c3 - 1); c5 += 1)
+              S_29(-c0 + c2 - c3 + c5, c0 + c3);
+        } else if (n >= c1 + 1 && c1 >= 0 && m >= c2 + 1) {
+          for (int c3 = 0; c3 <= min(min(31, m - c0 - 2), -c0 + c2 + 30); c3 += 1) {
+            for (int c4 = 0; c4 <= min(31, n - c1 - 1); c4 += 1) {
+              if (c0 == 0 && c2 == 0 && c3 == 0) {
+                if (c1 == 0 && c4 == 0)
+                  S_14(0);
+                S_19(c1 + c4, 0);
+              }
+              for (int c5 = max(0, c0 - c2 + c3 + 1); c5 <= min(31, m - c2 - 1); c5 += 1) {
+                if (c0 == 0 && c1 == 0 && c3 == 0 && c4 == 0)
+                  S_14(c2 + c5);
+                if (c0 == 0 && c3 == 0)
+                  S_19(c1 + c4, c2 + c5);
+                S_27(c0 + c3, c2 + c5, c1 + c4);
+              }
             }
+            if (c1 + 31 >= n)
+              for (int c5 = max(0, c0 - c2 + c3); c5 <= min(31, 2 * c0 - c2 + 2 * c3 - 1); c5 += 1)
+                S_29(-c0 + c2 - c3 + c5, c0 + c3);
           }
-          if (c1 + 31 >= n)
-            for (int c5 = max(0, c0 - c2 + c3); c5 <= min(31, 2 * c0 - c2 + 2 * c3 - 1); c5 += 1)
-              S_29(-c0 + c2 - c3 + c5, c0 + c3);
         }
-        if (c0 + 31 >= m && c1 + 31 >= n && c2 == c0) {
-          for (int c5 = m - c0 - 1; c5 <= min(31, 2 * m - c0 - 3); c5 += 1)
-            S_29(-m + c0 + c5 + 1, m - 1);
-        } else if (m >= c0 + 32 && c1 + 31 >= n && c2 == c0) {
+        if (c0 + 32 >= m && n >= c1 && c1 + 31 >= n) {
+          for (int c5 = max(0, m - c2 - 1); c5 <= min(31, 2 * m - c2 - 3); c5 += 1)
+            S_29(-m + c2 + c5 + 1, m - 1);
+        } else if (m >= c0 + 33 && n >= c1 + 1 && c1 >= 0 && c1 + 31 >= n && c2 == c0) {
           S_29(0, c0 + 31);
         }
-      } else if (c1 + 31 >= n && c2 >= m) {
-        for (int c3 = max(0, (c2 / 2) - c0 + 1); c3 <= min(31, m - c0 - 1); c3 += 1)
-          for (int c5 = 0; c5 <= min(31, 2 * c0 - c2 + 2 * c3 - 1); c5 += 1)
-            S_29(-c0 + c2 - c3 + c5, c0 + c3);
-      } else if (c1 <= -32 && c1 + 31 >= n && m >= c2 + 1) {
-        for (int c3 = max(0, (c2 / 2) - c0 + 1); c3 <= min(31, m - c0 - 1); c3 += 1)
-          for (int c5 = max(0, c0 - c2 + c3); c5 <= min(31, 2 * c0 - c2 + 2 * c3 - 1); c5 += 1)
-            S_29(-c0 + c2 - c3 + c5, c0 + c3);
-      }
-      if (m == 1 && c0 == 0 && c1 >= 32 && c2 == 0) {
+      } else if (c1 >= 32 && c2 == 0) {
         for (int c4 = 0; c4 <= min(31, n - c1 - 1); c4 += 1)
           S_19(c1 + c4, 0);
-      } else if (m == 1 && n >= 1 && c0 == 0 && c1 == 0 && c2 == 0) {
+      } else if (c1 == 0 && c2 == 0) {
         S_14(0);
         for (int c4 = 0; c4 <= min(31, n - 1); c4 += 1)
           S_19(c4, 0);
diff --git a/polly/lib/External/isl/test_inputs/codegen/hoist2.c b/polly/lib/External/isl/test_inputs/codegen/hoist2.c
index 24cfc639166e..907652fa9558 100644
--- a/polly/lib/External/isl/test_inputs/codegen/hoist2.c
+++ b/polly/lib/External/isl/test_inputs/codegen/hoist2.c
@@ -1,3 +1,5 @@
 for (int c0 = 1; c0 <= 5; c0 += 1)
-  for (int c1 = t1 - 64 * b + 64; c1 <= min(70, -((c0 - 1) % 2) - c0 + 73); c1 += 64)
-    A(c0, 64 * b + c1 - 8);
+  if (c0 <= 3 || (b == 1 && t1 + c0 >= 10) || (t1 == 5 && b == 1 && c0 == 4))
+    for (int c1 = t1 - 64 * b + 64; c1 <= min(70, -c0 + 73); c1 += 64)
+      if (c0 <= 3 || (t1 + c0 >= 10 && c1 == t1) || c1 == 5)
+        A(c0, 64 * b + c1 - 8);
diff --git a/polly/lib/External/isl/test_inputs/codegen/omega/lefur03-0.c b/polly/lib/External/isl/test_inputs/codegen/omega/lefur03-0.c
index 5e3f4a6e9a47..8b61d263af4c 100644
--- a/polly/lib/External/isl/test_inputs/codegen/omega/lefur03-0.c
+++ b/polly/lib/External/isl/test_inputs/codegen/omega/lefur03-0.c
@@ -1,7 +1,7 @@
 for (int c0 = 0; c0 <= 3; c0 += 1)
-  for (int c1 = max(2 * c0 - 3, c0 / 2); c1 <= min(3, c0 + 1); c1 += 1)
+  for (int c1 = max(0, 2 * c0 - 3); c1 <= min(3, c0 + 1); c1 += 1)
     for (int c2 = c0; c2 <= min(min(3, 2 * c0 - c1 + 1), 3 * c1 + 2); c2 += 1)
-      for (int c3 = max(max(max(0, c1 - (-c1 + 3) / 3), 2 * c0 - (c0 + c1 + 1) / 3 - 1), c2 + floord(3 * c1 - c2 - 1, 6)); c3 <= min(3, c0 + 1); c3 += 1)
+      for (int c3 = max(max(max(0, c1 - (-c1 + 3) / 3), c0 - (-c2 + 3) / 3), c2 + floord(3 * c1 - c2 - 1, 6)); c3 <= min(3, c0 + 1); c3 += 1)
         for (int c4 = max(max(max(max(-200 * c1 + 400 * c3 - 199, 250 * c3 + 1), 667 * c0 - 333 * c1 - (c0 + c1 + 3) / 3 - 332), 333 * c1 + c1 / 3), 333 * c2 + (c2 + 1) / 3); c4 <= min(min(min(min(1000, 500 * c0 + 499), -200 * c1 + 400 * c3 + 400), 333 * c2 - (-c2 + 3) / 3 + 333), 333 * c3 - (-c3 + 3) / 3 + 334); c4 += 1)
           for (int c5 = max(max(max(c4, 1000 * c0 - c4), 1000 * c3 - 2 * c4 + 2), 500 * c1 + (c4 + 1) / 2); c5 <= min(min(min(2 * c4 + 1, 1000 * c0 - c4 + 999), 1000 * c3 - 2 * c4 + 1001), 500 * c1 + (c4 + 1) / 2 + 499); c5 += 1)
             s0(c0, c1, c2, c3, c4, c5);
diff --git a/polly/lib/External/isl/test_inputs/codegen/omega/lefur04-0.c b/polly/lib/External/isl/test_inputs/codegen/omega/lefur04-0.c
index 4b99579554ee..d0046d928f4b 100644
--- a/polly/lib/External/isl/test_inputs/codegen/omega/lefur04-0.c
+++ b/polly/lib/External/isl/test_inputs/codegen/omega/lefur04-0.c
@@ -1,5 +1,5 @@
 for (int c0 = 0; c0 <= 3; c0 += 1)
-  for (int c1 = max(0, 2 * c0 - 3); c1 <= min(3, c0 + 1); c1 += 1)
+  for (int c1 = max(0, 2 * c0 - 3); c1 <= min(c0 + 1, -c0 + 6); c1 += 1)
     for (int c2 = c0; c2 <= min(min(3, 2 * c0 - c1 + 1), 3 * c1 + 2); c2 += 1)
       for (int c3 = max(max(max(0, c1 - (-c1 + 3) / 3), c0 - (-c2 + 3) / 3), c2 + floord(3 * c1 - c2 - 1, 6)); c3 <= min(3, c0 + 1); c3 += 1)
         for (int c5 = max(max(max(max(0, 2 * c3 - 4), c1 - (-c1 + 3) / 3), c2 - (c2 + 3) / 3), c3 - (c3 + 3) / 3); c5 <= min(min(c1 + 1, c3), -c2 + 2 * c3 - (c2 + 3) / 3 + 2); c5 += 1)
diff --git a/polly/lib/External/isl/test_inputs/codegen/omega/wak2-0.c b/polly/lib/External/isl/test_inputs/codegen/omega/wak2-0.c
index 435a1b788bb3..96e9f194616e 100644
--- a/polly/lib/External/isl/test_inputs/codegen/omega/wak2-0.c
+++ b/polly/lib/External/isl/test_inputs/codegen/omega/wak2-0.c
@@ -1,25 +1,23 @@
-{
+if (c2 >= d2 + 1) {
+  for (int c0 = a1; c0 <= b1; c0 += 1)
+    for (int c1_0 = c1; c1_0 <= d1; c1_0 += 1)
+      s0(c0, c1_0);
+} else {
   for (int c0 = a1; c0 <= min(b1, a2 - 1); c0 += 1)
     for (int c1_0 = c1; c1_0 <= d1; c1_0 += 1)
       s0(c0, c1_0);
-  if (c2 >= d2 + 1) {
-    for (int c0 = max(a1, a2); c0 <= min(b1, b2); c0 += 1)
-      for (int c1_0 = c1; c1_0 <= d1; c1_0 += 1)
+  for (int c0 = a2; c0 <= b2; c0 += 1) {
+    if (c0 >= a1 && b1 >= c0)
+      for (int c1_0 = c1; c1_0 <= min(d1, c2 - 1); c1_0 += 1)
         s0(c0, c1_0);
-  } else {
-    for (int c0 = a2; c0 <= b2; c0 += 1) {
-      if (c0 >= a1 && b1 >= c0)
-        for (int c1_0 = c1; c1_0 <= min(d1, c2 - 1); c1_0 += 1)
-          s0(c0, c1_0);
-      for (int c1_0 = c2; c1_0 <= d2; c1_0 += 1) {
-        if (c0 >= a1 && b1 >= c0 && c1_0 >= c1 && d1 >= c1_0)
-          s0(c0, c1_0);
-        s1(c0, c1_0);
-      }
-      if (c0 >= a1 && b1 >= c0)
-        for (int c1_0 = max(c1, d2 + 1); c1_0 <= d1; c1_0 += 1)
-          s0(c0, c1_0);
+    for (int c1_0 = c2; c1_0 <= d2; c1_0 += 1) {
+      if (c0 >= a1 && b1 >= c0 && c1_0 >= c1 && d1 >= c1_0)
+        s0(c0, c1_0);
+      s1(c0, c1_0);
     }
+    if (c0 >= a1 && b1 >= c0)
+      for (int c1_0 = max(c1, d2 + 1); c1_0 <= d1; c1_0 += 1)
+        s0(c0, c1_0);
   }
   for (int c0 = max(max(a1, a2), b2 + 1); c0 <= b1; c0 += 1)
     for (int c1_0 = c1; c1_0 <= d1; c1_0 += 1)
diff --git a/polly/lib/External/isl/test_inputs/codegen/omega/wak2-1.c b/polly/lib/External/isl/test_inputs/codegen/omega/wak2-1.c
index 0f5e74c0de76..b1f7286f280f 100644
--- a/polly/lib/External/isl/test_inputs/codegen/omega/wak2-1.c
+++ b/polly/lib/External/isl/test_inputs/codegen/omega/wak2-1.c
@@ -1,33 +1,31 @@
-{
+if (c2 >= d2 + 1) {
+  for (int c0 = a1; c0 <= b1; c0 += 1)
+    for (int c1_0 = c1; c1_0 <= d1; c1_0 += 1)
+      s0(c0, c1_0);
+} else {
   for (int c0 = a1; c0 <= min(b1, a2 - 1); c0 += 1)
     for (int c1_0 = c1; c1_0 <= d1; c1_0 += 1)
       s0(c0, c1_0);
-  if (c2 >= d2 + 1) {
-    for (int c0 = max(a1, a2); c0 <= min(b1, b2); c0 += 1)
-      for (int c1_0 = c1; c1_0 <= d1; c1_0 += 1)
+  for (int c0 = a2; c0 <= b2; c0 += 1) {
+    if (a1 >= c0 + 1) {
+      for (int c1_0 = c2; c1_0 <= d2; c1_0 += 1)
+        s1(c0, c1_0);
+    } else if (c0 >= b1 + 1) {
+      for (int c1_0 = c2; c1_0 <= d2; c1_0 += 1)
+        s1(c0, c1_0);
+    } else {
+      for (int c1_0 = c1; c1_0 <= min(d1, c2 - 1); c1_0 += 1)
         s0(c0, c1_0);
-  } else {
-    for (int c0 = a2; c0 <= b2; c0 += 1) {
-      if (a1 >= c0 + 1) {
-        for (int c1_0 = c2; c1_0 <= d2; c1_0 += 1)
-          s1(c0, c1_0);
-      } else if (c0 >= b1 + 1) {
-        for (int c1_0 = c2; c1_0 <= d2; c1_0 += 1)
-          s1(c0, c1_0);
-      } else {
-        for (int c1_0 = c1; c1_0 <= min(d1, c2 - 1); c1_0 += 1)
-          s0(c0, c1_0);
-        for (int c1_0 = c2; c1_0 <= min(c1 - 1, d2); c1_0 += 1)
-          s1(c0, c1_0);
-        for (int c1_0 = max(c1, c2); c1_0 <= min(d1, d2); c1_0 += 1) {
-          s0(c0, c1_0);
-          s1(c0, c1_0);
-        }
-        for (int c1_0 = max(c1, d2 + 1); c1_0 <= d1; c1_0 += 1)
-          s0(c0, c1_0);
-        for (int c1_0 = max(max(c1, d1 + 1), c2); c1_0 <= d2; c1_0 += 1)
-          s1(c0, c1_0);
+      for (int c1_0 = c2; c1_0 <= min(c1 - 1, d2); c1_0 += 1)
+        s1(c0, c1_0);
+      for (int c1_0 = max(c1, c2); c1_0 <= min(d1, d2); c1_0 += 1) {
+        s0(c0, c1_0);
+        s1(c0, c1_0);
       }
+      for (int c1_0 = max(c1, d2 + 1); c1_0 <= d1; c1_0 += 1)
+        s0(c0, c1_0);
+      for (int c1_0 = max(max(c1, d1 + 1), c2); c1_0 <= d2; c1_0 += 1)
+        s1(c0, c1_0);
     }
   }
   for (int c0 = max(max(a1, a2), b2 + 1); c0 <= b1; c0 += 1)
diff --git a/polly/lib/External/isl/test_inputs/codegen/unroll4.c b/polly/lib/External/isl/test_inputs/codegen/unroll4.c
index 30b2ba8efa89..6d4c3411f4da 100644
--- a/polly/lib/External/isl/test_inputs/codegen/unroll4.c
+++ b/polly/lib/External/isl/test_inputs/codegen/unroll4.c
@@ -2,14 +2,14 @@
   write_shared_A(3, ((t1 + 3) % 4) + 1, ((t2 + 31) % 32) + 1);
   if (t2 >= 1 && t2 <= 2 && t1 % 3 == 0)
     write_shared_A(3, (-t1 / 3) + 4, t2 + 32);
-  if ((t1 >= 1 && t1 <= 2 && t2 >= 3 && t2 <= 4) || ((-((t1 + 3) % 4) + t2 + 30) % 32) + t1 >= -4 * ((-t1 + 4) / 4) + 4)
+  if (((-((t1 + 3) % 4) + t2 + 30) % 32) + t1 >= ((t1 + 3) % 4) + ((t2 + 1) % 2) - 4 * ((-t1 + 4) / 4) + 1)
     write_shared_A(3, ((t1 + 3) % 4) + 5, -((((t1 + 3) % 4) - t2 + 33) % 32) + t1 + 4 * ((-t1 + 4) / 4) + 32);
   if (t1 >= 1 && t2 >= t1 + 1 && t2 <= 4)
     write_shared_A(3, t1 + 4, t2 + 32);
   write_shared_A(4, ((t1 + 3) % 4) + 1, ((t2 + 31) % 32) + 1);
   if (t2 >= 1 && t2 <= 2 && t1 % 3 == 0)
     write_shared_A(4, (-t1 / 3) + 4, t2 + 32);
-  if ((t1 >= 1 && t1 <= 2 && t2 >= 3 && t2 <= 4) || ((-((t1 + 3) % 4) + t2 + 30) % 32) + t1 >= -4 * ((-t1 + 4) / 4) + 4)
+  if (((-((t1 + 3) % 4) + t2 + 30) % 32) + t1 >= ((t1 + 3) % 4) + ((t2 + 1) % 2) - 4 * ((-t1 + 4) / 4) + 1)
     write_shared_A(4, ((t1 + 3) % 4) + 5, -((((t1 + 3) % 4) - t2 + 33) % 32) + t1 + 4 * ((-t1 + 4) / 4) + 32);
   if (t1 >= 1 && t2 >= t1 + 1 && t2 <= 4)
     write_shared_A(4, t1 + 4, t2 + 32);
diff --git a/polly/lib/External/isl/test_inputs/codegen/unroll6.c b/polly/lib/External/isl/test_inputs/codegen/unroll6.c
index 06010b1e57ca..1d8cc5eb771b 100644
--- a/polly/lib/External/isl/test_inputs/codegen/unroll6.c
+++ b/polly/lib/External/isl/test_inputs/codegen/unroll6.c
@@ -1,5 +1,5 @@
 {
-  if (nn >= 128 * g + 6 && nn >= ((t1 + 127) % 128) + 128 * g + 3 && ((t1 + 127) % 128) + 128 * g >= 0)
+  if (g >= 0 && nn >= 128 * g + 6 && nn >= ((t1 + 127) % 128) + 128 * g + 3)
     for (int c1 = 393214; c1 < nn - 1; c1 += 393216)
       A(c1, ((t1 + 127) % 128) + 128 * g + 1, ((t1 + 127) % 128) + 1);
   if (t1 >= 1 && t1 <= 2 && nn >= t1 + 128 * g + 130 && t1 + 128 * g >= -127)