From e58c023971de02f11b79e632db632d6a38768289 Mon Sep 17 00:00:00 2001
From: Sven Verdoolaege <skimo@kotnet.org>
Date: Thu, 20 Jun 2013 15:45:34 +0200
Subject: [PATCH] use implications to encode while and break filters

Filters that express while or break conditions used to be encoded
by filter maps mapping to all previous iterations.  Since we want
to keep track of index expressions in the future, this commits
breaks such filter maps into two parts, a filter expressing the condition
on the previous iteration and an implication expressing that this condition
extends to all previous iterations.

Signed-off-by: Sven Verdoolaege <skimo@kotnet.org>
---
 emit.c                         |   5 +-
 scan.cc                        | 125 +++++++++++++------
 scop.c                         | 271 +++++++++++++++++++++--------------------
 tests/break3.scop              |  11 +-
 tests/break4.scop              |  40 +++---
 tests/for_while.scop           |  10 +-
 tests/for_while_dec.scop       |  11 +-
 tests/for_while_inc.scop       |  11 +-
 tests/for_while_overflow.scop  |   7 +-
 tests/for_while_unsigned.scop  |  11 +-
 tests/for_while_unsigned2.scop |  11 +-
 tests/unsigned_break2.scop     |  11 +-
 tests/while.scop               |   9 +-
 tests/while_break.scop         |  44 ++++---
 tests/while_inc.scop           |   9 +-
 tests/while_overflow.scop      |   7 +-
 16 files changed, 347 insertions(+), 246 deletions(-)

diff --git a/emit.c b/emit.c
index 5b78758..6982278 100644
--- a/emit.c
+++ b/emit.c
@@ -471,7 +471,7 @@ static int emit_implication(yaml_emitter_t *emitter,
 	return 0;
 }
 
-/* Print the list of "n_implication" "implications" to "emitter".
+/* Print the list of "n_implication" "implications", if any, to "emitter".
  */
 static int emit_implications(yaml_emitter_t *emitter, int n_implication,
 	struct pet_implication **implications)
@@ -479,6 +479,9 @@ static int emit_implications(yaml_emitter_t *emitter, int n_implication,
 	int i;
 	yaml_event_t event;
 
+	if (n_implication == 0)
+		return 0;
+
 	if (emit_string(emitter, "implications") < 0)
 		return -1;
 	if (!yaml_sequence_start_event_initialize(&event, NULL, NULL, 1,
diff --git a/scan.cc b/scan.cc
index c9bb5c6..e716cf3 100644
--- a/scan.cc
+++ b/scan.cc
@@ -2077,29 +2077,76 @@ static __isl_give isl_map *identity_map(__isl_keep isl_set *domain)
 	return id;
 }
 
+/* Create a map that maps elements of a single-dimensional array "id_test"
+ * to the previous element (according to "inc"), provided this element
+ * belongs to "domain".  That is, create the map
+ *
+ *	{ id[x] -> id[x - inc] : x - inc in domain }
+ */
+static __isl_give isl_map *map_to_previous(__isl_take isl_id *id_test,
+	__isl_take isl_set *domain, __isl_take isl_val *inc)
+{
+	isl_space *space;
+	isl_local_space *ls;
+	isl_aff *aff;
+	isl_map *prev;
+
+	space = isl_set_get_space(domain);
+	ls = isl_local_space_from_space(space);
+	aff = isl_aff_var_on_domain(ls, isl_dim_set, 0);
+	aff = isl_aff_add_constant_val(aff, isl_val_neg(inc));
+	prev = isl_map_from_aff(aff);
+	prev = isl_map_intersect_range(prev, domain);
+	prev = isl_map_set_tuple_id(prev, isl_dim_out, id_test);
+
+	return prev;
+}
+
+/* Add an implication to "scop" expressing that if an element of
+ * virtual array "id_test" has value "satisfied" then all previous elements
+ * of this array also have that value.  The set of previous elements
+ * is bounded by "domain".  If "sign" is negative then iterator
+ * is decreasing and we express that all subsequent array elements
+ * (but still defined previously) have the same value.
+ */
+static struct pet_scop *add_implication(struct pet_scop *scop,
+	__isl_take isl_id *id_test, __isl_take isl_set *domain, int sign,
+	int satisfied)
+{
+	isl_space *space;
+	isl_map *map;
+
+	domain = isl_set_set_tuple_id(domain, id_test);
+	space = isl_set_get_space(domain);
+	if (sign > 0)
+		map = isl_map_lex_ge(space);
+	else
+		map = isl_map_lex_le(space);
+	map = isl_map_intersect_range(map, domain);
+	scop = pet_scop_add_implication(scop, map, satisfied);
+
+	return scop;
+}
+
 /* Add a filter to "scop" that imposes that it is only executed
  * when the variable identified by "id_test" has a zero value
  * for all previous iterations of "domain".
+ *
+ * In particular, add a filter that imposes that the array
+ * has a zero value at the previous iteration of domain and
+ * add an implication that implies that it then has that
+ * value for all previous iterations.
  */
 static struct pet_scop *scop_add_break(struct pet_scop *scop,
-	__isl_take isl_id *id_test, __isl_take isl_set *domain, int sign)
+	__isl_take isl_id *id_test, __isl_take isl_set *domain,
+	__isl_take isl_val *inc)
 {
-	isl_ctx *ctx = isl_set_get_ctx(domain);
-	isl_space *space;
-	isl_map *break_access;
 	isl_map *prev;
+	int sign = isl_val_sgn(inc);
 
-	space = isl_space_map_from_set(isl_set_get_space(domain));
-	break_access = isl_map_universe(space);
-	break_access = isl_map_intersect_range(break_access, domain);
-	break_access = isl_map_set_tuple_id(break_access, isl_dim_out, id_test);
-	if (sign > 0)
-		prev = isl_map_lex_gt_first(isl_map_get_space(break_access), 1);
-	else
-		prev = isl_map_lex_lt_first(isl_map_get_space(break_access), 1);
-	break_access = isl_map_intersect(break_access, prev);
-	scop = pet_scop_filter(scop, break_access, 0);
-	scop = pet_scop_merge_filters(scop);
+	prev = map_to_previous(isl_id_copy(id_test), isl_set_copy(domain), inc);
+	scop = add_implication(scop, id_test, domain, sign, 0);
+	scop = pet_scop_filter(scop, prev, 0);
 
 	return scop;
 }
@@ -2142,7 +2189,7 @@ struct pet_scop *PetScan::extract_infinite_loop(Stmt *body)
 	scop = pet_scop_embed(scop, isl_set_copy(domain),
 				isl_map_copy(ident), ident, id);
 	if (has_var_break)
-		scop = scop_add_break(scop, id_test, domain, 1);
+		scop = scop_add_break(scop, id_test, domain, isl_val_one(ctx));
 	else
 		isl_set_free(domain);
 
@@ -2259,6 +2306,10 @@ struct pet_scop *PetScan::extract_affine_while(__isl_take isl_pw_aff *pa,
  * of the loop, while the scop for the body is filtered to depend
  * on "id_test" evaluating to true for all iterations up to the
  * current iteration.
+ * The actual filter only imposes that this virtual array has
+ * value one on the previous or the current iteration.
+ * The fact that this condition also applies to the previous
+ * iterations is enforced by an implication.
  *
  * These filtered scops are then combined into a single scop.
  *
@@ -2267,31 +2318,28 @@ struct pet_scop *PetScan::extract_affine_while(__isl_take isl_pw_aff *pa,
  */
 static struct pet_scop *scop_add_while(struct pet_scop *scop_cond,
 	struct pet_scop *scop_body, __isl_take isl_id *id_test,
-	__isl_take isl_set *domain, int sign)
+	__isl_take isl_set *domain, __isl_take isl_val *inc)
 {
 	isl_ctx *ctx = isl_set_get_ctx(domain);
 	isl_space *space;
 	isl_map *test_access;
 	isl_map *prev;
+	int sign = isl_val_sgn(inc);
+	struct pet_scop *scop;
+
+	prev = map_to_previous(isl_id_copy(id_test), isl_set_copy(domain), inc);
+	scop_cond = pet_scop_filter(scop_cond, prev, 1);
 
 	space = isl_space_map_from_set(isl_set_get_space(domain));
-	test_access = isl_map_universe(space);
-	test_access = isl_map_intersect_range(test_access, domain);
-	test_access = isl_map_set_tuple_id(test_access, isl_dim_out, id_test);
-	if (sign > 0)
-		prev = isl_map_lex_ge_first(isl_map_get_space(test_access), 1);
-	else
-		prev = isl_map_lex_le_first(isl_map_get_space(test_access), 1);
-	test_access = isl_map_intersect(test_access, prev);
-	scop_body = pet_scop_filter(scop_body, isl_map_copy(test_access), 1);
-	if (sign > 0)
-		prev = isl_map_lex_gt_first(isl_map_get_space(test_access), 1);
-	else
-		prev = isl_map_lex_lt_first(isl_map_get_space(test_access), 1);
-	test_access = isl_map_intersect(test_access, prev);
-	scop_cond = pet_scop_filter(scop_cond, test_access, 1);
+	test_access = isl_map_identity(space);
+	test_access = isl_map_set_tuple_id(test_access, isl_dim_out,
+						isl_id_copy(id_test));
+	scop_body = pet_scop_filter(scop_body, test_access, 1);
 
-	return pet_scop_add_seq(ctx, scop_cond, scop_body);
+	scop = pet_scop_add_seq(ctx, scop_cond, scop_body);
+	scop = add_implication(scop, id_test, domain, sign, 1);
+
+	return scop;
 }
 
 /* Check if the while loop is of the form
@@ -2372,11 +2420,12 @@ struct pet_scop *PetScan::extract(WhileStmt *stmt)
 
 	if (has_var_break) {
 		scop = scop_add_break(scop, isl_id_copy(id_break_test),
-					isl_set_copy(domain), 1);
+					isl_set_copy(domain), isl_val_one(ctx));
 		scop_body = scop_add_break(scop_body, id_break_test,
-					isl_set_copy(domain), 1);
+					isl_set_copy(domain), isl_val_one(ctx));
 	}
-	scop = scop_add_while(scop, scop_body, id_test, domain, 1);
+	scop = scop_add_while(scop, scop_body, id_test, domain,
+				isl_val_one(ctx));
 
 	return scop;
 }
@@ -2933,10 +2982,10 @@ struct pet_scop *PetScan::extract_for(ForStmt *stmt)
 	scop = resolve_nested(scop);
 	if (has_var_break)
 		scop = scop_add_break(scop, id_break_test, isl_set_copy(domain),
-					isl_val_sgn(inc));
+					isl_val_copy(inc));
 	if (id_test) {
 		scop = scop_add_while(scop_cond, scop, id_test, domain,
-					isl_val_sgn(inc));
+					isl_val_copy(inc));
 		isl_set_free(valid_inc);
 	} else {
 		scop = pet_scop_restrict_context(scop, valid_inc);
diff --git a/scop.c b/scop.c
index 647edb2..de62cd8 100644
--- a/scop.c
+++ b/scop.c
@@ -2099,21 +2099,140 @@ error:
 	return pet_expr_free(expr);
 }
 
+/* Look through the applications in "scop" for any that can be
+ * applied to the filter expressed by "map" and "satisified".
+ * If there is any, then apply it to "map" and return the result.
+ * Otherwise, return "map".
+ * "id" is the identifier of the virtual array.
+ *
+ * We only introduce at most one implication for any given virtual array,
+ * so we can apply the implication and return as soon as we find one.
+ */
+static __isl_give isl_map *apply_implications(struct pet_scop *scop,
+	__isl_take isl_map *map, __isl_keep isl_id *id, int satisfied)
+{
+	int i;
+
+	for (i = 0; i < scop->n_implication; ++i) {
+		struct pet_implication *pi = scop->implications[i];
+		isl_id *pi_id;
+
+		if (pi->satisfied != satisfied)
+			continue;
+		pi_id = isl_map_get_tuple_id(pi->extension, isl_dim_in);
+		isl_id_free(pi_id);
+		if (pi_id != id)
+			continue;
+
+		return isl_map_apply_range(map, isl_map_copy(pi->extension));
+	}
+
+	return map;
+}
+
+/* Is the filter expressed by "test" and "satisfied" implied
+ * by filter "pos" on "domain", with filter "expr", taking into
+ * account the implications of "scop"?
+ *
+ * For filter on domain implying that expressed by "test" and "satisfied",
+ * the filter needs to be an access to the same (virtual) array as "test" and
+ * the filter value needs to be equal to "satisfied".
+ * Moreover, the filter access relation, possibly extended by
+ * the implications in "scop" needs to contain "test".
+ */
+static int implies_filter(struct pet_scop *scop,
+	__isl_keep isl_map *domain, int pos, struct pet_expr *expr,
+	__isl_keep isl_map *test, int satisfied)
+{
+	isl_id *test_id, *arg_id;
+	isl_val *val;
+	int is_int;
+	int s;
+	int is_subset;
+	isl_map *implied;
+
+	if (expr->type != pet_expr_access)
+		return 0;
+	test_id = isl_map_get_tuple_id(test, isl_dim_out);
+	arg_id = pet_expr_access_get_id(expr);
+	isl_id_free(arg_id);
+	isl_id_free(test_id);
+	if (test_id != arg_id)
+		return 0;
+	val = isl_map_plain_get_val_if_fixed(domain, isl_dim_out, pos);
+	is_int = isl_val_is_int(val);
+	if (is_int)
+		s = isl_val_get_num_si(val);
+	isl_val_free(val);
+	if (!val)
+		return -1;
+	if (!is_int)
+		return 0;
+	if (s != satisfied)
+		return 0;
+
+	implied = isl_map_copy(expr->acc.access);
+	implied = apply_implications(scop, implied, test_id, satisfied);
+	is_subset = isl_map_is_subset(test, implied);
+	isl_map_free(implied);
+
+	return is_subset;
+}
+
+/* Is the filter expressed by "test" and "satisfied" implied
+ * by any of the filters on the domain of "stmt", taking into
+ * account the implications of "scop"?
+ */
+static int filter_implied(struct pet_scop *scop,
+	struct pet_stmt *stmt, __isl_keep isl_map *test, int satisfied)
+{
+	int i;
+	int implied;
+	isl_id *test_id;
+	isl_map *domain;
+
+	if (!scop || !stmt || !test)
+		return -1;
+	if (scop->n_implication == 0)
+		return 0;
+	if (stmt->n_arg == 0)
+		return 0;
+
+	domain = isl_set_unwrap(isl_set_copy(stmt->domain));
+
+	implied = 0;
+	for (i = 0; i < stmt->n_arg; ++i) {
+		implied = implies_filter(scop, domain, i, stmt->args[i],
+					 test, satisfied);
+		if (implied < 0 || implied)
+			break;
+	}
+
+	isl_map_free(domain);
+	return implied;
+}
+
 /* Make the statement "stmt" depend on the value of "test"
  * being equal to "satisfied" by adjusting stmt->domain.
  *
  * The domain of "test" corresponds to the (zero or more) outer dimensions
  * of the iteration domain.
  *
- * We insert an argument corresponding to a read to "test"
+ * We first extend "test" to apply to the entire iteration domain and
+ * then check if the filter that we are about to add is implied
+ * by any of the current filters, possibly taking into account
+ * the implications in "scop".  If so, we leave "stmt" untouched and return.
+ *
+ * Otherwise, we insert an argument corresponding to a read to "test"
  * from the iteration domain of "stmt" in front of the list of arguments.
  * We also insert a corresponding output dimension in the wrapped
  * map contained in stmt->domain, with value set to "satisfied".
  */
-static struct pet_stmt *stmt_filter(struct pet_stmt *stmt,
-	__isl_take isl_map *test, int satisfied)
+static struct pet_stmt *stmt_filter(struct pet_scop *scop,
+	struct pet_stmt *stmt, __isl_take isl_map *test, int satisfied)
 {
 	int i;
+	int implied;
 	isl_id *id;
 	isl_ctx *ctx;
 	isl_map *map, *add_dom;
@@ -2124,12 +2243,10 @@ static struct pet_stmt *stmt_filter(struct pet_stmt *stmt,
 	if (!stmt || !test)
 		goto error;
 
-	id = isl_map_get_tuple_id(test, isl_dim_out);
-	map = insert_filter_map(isl_set_get_space(stmt->domain), id, satisfied);
-	stmt->domain = isl_set_apply(stmt->domain, map);
-
-	space = isl_space_unwrap(isl_set_get_space(stmt->domain));
-	dom = isl_set_universe(isl_space_domain(space));
+	space = isl_set_get_space(stmt->domain);
+	if (isl_space_is_wrapping(space))
+		space = isl_space_domain(isl_space_unwrap(space));
+	dom = isl_set_universe(space);
 	n_test_dom = isl_map_dim(test, isl_dim_in);
 	add_dom = isl_map_from_range(dom);
 	add_dom = isl_map_add_dims(add_dom, isl_dim_in, n_test_dom);
@@ -2138,6 +2255,18 @@ static struct pet_stmt *stmt_filter(struct pet_stmt *stmt,
 						    isl_dim_out, i);
 	test = isl_map_apply_domain(test, add_dom);
 
+	implied = filter_implied(scop, stmt, test, satisfied);
+	if (implied < 0)
+		goto error;
+	if (implied) {
+		isl_map_free(test);
+		return stmt;
+	}
+
+	id = isl_map_get_tuple_id(test, isl_dim_out);
+	map = insert_filter_map(isl_set_get_space(stmt->domain), id, satisfied);
+	stmt->domain = isl_set_apply(stmt->domain, map);
+
 	if (args_insert_access(&stmt->n_arg, &stmt->args, test) < 0)
 		goto error;
 
@@ -2359,7 +2488,7 @@ struct pet_scop *pet_scop_filter(struct pet_scop *scop,
 		goto error;
 
 	for (i = 0; i < scop->n_stmt; ++i) {
-		scop->stmts[i] = stmt_filter(scop->stmts[i],
+		scop->stmts[i] = stmt_filter(scop, scop->stmts[i],
 						isl_map_copy(test), satisfied);
 		if (!scop->stmts[i])
 			goto error;
@@ -2372,128 +2501,6 @@ error:
 	return pet_scop_free(scop);
 }
 
-/* Do the filters "i" and "j" always have the same value?
- */
-static int equal_filter_values(__isl_keep isl_set *domain, int i, int j)
-{
-	isl_map *map, *test;
-	int equal;
-
-	map = isl_set_unwrap(isl_set_copy(domain));
-	test = isl_map_universe(isl_map_get_space(map));
-	test = isl_map_equate(test, isl_dim_out, i, isl_dim_out, j);
-	equal = isl_map_is_subset(map, test);
-	isl_map_free(map);
-	isl_map_free(test);
-
-	return equal;
-}
-
-/* Merge filters "i" and "j" into a single filter ("i") with as filter
- * access relation, the union of the two access relations.
- */
-static struct pet_stmt *merge_filter_pair(struct pet_stmt *stmt, int i, int j)
-{
-	int k;
-	isl_map *map;
-
-	if (!stmt)
-		return NULL;
-
-	stmt->args[i]->acc.access = isl_map_union(stmt->args[i]->acc.access,
-				    isl_map_copy(stmt->args[j]->acc.access));
-	stmt->args[i]->acc.access = isl_map_coalesce(stmt->args[i]->acc.access);
-
-	pet_expr_free(stmt->args[j]);
-	for (k = j; k < stmt->n_arg - 1; ++k)
-		stmt->args[k] = stmt->args[k + 1];
-	stmt->n_arg--;
-
-	map = isl_set_unwrap(stmt->domain);
-	map = isl_map_project_out(map, isl_dim_out, j, 1);
-	stmt->domain = isl_map_wrap(map);
-
-	if (!stmt->domain || !stmt->args[i]->acc.access)
-		return pet_stmt_free(stmt);
-
-	return stmt;
-}
-
-/* Look for any pair of filters that access the same filter variable
- * and that have the same filter value and merge them into a single
- * filter with as filter access relation the union of the filter access
- * relations.
- */
-static struct pet_stmt *stmt_merge_filters(struct pet_stmt *stmt)
-{
-	int i, j;
-	isl_space *space_i, *space_j;
-
-	if (!stmt)
-		return NULL;
-	if (stmt->n_arg <= 1)
-		return stmt;
-
-	for (i = 0; i < stmt->n_arg - 1; ++i) {
-		if (stmt->args[i]->type != pet_expr_access)
-			continue;
-		if (pet_expr_is_affine(stmt->args[i]))
-			continue;
-
-		space_i = isl_map_get_space(stmt->args[i]->acc.access);
-		
-		for (j = stmt->n_arg - 1; j > i; --j) {
-			int eq;
-
-			if (stmt->args[j]->type != pet_expr_access)
-				continue;
-			if (pet_expr_is_affine(stmt->args[j]))
-				continue;
-
-			space_j = isl_map_get_space(stmt->args[j]->acc.access);
-
-			eq = isl_space_is_equal(space_i, space_j);
-			if (eq >= 0 && eq)
-				eq = equal_filter_values(stmt->domain, i, j);
-			if (eq >= 0 && eq)
-				stmt = merge_filter_pair(stmt, i, j);
-
-			isl_space_free(space_j);
-
-			if (eq < 0 || !stmt)
-				break;
-		}
-
-		isl_space_free(space_i);
-
-		if (j > i || !stmt)
-			return pet_stmt_free(stmt);
-	}
-
-	return stmt;
-}
-
-/* Look for any pair of filters that access the same filter variable
- * and that have the same filter value and merge them into a single
- * filter with as filter access relation the union of the filter access
- * relations.
- */
-struct pet_scop *pet_scop_merge_filters(struct pet_scop *scop)
-{
-	int i;
-
-	if (!scop)
-		return NULL;
-
-	for (i = 0; i < scop->n_stmt; ++i) {
-		scop->stmts[i] = stmt_merge_filters(scop->stmts[i]);
-		if (!scop->stmts[i])
-			return pet_scop_free(scop);
-	}
-
-	return scop;
-}
-
 /* Add all parameters in "expr" to "dim" and return the result.
  */
 static __isl_give isl_space *expr_collect_params(struct pet_expr *expr,
diff --git a/tests/break3.scop b/tests/break3.scop
index 5fa1401..2f56a03 100644
--- a/tests/break3.scop
+++ b/tests/break3.scop
@@ -32,7 +32,7 @@ statements:
       write: 0
   arguments:
   - type: access
-    relation: '{ S_0[i, j] -> __pet_test_0[i, o1] : o1 <= -1 + j and o1 >= 0 }'
+    relation: '{ S_0[i, j] -> __pet_test_0[i, -1 + j] : j >= 1 }'
     reference: __pet_ref_0
     read: 1
     write: 0
@@ -52,7 +52,7 @@ statements:
       name: f
   arguments:
   - type: access
-    relation: '{ S_1[i, j] -> __pet_test_0[i, o1] : o1 <= -1 + j and o1 >= 0 }'
+    relation: '{ S_1[i, j] -> __pet_test_0[i, -1 + j] : j >= 1 }'
     reference: __pet_ref_3
     read: 1
     write: 0
@@ -83,8 +83,11 @@ statements:
         write: 0
   arguments:
   - type: access
-    relation: '{ S_2[i, j] -> __pet_test_0[i, o1] : o1 <= -1 + j and o1 >= 0; S_2[i,
-      j] -> __pet_test_0[i, j] }'
+    relation: '{ S_2[i, j] -> __pet_test_0[i, j] }'
     reference: __pet_ref_5
     read: 1
     write: 0
+implications:
+- satisfied: 0
+  extension: '{ __pet_test_0[i, j] -> __pet_test_0[i, j''] : i >= 0 and i <= 99 and
+    j'' <= j and j'' >= 0 and j'' <= 99 }'
diff --git a/tests/break4.scop b/tests/break4.scop
index b5dc2fb..4647a6c 100644
--- a/tests/break4.scop
+++ b/tests/break4.scop
@@ -104,7 +104,7 @@ statements:
       write: 0
   arguments:
   - type: access
-    relation: '{ S_0[i, j] -> __pet_test_12[i, o1] : o1 <= -1 + j and o1 >= 0 }'
+    relation: '{ S_0[i, j] -> __pet_test_12[i, -1 + j] : j >= 1 }'
     reference: __pet_ref_0
     read: 1
     write: 0
@@ -124,7 +124,7 @@ statements:
       name: f
   arguments:
   - type: access
-    relation: '{ S_1[i, j] -> __pet_test_12[i, o1] : o1 <= -1 + j and o1 >= 0 }'
+    relation: '{ S_1[i, j] -> __pet_test_12[i, -1 + j] }'
     reference: __pet_ref_3
     read: 1
     write: 0
@@ -159,7 +159,7 @@ statements:
         write: 0
   arguments:
   - type: access
-    relation: '{ S_2[i, j] -> __pet_test_12[i, o1] : o1 <= -1 + j and o1 >= 0 }'
+    relation: '{ S_2[i, j] -> __pet_test_12[i, -1 + j] : j >= 1 }'
     reference: __pet_ref_5
     read: 1
     write: 0
@@ -179,7 +179,7 @@ statements:
       name: f
   arguments:
   - type: access
-    relation: '{ S_3[i, j] -> __pet_test_12[i, o1] : o1 <= -1 + j and o1 >= 0 }'
+    relation: '{ S_3[i, j] -> __pet_test_12[i, -1 + j] : j >= 1 }'
     reference: __pet_ref_10
     read: 1
     write: 0
@@ -205,7 +205,7 @@ statements:
       name: f
   arguments:
   - type: access
-    relation: '{ S_4[i, j] -> __pet_test_12[i, o1] : o1 <= -1 + j and o1 >= 0 }'
+    relation: '{ S_4[i, j] -> __pet_test_12[i, -1 + j] : j >= 1 }'
     reference: __pet_ref_13
     read: 1
     write: 0
@@ -239,7 +239,7 @@ statements:
       write: 0
   arguments:
   - type: access
-    relation: '{ S_5[i, j] -> __pet_test_12[i, o1] : o1 <= -1 + j and o1 >= 0 }'
+    relation: '{ S_5[i, j] -> __pet_test_12[i, -1 + j] : j >= 1 }'
     reference: __pet_ref_17
     read: 1
     write: 0
@@ -275,7 +275,7 @@ statements:
       name: f
   arguments:
   - type: access
-    relation: '{ S_6[i, j] -> __pet_test_12[i, o1] : o1 <= -1 + j and o1 >= 0 }'
+    relation: '{ S_6[i, j] -> __pet_test_12[i, -1 + j] : j >= 1 }'
     reference: __pet_ref_23
     read: 1
     write: 0
@@ -314,7 +314,7 @@ statements:
       write: 0
   arguments:
   - type: access
-    relation: '{ S_7[i, j] -> __pet_test_12[i, o1] : o1 <= -1 + j and o1 >= 0 }'
+    relation: '{ S_7[i, j] -> __pet_test_12[i, -1 + j] : j >= 1 }'
     reference: __pet_ref_28
     read: 1
     write: 0
@@ -376,7 +376,7 @@ statements:
           write: 0
   arguments:
   - type: access
-    relation: '{ S_8[i, j] -> __pet_test_12[i, o1] : o1 <= -1 + j and o1 >= 0 }'
+    relation: '{ S_8[i, j] -> __pet_test_12[i, -1 + j] : j >= 1 }'
     reference: __pet_ref_35
     read: 1
     write: 0
@@ -410,7 +410,7 @@ statements:
       write: 0
   arguments:
   - type: access
-    relation: '{ S_9[i, j] -> __pet_test_12[i, o1] : o1 <= -1 + j and o1 >= 0 }'
+    relation: '{ S_9[i, j] -> __pet_test_12[i, -1 + j] : j >= 1 }'
     reference: __pet_ref_43
     read: 1
     write: 0
@@ -466,7 +466,7 @@ statements:
         write: 0
   arguments:
   - type: access
-    relation: '{ S_10[i, j] -> __pet_test_12[i, o1] : o1 <= -1 + j and o1 >= 0 }'
+    relation: '{ S_10[i, j] -> __pet_test_12[i, -1 + j] : j >= 1 }'
     reference: __pet_ref_49
     read: 1
     write: 0
@@ -512,7 +512,7 @@ statements:
         write: 0
   arguments:
   - type: access
-    relation: '{ S_11[i, j] -> __pet_test_12[i, o1] : o1 <= -1 + j and o1 >= 0 }'
+    relation: '{ S_11[i, j] -> __pet_test_12[i, -1 + j] : j >= 1 }'
     reference: __pet_ref_56
     read: 1
     write: 0
@@ -558,7 +558,7 @@ statements:
           write: 0
   arguments:
   - type: access
-    relation: '{ S_12[i, j] -> __pet_test_12[i, o1] : o1 <= -1 + j and o1 >= 0 }'
+    relation: '{ S_12[i, j] -> __pet_test_12[i, -1 + j] : j >= 1 }'
     reference: __pet_ref_63
     read: 1
     write: 0
@@ -599,7 +599,7 @@ statements:
           write: 0
   arguments:
   - type: access
-    relation: '{ S_13[i, j] -> __pet_test_12[i, o1] : o1 <= -1 + j and o1 >= 0 }'
+    relation: '{ S_13[i, j] -> __pet_test_12[i, -1 + j] : j >= 1 }'
     reference: __pet_ref_69
     read: 1
     write: 0
@@ -619,7 +619,7 @@ statements:
       name: f
   arguments:
   - type: access
-    relation: '{ S_14[i, j] -> __pet_test_12[i, o1] : o1 <= -1 + j and o1 >= 0 }'
+    relation: '{ S_14[i, j] -> __pet_test_12[i, -1 + j] : j >= 1 }'
     reference: __pet_ref_75
     read: 1
     write: 0
@@ -665,7 +665,7 @@ statements:
           write: 0
   arguments:
   - type: access
-    relation: '{ S_15[i, j] -> __pet_test_12[i, o1] : o1 <= -1 + j and o1 >= 0 }'
+    relation: '{ S_15[i, j] -> __pet_test_12[i, -1 + j] : j >= 1 }'
     reference: __pet_ref_78
     read: 1
     write: 0
@@ -706,7 +706,7 @@ statements:
           write: 0
   arguments:
   - type: access
-    relation: '{ S_16[i, j] -> __pet_test_12[i, o1] : o1 <= -1 + j and o1 >= 0 }'
+    relation: '{ S_16[i, j] -> __pet_test_12[i, -1 + j] : j >= 1 }'
     reference: __pet_ref_84
     read: 1
     write: 0
@@ -737,7 +737,7 @@ statements:
         write: 0
   arguments:
   - type: access
-    relation: '{ S_17[i, j] -> __pet_test_12[i, o1] : o1 <= -1 + j and o1 >= 0 }'
+    relation: '{ S_17[i, j] -> __pet_test_12[i, -1 + j] : j >= 1 }'
     reference: __pet_ref_90
     read: 1
     write: 0
@@ -746,3 +746,7 @@ statements:
     reference: __pet_ref_91
     read: 1
     write: 0
+implications:
+- satisfied: 0
+  extension: '{ __pet_test_12[i, j] -> __pet_test_12[i, j''] : i >= 0 and i <= 99
+    and j'' <= j and j'' >= 0 and j'' <= 99 }'
diff --git a/tests/for_while.scop b/tests/for_while.scop
index df79531..ba4f9b5 100644
--- a/tests/for_while.scop
+++ b/tests/for_while.scop
@@ -54,8 +54,7 @@ statements:
         write: 0
   arguments:
   - type: access
-    relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, o1] : o1 >= 0 and o1 <= -1
-      + x2 }'
+    relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, -1 + x2] : x2 >= 1 }'
     reference: __pet_ref_1
     read: 1
     write: 0
@@ -81,8 +80,7 @@ statements:
         write: 0
   arguments:
   - type: access
-    relation: '[n] -> { S2[x1, x2] -> __pet_test_0[x1, o1] : o1 >= 0 and o1 <= x2
-      }'
+    relation: '[n] -> { S2[x1, x2] -> __pet_test_0[x1, x2] }'
     reference: __pet_ref_5
     read: 1
     write: 0
@@ -98,3 +96,7 @@ statements:
       reference: __pet_ref_8
       read: 1
       write: 0
+implications:
+- satisfied: 1
+  extension: '[n] -> { __pet_test_0[x1, x2] -> __pet_test_0[x1, x2''] : x1 >= 0 and
+    x1 <= -1 + n and x2'' <= x2 and x2'' >= 0 }'
diff --git a/tests/for_while_dec.scop b/tests/for_while_dec.scop
index 76e2f9c..1e330f3 100644
--- a/tests/for_while_dec.scop
+++ b/tests/for_while_dec.scop
@@ -56,8 +56,7 @@ statements:
         write: 0
   arguments:
   - type: access
-    relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, o1] : exists (e0 = [(o1)/3]:
-      3e0 = o1 and o1 >= 3 + x2 and o1 <= 9) }'
+    relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, 3 + x2] : x2 <= 6 }'
     reference: __pet_ref_1
     read: 1
     write: 0
@@ -84,8 +83,7 @@ statements:
         write: 0
   arguments:
   - type: access
-    relation: '[n] -> { S2[x1, x2] -> __pet_test_0[x1, o1] : exists (e0 = [(o1)/3]:
-      3e0 = o1 and o1 >= x2 and o1 <= 9) }'
+    relation: '[n] -> { S2[x1, x2] -> __pet_test_0[x1, x2] }'
     reference: __pet_ref_5
     read: 1
     write: 0
@@ -101,3 +99,8 @@ statements:
       reference: __pet_ref_8
       read: 1
       write: 0
+implications:
+- satisfied: 1
+  extension: '[n] -> { __pet_test_0[x1, x2] -> __pet_test_0[x1, x2''] : exists (e0
+    = [(x2'')/3]: 3e0 = x2'' and x1 >= 0 and x1 <= -1 + n and x2'' >= x2 and x2''
+    <= 9) }'
diff --git a/tests/for_while_inc.scop b/tests/for_while_inc.scop
index 48b7459..7f49451 100644
--- a/tests/for_while_inc.scop
+++ b/tests/for_while_inc.scop
@@ -56,8 +56,7 @@ statements:
         write: 0
   arguments:
   - type: access
-    relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, o1] : exists (e0 = [(-1 +
-      o1)/2]: 2e0 = -1 + o1 and o1 >= 9 and o1 <= -2 + x2) }'
+    relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, -2 + x2] : x2 >= 11 }'
     reference: __pet_ref_1
     read: 1
     write: 0
@@ -84,8 +83,7 @@ statements:
         write: 0
   arguments:
   - type: access
-    relation: '[n] -> { S2[x1, x2] -> __pet_test_0[x1, o1] : exists (e0 = [(-1 + o1)/2]:
-      2e0 = -1 + o1 and o1 >= 9 and o1 <= x2) }'
+    relation: '[n] -> { S2[x1, x2] -> __pet_test_0[x1, x2] }'
     reference: __pet_ref_5
     read: 1
     write: 0
@@ -101,3 +99,8 @@ statements:
       reference: __pet_ref_8
       read: 1
       write: 0
+implications:
+- satisfied: 1
+  extension: '[n] -> { __pet_test_0[x1, x2] -> __pet_test_0[x1, x2''] : exists (e0
+    = [(-1 + x2'')/2]: 2e0 = -1 + x2'' and x1 >= 0 and x1 <= -1 + n and x2'' <= x2
+    and x2'' >= 9) }'
diff --git a/tests/for_while_overflow.scop b/tests/for_while_overflow.scop
index 2b4a54a..12a60b6 100644
--- a/tests/for_while_overflow.scop
+++ b/tests/for_while_overflow.scop
@@ -46,7 +46,7 @@ statements:
       name: t
   arguments:
   - type: access
-    relation: '[N] -> { S_1[T] -> __pet_test_0[o0] : o0 >= 0 and o0 <= -1 + T }'
+    relation: '[N] -> { S_1[T] -> __pet_test_0[-1 + T] : T >= 1 }'
     reference: __pet_ref_2
     read: 1
     write: 0
@@ -78,7 +78,10 @@ statements:
         write: 0
   arguments:
   - type: access
-    relation: '[N] -> { S_2[T, i] -> __pet_test_0[o0] : o0 >= 0 and o0 <= T }'
+    relation: '[N] -> { S_2[T, i] -> __pet_test_0[T] }'
     reference: __pet_ref_4
     read: 1
     write: 0
+implications:
+- satisfied: 1
+  extension: '{ __pet_test_0[T] -> __pet_test_0[T''] : T'' <= T and T'' >= 0 }'
diff --git a/tests/for_while_unsigned.scop b/tests/for_while_unsigned.scop
index aa7a012..f01e6f2 100644
--- a/tests/for_while_unsigned.scop
+++ b/tests/for_while_unsigned.scop
@@ -57,8 +57,7 @@ statements:
         write: 0
   arguments:
   - type: access
-    relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, o1] : exists (e0 = [(o1)/3]:
-      3e0 = o1 and o1 >= 3 + x2 and o1 <= 9) }'
+    relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, 3 + x2] : x2 <= 6 }'
     reference: __pet_ref_1
     read: 1
     write: 0
@@ -85,8 +84,7 @@ statements:
         write: 0
   arguments:
   - type: access
-    relation: '[n] -> { S2[x1, x2] -> __pet_test_0[x1, o1] : exists (e0 = [(o1)/3]:
-      3e0 = o1 and o1 >= x2 and o1 <= 9) }'
+    relation: '[n] -> { S2[x1, x2] -> __pet_test_0[x1, x2] }'
     reference: __pet_ref_5
     read: 1
     write: 0
@@ -102,3 +100,8 @@ statements:
       reference: __pet_ref_8
       read: 1
       write: 0
+implications:
+- satisfied: 1
+  extension: '[n] -> { __pet_test_0[x1, x2] -> __pet_test_0[x1, x2''] : exists (e0
+    = [(x2'')/3]: 3e0 = x2'' and x1 >= 0 and x1 <= -1 + n and x2'' >= x2 and x2''
+    <= 9) }'
diff --git a/tests/for_while_unsigned2.scop b/tests/for_while_unsigned2.scop
index 918b34b..63947ca 100644
--- a/tests/for_while_unsigned2.scop
+++ b/tests/for_while_unsigned2.scop
@@ -61,8 +61,7 @@ statements:
         write: 0
   arguments:
   - type: access
-    relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, o1] : exists (e0 = [(o1)/3]:
-      3e0 = o1 and o1 >= 3 + x2 and o1 <= 9) }'
+    relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, 3 + x2] : x2 <= 6 }'
     reference: __pet_ref_1
     read: 1
     write: 0
@@ -100,8 +99,7 @@ statements:
           write: 0
   arguments:
   - type: access
-    relation: '[n] -> { S2[x1, x2, x3] -> __pet_test_0[x1, o1] : exists (e0 = [(o1)/3]:
-      3e0 = o1 and o1 >= x2 and o1 <= 9) }'
+    relation: '[n] -> { S2[x1, x2, x3] -> __pet_test_0[x1, x2] }'
     reference: __pet_ref_5
     read: 1
     write: 0
@@ -117,3 +115,8 @@ statements:
       reference: __pet_ref_9
       read: 1
       write: 0
+implications:
+- satisfied: 1
+  extension: '[n] -> { __pet_test_0[x1, x2] -> __pet_test_0[x1, x2''] : exists (e0
+    = [(x2'')/3]: 3e0 = x2'' and x1 >= 0 and x1 <= -1 + n and x2'' >= x2 and x2''
+    <= 9) }'
diff --git a/tests/unsigned_break2.scop b/tests/unsigned_break2.scop
index d59682a..507bcd7 100644
--- a/tests/unsigned_break2.scop
+++ b/tests/unsigned_break2.scop
@@ -34,7 +34,7 @@ statements:
       write: 0
   arguments:
   - type: access
-    relation: '{ S_0[k] -> __pet_test_0[o0] : o0 <= -1 + k and o0 >= 252 }'
+    relation: '{ S_0[k] -> __pet_test_0[-1 + k] : k >= 253 }'
     reference: __pet_ref_0
     read: 1
     write: 0
@@ -54,7 +54,7 @@ statements:
       name: f
   arguments:
   - type: access
-    relation: '{ S_1[k] -> __pet_test_0[o0] : o0 <= -1 + k and o0 >= 252 }'
+    relation: '{ S_1[k] -> __pet_test_0[-1 + k] : k >= 253 }'
     reference: __pet_ref_3
     read: 1
     write: 0
@@ -78,8 +78,11 @@ statements:
       write: 0
   arguments:
   - type: access
-    relation: '{ S_2[k] -> __pet_test_0[o0] : o0 <= -1 + k and o0 >= 252; S_2[k] ->
-      __pet_test_0[k] }'
+    relation: '{ S_2[k] -> __pet_test_0[k] }'
     reference: __pet_ref_5
     read: 1
     write: 0
+implications:
+- satisfied: 0
+  extension: '{ __pet_test_0[k] -> __pet_test_0[k''] : k'' <= k and k'' >= 252 and
+    k'' <= 261 }'
diff --git a/tests/while.scop b/tests/while.scop
index b4eb62a..2771801 100644
--- a/tests/while.scop
+++ b/tests/while.scop
@@ -54,8 +54,7 @@ statements:
         write: 0
   arguments:
   - type: access
-    relation: '[n] -> { S_1[x, t] -> __pet_test_0[x, o1] : o1 >= 0 and o1 <= -1 +
-      t }'
+    relation: '[n] -> { S_1[x, t] -> __pet_test_0[x, -1 + t] : t >= 1 }'
     reference: __pet_ref_1
     read: 1
     write: 0
@@ -81,7 +80,7 @@ statements:
         write: 0
   arguments:
   - type: access
-    relation: '[n] -> { S2[x, t] -> __pet_test_0[x, o1] : o1 >= 0 and o1 <= t }'
+    relation: '[n] -> { S2[x, t] -> __pet_test_0[x, t] }'
     reference: __pet_ref_5
     read: 1
     write: 0
@@ -97,3 +96,7 @@ statements:
       reference: __pet_ref_8
       read: 1
       write: 0
+implications:
+- satisfied: 1
+  extension: '[n] -> { __pet_test_0[x, t] -> __pet_test_0[x, t''] : x >= 0 and x <=
+    -1 + n and t'' <= t and t'' >= 0 }'
diff --git a/tests/while_break.scop b/tests/while_break.scop
index 277ebf3..0e0537f 100644
--- a/tests/while_break.scop
+++ b/tests/while_break.scop
@@ -84,7 +84,7 @@ statements:
       write: 0
   arguments:
   - type: access
-    relation: '[N] -> { S_2[t] -> __pet_test_0[o0] : o0 >= 0 and o0 <= -1 + t }'
+    relation: '[N] -> { S_2[t] -> __pet_test_0[-1 + t] : t >= 1 }'
     reference: __pet_ref_4
     read: 1
     write: 0
@@ -104,7 +104,7 @@ statements:
       name: f
   arguments:
   - type: access
-    relation: '[N] -> { S_3[t] -> __pet_test_0[o0] : o0 >= 0 and o0 <= -1 + t }'
+    relation: '[N] -> { S_3[t] -> __pet_test_0[-1 + t] : t >= 1 }'
     reference: __pet_ref_7
     read: 1
     write: 0
@@ -127,8 +127,7 @@ statements:
       write: 0
   arguments:
   - type: access
-    relation: '[N] -> { S_4[t] -> __pet_test_0[o0] : o0 >= 0 and o0 <= -1 + t; S_4[t]
-      -> __pet_test_0[t] }'
+    relation: '[N] -> { S_4[t] -> __pet_test_0[t] }'
     reference: __pet_ref_9
     read: 1
     write: 0
@@ -148,8 +147,8 @@ statements:
       name: f
   arguments:
   - type: access
-    relation: '[N] -> { S_5[t] -> __pet_test_1[o0] : N = 0 and o0 >= 1 and o0 <= -1
-      + t; S_5[t] -> __pet_test_1[0] : t >= 1 }'
+    relation: '[N] -> { S_5[t] -> __pet_test_1[-1 + t] : N = 0 and t >= 2; S_5[1]
+      -> __pet_test_1[0] }'
     reference: __pet_ref_12
     read: 1
     write: 0
@@ -172,8 +171,7 @@ statements:
       write: 0
   arguments:
   - type: access
-    relation: '[N] -> { S_6[t] -> __pet_test_1[o0] : N = 0 and o0 >= 1 and o0 <= t;
-      S_6[t] -> __pet_test_1[0] }'
+    relation: '[N] -> { S_6[t] -> __pet_test_1[t] }'
     reference: __pet_ref_14
     read: 1
     write: 0
@@ -196,8 +194,7 @@ statements:
       write: 0
   arguments:
   - type: access
-    relation: '[N] -> { S_7[t] -> __pet_test_1[o0] : o0 >= 1 and o0 <= t; S_7[t] ->
-      __pet_test_1[0] }'
+    relation: '[N] -> { S_7[t] -> __pet_test_1[t] }'
     reference: __pet_ref_17
     read: 1
     write: 0
@@ -217,12 +214,12 @@ statements:
       name: f
   arguments:
   - type: access
-    relation: '[N] -> { S_8[t] -> __pet_test_2[o0] : o0 >= 0 and o0 <= -1 + t }'
+    relation: '[N] -> { S_8[t] -> __pet_test_2[-1 + t] : t >= 1 }'
     reference: __pet_ref_20
     read: 1
     write: 0
   - type: access
-    relation: '[N] -> { S_8[t] -> __pet_test_3[o0] : o0 >= 0 and o0 <= -1 + t }'
+    relation: '[N] -> { S_8[t] -> __pet_test_3[-1 + t] : t >= 1 }'
     reference: __pet_ref_21
     read: 1
     write: 0
@@ -245,12 +242,12 @@ statements:
       write: 0
   arguments:
   - type: access
-    relation: '[N] -> { S_9[t] -> __pet_test_2[o0] : o0 >= 0 and o0 <= t }'
+    relation: '[N] -> { S_9[t] -> __pet_test_2[t] }'
     reference: __pet_ref_23
     read: 1
     write: 0
   - type: access
-    relation: '[N] -> { S_9[t] -> __pet_test_3[o0] : o0 >= 0 and o0 <= -1 + t }'
+    relation: '[N] -> { S_9[t] -> __pet_test_3[-1 + t] : t >= 1 }'
     reference: __pet_ref_24
     read: 1
     write: 0
@@ -270,12 +267,12 @@ statements:
       name: f
   arguments:
   - type: access
-    relation: '[N] -> { S_10[t] -> __pet_test_2[o0] : o0 >= 0 and o0 <= t }'
+    relation: '[N] -> { S_10[t] -> __pet_test_2[t] }'
     reference: __pet_ref_27
     read: 1
     write: 0
   - type: access
-    relation: '[N] -> { S_10[t] -> __pet_test_3[o0] : o0 >= 0 and o0 <= -1 + t }'
+    relation: '[N] -> { S_10[t] -> __pet_test_3[-1 + t] : t >= 1 }'
     reference: __pet_ref_28
     read: 1
     write: 0
@@ -298,13 +295,22 @@ statements:
       write: 0
   arguments:
   - type: access
-    relation: '[N] -> { S_11[t] -> __pet_test_2[o0] : o0 >= 0 and o0 <= t }'
+    relation: '[N] -> { S_11[t] -> __pet_test_2[t] }'
     reference: __pet_ref_30
     read: 1
     write: 0
   - type: access
-    relation: '[N] -> { S_11[t] -> __pet_test_3[o0] : o0 >= 0 and o0 <= -1 + t; S_11[t]
-      -> __pet_test_3[t] }'
+    relation: '[N] -> { S_11[t] -> __pet_test_3[t] }'
     reference: __pet_ref_31
     read: 1
     write: 0
+implications:
+- satisfied: 0
+  extension: '{ __pet_test_0[t] -> __pet_test_0[t''] : t'' <= t and t'' >= 0 }'
+- satisfied: 1
+  extension: '[N] -> { __pet_test_1[t] -> __pet_test_1[t''] : N = 0 and t'' <= t and
+    t'' >= 1; __pet_test_1[t] -> __pet_test_1[0] : t >= 0 }'
+- satisfied: 0
+  extension: '{ __pet_test_3[t] -> __pet_test_3[t''] : t'' <= t and t'' >= 0 }'
+- satisfied: 1
+  extension: '{ __pet_test_2[t] -> __pet_test_2[t''] : t'' <= t and t'' >= 0 }'
diff --git a/tests/while_inc.scop b/tests/while_inc.scop
index 94c59b7..e5592ed 100644
--- a/tests/while_inc.scop
+++ b/tests/while_inc.scop
@@ -61,7 +61,7 @@ statements:
         write: 0
   arguments:
   - type: access
-    relation: '{ S_1[t] -> __pet_test_0[o0] : o0 >= 0 and o0 <= -1 + t }'
+    relation: '{ S_1[t] -> __pet_test_0[-1 + t] : t >= 1 }'
     reference: __pet_ref_2
     read: 1
     write: 0
@@ -90,7 +90,7 @@ statements:
       write: 0
   arguments:
   - type: access
-    relation: '{ S_2[t] -> __pet_test_0[o0] : o0 >= 0 and o0 <= t }'
+    relation: '{ S_2[t] -> __pet_test_0[t] }'
     reference: __pet_ref_6
     read: 1
     write: 0
@@ -108,7 +108,10 @@ statements:
       write: 1
   arguments:
   - type: access
-    relation: '{ S_3[t] -> __pet_test_0[o0] : o0 >= 0 and o0 <= t }'
+    relation: '{ S_3[t] -> __pet_test_0[t] }'
     reference: __pet_ref_10
     read: 1
     write: 0
+implications:
+- satisfied: 1
+  extension: '{ __pet_test_0[t] -> __pet_test_0[t''] : t'' <= t and t'' >= 0 }'
diff --git a/tests/while_overflow.scop b/tests/while_overflow.scop
index ebab710..982ce60 100644
--- a/tests/while_overflow.scop
+++ b/tests/while_overflow.scop
@@ -46,7 +46,7 @@ statements:
       name: t
   arguments:
   - type: access
-    relation: '[N] -> { S_1[t] -> __pet_test_0[o0] : o0 >= 0 and o0 <= -1 + t }'
+    relation: '[N] -> { S_1[t] -> __pet_test_0[-1 + t] : t >= 1 }'
     reference: __pet_ref_2
     read: 1
     write: 0
@@ -78,7 +78,10 @@ statements:
         write: 0
   arguments:
   - type: access
-    relation: '[N] -> { S_2[t, i] -> __pet_test_0[o0] : o0 >= 0 and o0 <= t }'
+    relation: '[N] -> { S_2[t, i] -> __pet_test_0[t] }'
     reference: __pet_ref_4
     read: 1
     write: 0
+implications:
+- satisfied: 1
+  extension: '{ __pet_test_0[t] -> __pet_test_0[t''] : t'' <= t and t'' >= 0 }'
-- 
2.11.4.GIT