From 3aa8c11deebbbf1d8aee4480dd20b488e7795c06 Mon Sep 17 00:00:00 2001
From: Tristan Le Gall <tristan.le-gall@cea.fr>
Date: Fri, 23 Dec 2022 01:32:02 +0100
Subject: [PATCH] [alias] dune promote

---
 .../alias/tests/basic/oracle/test.res.oracle  |   2 +-
 .../real_world/oracle/example1.res.oracle     | 608 +++++++++++++++++-
 2 files changed, 608 insertions(+), 2 deletions(-)

diff --git a/src/plugins/alias/tests/basic/oracle/test.res.oracle b/src/plugins/alias/tests/basic/oracle/test.res.oracle
index a1861b053e4..eff48a5c96a 100644
--- a/src/plugins/alias/tests/basic/oracle/test.res.oracle
+++ b/src/plugins/alias/tests/basic/oracle/test.res.oracle
@@ -2,4 +2,4 @@
 [alias] Parsing done
 [alias] Functions done
 [alias] Analysis complete
-[]
+[]
\ No newline at end of file
diff --git a/src/plugins/alias/tests/real_world/oracle/example1.res.oracle b/src/plugins/alias/tests/real_world/oracle/example1.res.oracle
index d54d4f84126..11a6a2ae06d 100644
--- a/src/plugins/alias/tests/real_world/oracle/example1.res.oracle
+++ b/src/plugins/alias/tests/real_world/oracle/example1.res.oracle
@@ -6,6 +6,50 @@ List of edges:
 
 Pending: 
 
+LMap: 
+
+VMap: 
+
+
+Checking invariants
+List of vertices: 
+(id=0 LSet= { tmp })
+
+List of edges: 
+
+Pending: 
+(id=0 pending= {  })
+
+LMap: 
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { tmp })
+
+
+Checking invariants
+List of vertices: 
+(id=0 LSet= { tmp })
+(id=1 LSet= {  })
+(id=2 LSet= { x })
+
+List of edges: 
+(0 -> 1)
+
+Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+(id=2 pending= {  })
+
+LMap: 
+(lval=x -> id= 2)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { tmp })
+(id = 1 -> lset= {  })
+(id = 2 -> lset= { x })
+
 
 State before do_assignment tmp = x : List of vertices: 
 (id=0 LSet= { x; tmp })
@@ -18,6 +62,14 @@ Pending:
 (id=0 pending= {  })
 (id=1 pending= {  })
 
+LMap: 
+(lval=x -> id= 0)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { x; tmp })
+(id = 1 -> lset= {  })
+
 
 [alias] Skiping idata = (double *)malloc((unsigned long)10 * sizeof(double)); (doInstr not implemented)
 [alias] Skiping idata = (double *)malloc((unsigned long)10 * sizeof(double)); (doInstr not implemented)
@@ -29,6 +81,16 @@ List of edges:
 (0 -> 1)
 
 Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+
+LMap: 
+(lval=x -> id= 0)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { x; tmp })
+(id = 1 -> lset= {  })
 
 
 [alias] Skipping assignment idata = tmp->t2[*(tmp->n2)] (not implemented)
@@ -40,6 +102,16 @@ List of edges:
 (0 -> 1)
 
 Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+
+LMap: 
+(lval=x -> id= 0)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { x; tmp })
+(id = 1 -> lset= {  })
 
 
 [alias] Skipping assignment idata = tmp->t2[*(tmp->n2)] (not implemented)
@@ -51,6 +123,16 @@ List of edges:
 (0 -> 1)
 
 Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+
+LMap: 
+(lval=x -> id= 0)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { x; tmp })
+(id = 1 -> lset= {  })
 
 
 [alias] Skipping assignment odata = tmp->t1[*(tmp->n1)] (not implemented)
@@ -62,6 +144,16 @@ List of edges:
 (0 -> 1)
 
 Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+
+LMap: 
+(lval=x -> id= 0)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { x; tmp })
+(id = 1 -> lset= {  })
 
 
 [alias] Skipping assignment odata = tmp->t1[*(tmp->n1)] (not implemented)
@@ -73,6 +165,16 @@ List of edges:
 (0 -> 1)
 
 Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+
+LMap: 
+(lval=x -> id= 0)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { x; tmp })
+(id = 1 -> lset= {  })
 
 
 State before do_assignment idx = 0 : List of vertices: 
@@ -83,6 +185,16 @@ List of edges:
 (0 -> 1)
 
 Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+
+LMap: 
+(lval=x -> id= 0)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { x; tmp })
+(id = 1 -> lset= {  })
 
 
 [alias] Skiping tmp_1 = sin(*(idata + idx)); (doInstr not implemented)
@@ -95,6 +207,16 @@ List of edges:
 (0 -> 1)
 
 Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+
+LMap: 
+(lval=x -> id= 0)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { x; tmp })
+(id = 1 -> lset= {  })
 
 
 [alias] Skipping assignment *(odata + idx) = 0.5 * tmp_1 (not implemented)
@@ -106,6 +228,16 @@ List of edges:
 (0 -> 1)
 
 Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+
+LMap: 
+(lval=x -> id= 0)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { x; tmp })
+(id = 1 -> lset= {  })
 
 
 [alias] Skipping assignment *(odata + idx) = 0.5 * tmp_1 (not implemented)
@@ -117,6 +249,16 @@ List of edges:
 (0 -> 1)
 
 Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+
+LMap: 
+(lval=x -> id= 0)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { x; tmp })
+(id = 1 -> lset= {  })
 
 
 [alias] Skipping assignment idx = idx + 1 (not implemented)
@@ -128,6 +270,16 @@ List of edges:
 (0 -> 1)
 
 Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+
+LMap: 
+(lval=x -> id= 0)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { x; tmp })
+(id = 1 -> lset= {  })
 
 
 [alias] Skipping assignment idx = idx + 1 (not implemented)
@@ -139,6 +291,50 @@ List of edges:
 
 Pending: 
 
+LMap: 
+
+VMap: 
+
+
+Checking invariants
+List of vertices: 
+(id=0 LSet= { tmp })
+
+List of edges: 
+
+Pending: 
+(id=0 pending= {  })
+
+LMap: 
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { tmp })
+
+
+Checking invariants
+List of vertices: 
+(id=0 LSet= { tmp })
+(id=1 LSet= {  })
+(id=2 LSet= { x })
+
+List of edges: 
+(0 -> 1)
+
+Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+(id=2 pending= {  })
+
+LMap: 
+(lval=x -> id= 2)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { tmp })
+(id = 1 -> lset= {  })
+(id = 2 -> lset= { x })
+
 
 State before do_assignment tmp = x : List of vertices: 
 (id=0 LSet= { x; tmp })
@@ -151,6 +347,14 @@ Pending:
 (id=0 pending= {  })
 (id=1 pending= {  })
 
+LMap: 
+(lval=x -> id= 0)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { x; tmp })
+(id = 1 -> lset= {  })
+
 
 [alias] Skiping idata = (double *)malloc((unsigned long)10 * sizeof(double)); (doInstr not implemented)
 [alias] Skiping idata = (double *)malloc((unsigned long)10 * sizeof(double)); (doInstr not implemented)
@@ -162,6 +366,16 @@ List of edges:
 (0 -> 1)
 
 Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+
+LMap: 
+(lval=x -> id= 0)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { x; tmp })
+(id = 1 -> lset= {  })
 
 
 [alias] Skipping assignment idata = tmp->t1[*(tmp->n1)] (not implemented)
@@ -173,6 +387,16 @@ List of edges:
 (0 -> 1)
 
 Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+
+LMap: 
+(lval=x -> id= 0)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { x; tmp })
+(id = 1 -> lset= {  })
 
 
 [alias] Skipping assignment idata = tmp->t1[*(tmp->n1)] (not implemented)
@@ -184,6 +408,16 @@ List of edges:
 (0 -> 1)
 
 Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+
+LMap: 
+(lval=x -> id= 0)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { x; tmp })
+(id = 1 -> lset= {  })
 
 
 [alias] Skipping assignment odata = tmp->t2[*(tmp->n2)] (not implemented)
@@ -195,6 +429,16 @@ List of edges:
 (0 -> 1)
 
 Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+
+LMap: 
+(lval=x -> id= 0)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { x; tmp })
+(id = 1 -> lset= {  })
 
 
 [alias] Skipping assignment odata = tmp->t2[*(tmp->n2)] (not implemented)
@@ -206,6 +450,16 @@ List of edges:
 (0 -> 1)
 
 Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+
+LMap: 
+(lval=x -> id= 0)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { x; tmp })
+(id = 1 -> lset= {  })
 
 
 State before do_assignment idx = 0 : List of vertices: 
@@ -216,6 +470,16 @@ List of edges:
 (0 -> 1)
 
 Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+
+LMap: 
+(lval=x -> id= 0)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { x; tmp })
+(id = 1 -> lset= {  })
 
 
 State before do_assignment *(odata + idx) = (double)3 * *(idata + idx) + (double)1 : 
@@ -227,6 +491,16 @@ List of edges:
 (0 -> 1)
 
 Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+
+LMap: 
+(lval=x -> id= 0)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { x; tmp })
+(id = 1 -> lset= {  })
 
 
 [alias] Skipping assignment *(odata + idx) = (double)3 * *(idata + idx) + (double)1 (not implemented)
@@ -239,6 +513,16 @@ List of edges:
 (0 -> 1)
 
 Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+
+LMap: 
+(lval=x -> id= 0)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { x; tmp })
+(id = 1 -> lset= {  })
 
 
 [alias] Skipping assignment *(odata + idx) = (double)3 * *(idata + idx) + (double)1 (not implemented)
@@ -250,6 +534,16 @@ List of edges:
 (0 -> 1)
 
 Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+
+LMap: 
+(lval=x -> id= 0)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { x; tmp })
+(id = 1 -> lset= {  })
 
 
 [alias] Skipping assignment idx = idx + 1 (not implemented)
@@ -261,6 +555,16 @@ List of edges:
 (0 -> 1)
 
 Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+
+LMap: 
+(lval=x -> id= 0)
+(lval=tmp -> id= 0)
+
+VMap: 
+(id = 0 -> lset= { x; tmp })
+(id = 1 -> lset= {  })
 
 
 [alias] Skipping assignment idx = idx + 1 (not implemented)
@@ -276,6 +580,10 @@ List of edges:
 
 Pending: 
 
+LMap: 
+
+VMap: 
+
 
 State before do_assignment i = 0 : List of vertices: 
 
@@ -283,6 +591,10 @@ List of edges:
 
 Pending: 
 
+LMap: 
+
+VMap: 
+
 
 [alias] Skiping a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double)); (doInstr not implemented)
 [alias] Skiping a->t1[i] = (double *)malloc((unsigned long)10 * sizeof(double)); (doInstr not implemented)
@@ -294,6 +606,10 @@ List of edges:
 
 Pending: 
 
+LMap: 
+
+VMap: 
+
 
 [alias] Skipping assignment i = i + 1 (not implemented)
 State before do_assignment i = i + 1 : List of vertices: 
@@ -302,6 +618,10 @@ List of edges:
 
 Pending: 
 
+LMap: 
+
+VMap: 
+
 
 [alias] Skipping assignment i = i + 1 (not implemented)
 [alias] Skiping a->n1 = (int *)malloc(sizeof(int)); (doInstr not implemented)
@@ -314,6 +634,29 @@ List of edges:
 
 Pending: 
 
+LMap: 
+
+VMap: 
+
+
+Checking invariants
+List of vertices: 
+(id=0 LSet= {  })
+(id=1 LSet= { a->n1 })
+
+List of edges: 
+
+Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+
+LMap: 
+(lval=a->n1 -> id= 1)
+
+VMap: 
+(id = 0 -> lset= {  })
+(id = 1 -> lset= { a->n1 })
+
 
 State before do_assignment *(a->n1) = 1 : List of vertices: 
 (id=0 LSet= {  })
@@ -326,6 +669,13 @@ Pending:
 (id=0 pending= {  })
 (id=1 pending= {  })
 
+LMap: 
+(lval=a->n1 -> id= 1)
+
+VMap: 
+(id = 0 -> lset= {  })
+(id = 1 -> lset= { a->n1 })
+
 
 State before do_assignment *(a->n2) = 1 : List of vertices: 
 (id=0 LSet= {  })
@@ -340,6 +690,44 @@ Pending:
 (id=1 pending= {  })
 (id=2 pending= { 2 })
 
+LMap: 
+(lval=a->n1 -> id= 1)
+
+VMap: 
+(id = 0 -> lset= {  })
+(id = 1 -> lset= { a->n1 })
+(id = 2 -> lset= {  })
+
+
+Checking invariants
+List of vertices: 
+(id=0 LSet= {  })
+(id=1 LSet= { a->n1 })
+(id=2 LSet= {  })
+(id=3 LSet= {  })
+(id=4 LSet= { a->n2 })
+
+List of edges: 
+(1 -> 0)
+
+Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+(id=2 pending= { 2 })
+(id=3 pending= {  })
+(id=4 pending= {  })
+
+LMap: 
+(lval=a->n1 -> id= 1)
+(lval=a->n2 -> id= 4)
+
+VMap: 
+(id = 0 -> lset= {  })
+(id = 1 -> lset= { a->n1 })
+(id = 2 -> lset= {  })
+(id = 3 -> lset= {  })
+(id = 4 -> lset= { a->n2 })
+
 
 State before do_assignment *(a->n2) = 1 : List of vertices: 
 (id=0 LSet= {  })
@@ -359,6 +747,17 @@ Pending:
 (id=3 pending= {  })
 (id=4 pending= {  })
 
+LMap: 
+(lval=a->n1 -> id= 1)
+(lval=a->n2 -> id= 4)
+
+VMap: 
+(id = 0 -> lset= {  })
+(id = 1 -> lset= { a->n1 })
+(id = 2 -> lset= {  })
+(id = 3 -> lset= {  })
+(id = 4 -> lset= { a->n2 })
+
 
 State before do_assignment i = 0 : List of vertices: 
 (id=0 LSet= {  })
@@ -380,6 +779,18 @@ Pending:
 (id=4 pending= {  })
 (id=5 pending= { 5 })
 
+LMap: 
+(lval=a->n1 -> id= 1)
+(lval=a->n2 -> id= 4)
+
+VMap: 
+(id = 0 -> lset= {  })
+(id = 1 -> lset= { a->n1 })
+(id = 2 -> lset= {  })
+(id = 3 -> lset= {  })
+(id = 4 -> lset= { a->n2 })
+(id = 5 -> lset= {  })
+
 
 State before do_assignment i = 0 : List of vertices: 
 (id=0 LSet= {  })
@@ -401,6 +812,18 @@ Pending:
 (id=4 pending= {  })
 (id=5 pending= { 5 })
 
+LMap: 
+(lval=a->n1 -> id= 1)
+(lval=a->n2 -> id= 4)
+
+VMap: 
+(id = 0 -> lset= {  })
+(id = 1 -> lset= { a->n1 })
+(id = 2 -> lset= {  })
+(id = 3 -> lset= {  })
+(id = 4 -> lset= { a->n2 })
+(id = 5 -> lset= {  })
+
 
 State before do_assignment b->t1[i] = a->t1[i] : List of vertices: 
 (id=0 LSet= {  })
@@ -422,6 +845,18 @@ Pending:
 (id=4 pending= {  })
 (id=5 pending= { 5 })
 
+LMap: 
+(lval=a->n1 -> id= 1)
+(lval=a->n2 -> id= 4)
+
+VMap: 
+(id = 0 -> lset= {  })
+(id = 1 -> lset= { a->n1 })
+(id = 2 -> lset= {  })
+(id = 3 -> lset= {  })
+(id = 4 -> lset= { a->n2 })
+(id = 5 -> lset= {  })
+
 
 [alias] Skipping assignment b->t1[i] = a->t1[i] (not implemented)
 State before do_assignment b->t1[i] = a->t1[i] : List of vertices: 
@@ -444,6 +879,18 @@ Pending:
 (id=4 pending= {  })
 (id=5 pending= { 5 })
 
+LMap: 
+(lval=a->n1 -> id= 1)
+(lval=a->n2 -> id= 4)
+
+VMap: 
+(id = 0 -> lset= {  })
+(id = 1 -> lset= { a->n1 })
+(id = 2 -> lset= {  })
+(id = 3 -> lset= {  })
+(id = 4 -> lset= { a->n2 })
+(id = 5 -> lset= {  })
+
 
 [alias] Skipping assignment b->t1[i] = a->t1[i] (not implemented)
 State before do_assignment b->t2[i] = a->t2[i] : List of vertices: 
@@ -466,6 +913,18 @@ Pending:
 (id=4 pending= {  })
 (id=5 pending= { 5 })
 
+LMap: 
+(lval=a->n1 -> id= 1)
+(lval=a->n2 -> id= 4)
+
+VMap: 
+(id = 0 -> lset= {  })
+(id = 1 -> lset= { a->n1 })
+(id = 2 -> lset= {  })
+(id = 3 -> lset= {  })
+(id = 4 -> lset= { a->n2 })
+(id = 5 -> lset= {  })
+
 
 [alias] Skipping assignment b->t2[i] = a->t2[i] (not implemented)
 State before do_assignment b->t2[i] = a->t2[i] : List of vertices: 
@@ -488,6 +947,18 @@ Pending:
 (id=4 pending= {  })
 (id=5 pending= { 5 })
 
+LMap: 
+(lval=a->n1 -> id= 1)
+(lval=a->n2 -> id= 4)
+
+VMap: 
+(id = 0 -> lset= {  })
+(id = 1 -> lset= { a->n1 })
+(id = 2 -> lset= {  })
+(id = 3 -> lset= {  })
+(id = 4 -> lset= { a->n2 })
+(id = 5 -> lset= {  })
+
 
 [alias] Skipping assignment b->t2[i] = a->t2[i] (not implemented)
 State before do_assignment i = i + 1 : List of vertices: 
@@ -510,6 +981,18 @@ Pending:
 (id=4 pending= {  })
 (id=5 pending= { 5 })
 
+LMap: 
+(lval=a->n1 -> id= 1)
+(lval=a->n2 -> id= 4)
+
+VMap: 
+(id = 0 -> lset= {  })
+(id = 1 -> lset= { a->n1 })
+(id = 2 -> lset= {  })
+(id = 3 -> lset= {  })
+(id = 4 -> lset= { a->n2 })
+(id = 5 -> lset= {  })
+
 
 [alias] Skipping assignment i = i + 1 (not implemented)
 State before do_assignment i = i + 1 : List of vertices: 
@@ -532,6 +1015,18 @@ Pending:
 (id=4 pending= {  })
 (id=5 pending= { 5 })
 
+LMap: 
+(lval=a->n1 -> id= 1)
+(lval=a->n2 -> id= 4)
+
+VMap: 
+(id = 0 -> lset= {  })
+(id = 1 -> lset= { a->n1 })
+(id = 2 -> lset= {  })
+(id = 3 -> lset= {  })
+(id = 4 -> lset= { a->n2 })
+(id = 5 -> lset= {  })
+
 
 [alias] Skipping assignment i = i + 1 (not implemented)
 State before do_assignment b->n1 = a->n1 : List of vertices: 
@@ -554,6 +1049,18 @@ Pending:
 (id=4 pending= {  })
 (id=5 pending= { 5 })
 
+LMap: 
+(lval=a->n1 -> id= 1)
+(lval=a->n2 -> id= 4)
+
+VMap: 
+(id = 0 -> lset= {  })
+(id = 1 -> lset= { a->n1 })
+(id = 2 -> lset= {  })
+(id = 3 -> lset= {  })
+(id = 4 -> lset= { a->n2 })
+(id = 5 -> lset= {  })
+
 
 [alias] Skipping assignment b->n1 = a->n1 (not implemented)
 State before do_assignment b->n1 = a->n1 : List of vertices: 
@@ -576,6 +1083,18 @@ Pending:
 (id=4 pending= {  })
 (id=5 pending= { 5 })
 
+LMap: 
+(lval=a->n1 -> id= 1)
+(lval=a->n2 -> id= 4)
+
+VMap: 
+(id = 0 -> lset= {  })
+(id = 1 -> lset= { a->n1 })
+(id = 2 -> lset= {  })
+(id = 3 -> lset= {  })
+(id = 4 -> lset= { a->n2 })
+(id = 5 -> lset= {  })
+
 
 [alias] Skipping assignment b->n1 = a->n1 (not implemented)
 State before do_assignment b->n2 = a->n2 : List of vertices: 
@@ -598,6 +1117,18 @@ Pending:
 (id=4 pending= {  })
 (id=5 pending= { 5 })
 
+LMap: 
+(lval=a->n1 -> id= 1)
+(lval=a->n2 -> id= 4)
+
+VMap: 
+(id = 0 -> lset= {  })
+(id = 1 -> lset= { a->n1 })
+(id = 2 -> lset= {  })
+(id = 3 -> lset= {  })
+(id = 4 -> lset= { a->n2 })
+(id = 5 -> lset= {  })
+
 
 [alias] Skipping assignment b->n2 = a->n2 (not implemented)
 State before do_assignment b->n2 = a->n2 : List of vertices: 
@@ -620,6 +1151,18 @@ Pending:
 (id=4 pending= {  })
 (id=5 pending= { 5 })
 
+LMap: 
+(lval=a->n1 -> id= 1)
+(lval=a->n2 -> id= 4)
+
+VMap: 
+(id = 0 -> lset= {  })
+(id = 1 -> lset= { a->n1 })
+(id = 2 -> lset= {  })
+(id = 3 -> lset= {  })
+(id = 4 -> lset= { a->n2 })
+(id = 5 -> lset= {  })
+
 
 [alias] Skipping assignment b->n2 = a->n2 (not implemented)
 [alias] Skiping f1(a); (doInstr not implemented)
@@ -646,6 +1189,18 @@ Pending:
 (id=4 pending= {  })
 (id=5 pending= { 5 })
 
+LMap: 
+(lval=a->n1 -> id= 1)
+(lval=a->n2 -> id= 4)
+
+VMap: 
+(id = 0 -> lset= {  })
+(id = 1 -> lset= { a->n1 })
+(id = 2 -> lset= {  })
+(id = 3 -> lset= {  })
+(id = 4 -> lset= { a->n2 })
+(id = 5 -> lset= {  })
+
 
 State before do_assignment __retres = 0 : List of vertices: 
 (id=0 LSet= {  })
@@ -667,6 +1222,18 @@ Pending:
 (id=4 pending= {  })
 (id=5 pending= { 5 })
 
+LMap: 
+(lval=a->n1 -> id= 1)
+(lval=a->n2 -> id= 4)
+
+VMap: 
+(id = 0 -> lset= {  })
+(id = 1 -> lset= { a->n1 })
+(id = 2 -> lset= {  })
+(id = 3 -> lset= {  })
+(id = 4 -> lset= { a->n2 })
+(id = 5 -> lset= {  })
+
 
 State before do_assignment *n = 0 : List of vertices: 
 
@@ -674,6 +1241,29 @@ List of edges:
 
 Pending: 
 
+LMap: 
+
+VMap: 
+
+
+Checking invariants
+List of vertices: 
+(id=0 LSet= {  })
+(id=1 LSet= { n })
+
+List of edges: 
+
+Pending: 
+(id=0 pending= {  })
+(id=1 pending= {  })
+
+LMap: 
+(lval=n -> id= 1)
+
+VMap: 
+(id = 0 -> lset= {  })
+(id = 1 -> lset= { n })
+
 
 State before do_assignment *n = 0 : List of vertices: 
 (id=0 LSet= {  })
@@ -688,6 +1278,14 @@ Pending:
 (id=1 pending= {  })
 (id=2 pending= {  })
 
+LMap: 
+(lval=n -> id= 1)
+
+VMap: 
+(id = 0 -> lset= {  })
+(id = 1 -> lset= { n })
+(id = 2 -> lset= {  })
+
 
 State before do_assignment *n = *n + 1 : List of vertices: 
 
@@ -695,6 +1293,10 @@ List of edges:
 
 Pending: 
 
+LMap: 
+
+VMap: 
+
 
 [alias] Skipping assignment *n = *n + 1 (not implemented)
 State before do_assignment *n = *n + 1 : List of vertices: 
@@ -703,6 +1305,10 @@ List of edges:
 
 Pending: 
 
+LMap: 
+
+VMap: 
+
 
 [alias] Skipping assignment *n = *n + 1 (not implemented)
 [alias] Functions done
@@ -991,4 +1597,4 @@ Pending:
 <end of list>
 )
 [alias] Analysis complete
-]
+]
\ No newline at end of file
-- 
GitLab