diff --git a/.gitignore b/.gitignore
index f3f1f0fb0bc7a31a3cd656e4da33bf7c06dc982d..9b8d90084d3fc163310e33706f727aa6459849c7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -39,7 +39,7 @@ farith/
 
 # debug files
 *debug_graph.tmp/
-*debug_diffgraph.tmp/
+*debug_wegraph.tmp/
 
 # mac artifacts
 
diff --git a/colibri2/tests/solve/smt_array/sat/dune b/colibri2/tests/solve/smt_array/sat/dune
index 6961407484c34044d304a32c6d47398de1775bd2..82d1ec51e6fa435d1814b311ae3d74cf4ab66c5d 100644
--- a/colibri2/tests/solve/smt_array/sat/dune
+++ b/colibri2/tests/solve/smt_array/sat/dune
@@ -17,7 +17,7 @@
     --options
     "array-res-ext array-res-aup"
     --options
-    "array-diff-graph"
+    "array-wegraph"
     --options
     "array-choice"
     --options
@@ -25,11 +25,11 @@
     --options
     "array-res-ext array-res-aup array-choice"
     --options
-    "array-diff-graph array-choice"
+    "array-wegraph array-choice"
     ;--options
-    ;"array-diff-graph array-res-ext"
+    ;"array-wegraph array-res-ext"
     ;--options
-    ;"array-diff-graph array-res-ext array-res-aup"
+    ;"array-wegraph array-res-ext array-res-aup"
     .
     sat)))
  (mode promote))
diff --git a/colibri2/tests/solve/smt_array/sat/dune.inc b/colibri2/tests/solve/smt_array/sat/dune.inc
index 19710c39dd36a5b2294b1b736b3bf1b04e22d111..11608400050c9ef6bf31d91e172f73909d0dccdc 100644
--- a/colibri2/tests/solve/smt_array/sat/dune.inc
+++ b/colibri2/tests/solve/smt_array/sat/dune.inc
@@ -25,15 +25,15 @@
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --check-status sat 
 --dont-print-result %{dep:test1.smt2})) (package colibri2))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status sat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status sat 
 --dont-print-result %{dep:imp1.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status sat --learning --dont-print-result %{dep:imp1.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status sat --learning --dont-print-result %{dep:imp1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status sat 
 --dont-print-result %{dep:neq.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status sat 
 --dont-print-result %{dep:test1.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat 
 --dont-print-result %{dep:imp1.smt2})) (package colibri2))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat --learning --dont-print-result %{dep:imp1.smt2})) (package colibri2))
@@ -61,12 +61,12 @@
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat 
 --dont-print-result %{dep:test1.smt2})) (package colibri2))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status sat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status sat 
 --dont-print-result %{dep:imp1.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status sat --learning --dont-print-result %{dep:imp1.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status sat --learning --dont-print-result %{dep:imp1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status sat 
 --dont-print-result %{dep:neq.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status sat 
 --dont-print-result %{dep:test1.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
diff --git a/colibri2/tests/solve/smt_array/unsat/dune b/colibri2/tests/solve/smt_array/unsat/dune
index 5227ff747b452c43da9bab2f09c32b7226c975a7..198aca159e03da738c846942069af64a0e85af62 100644
--- a/colibri2/tests/solve/smt_array/unsat/dune
+++ b/colibri2/tests/solve/smt_array/unsat/dune
@@ -17,7 +17,7 @@
     --options
     "array-res-ext array-res-aup"
     --options
-    "array-diff-graph"
+    "array-wegraph"
     --options
     "array-choice"
     --options
@@ -25,11 +25,11 @@
     --options
     "array-res-ext array-res-aup array-choice"
     --options
-    "array-diff-graph array-choice"
+    "array-wegraph array-choice"
     ;--options
-    ;"array-diff-graph array-res-ext"
+    ;"array-wegraph array-res-ext"
     ;--options
-    ;"array-diff-graph array-res-ext array-res-aup"
+    ;"array-wegraph array-res-ext array-res-aup"
     .
     unsat)))
  (mode promote))
diff --git a/colibri2/tests/solve/smt_array/unsat/dune.inc b/colibri2/tests/solve/smt_array/unsat/dune.inc
index 3924334bbb63002b8d4dd542c6c82e2339ee3502..6ee77bbf3ed800f8dbff39873dead8c76746c7ae 100644
--- a/colibri2/tests/solve/smt_array/unsat/dune.inc
+++ b/colibri2/tests/solve/smt_array/unsat/dune.inc
@@ -133,51 +133,51 @@
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --check-status unsat 
 --dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --check-status unsat --learning --dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat 
 --dont-print-result %{dep:distinct.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat --learning --dont-print-result %{dep:distinct.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat --learning --dont-print-result %{dep:distinct.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat 
 --dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat 
 --dont-print-result %{dep:eq2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat --learning --dont-print-result %{dep:eq2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat --learning --dont-print-result %{dep:eq2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat 
 --dont-print-result %{dep:eq3.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat --learning --dont-print-result %{dep:eq3.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat --learning --dont-print-result %{dep:eq3.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat 
 --dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat --learning --dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat --learning --dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat 
 --dont-print-result %{dep:eq4.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat --learning --dont-print-result %{dep:eq4.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat --learning --dont-print-result %{dep:eq4.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat 
 --dont-print-result %{dep:impls1.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat --learning --dont-print-result %{dep:impls1.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat --learning --dont-print-result %{dep:impls1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat 
 --dont-print-result %{dep:impls2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat --learning --dont-print-result %{dep:impls2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat --learning --dont-print-result %{dep:impls2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat 
 --dont-print-result %{dep:impls3.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat --learning --dont-print-result %{dep:impls3.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat --learning --dont-print-result %{dep:impls3.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat 
 --dont-print-result %{dep:impls4.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat --learning --dont-print-result %{dep:impls4.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat --learning --dont-print-result %{dep:impls4.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat 
 --dont-print-result %{dep:impls5.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat --learning --dont-print-result %{dep:impls5.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat --learning --dont-print-result %{dep:impls5.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat 
 --dont-print-result %{dep:impls6.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat --learning --dont-print-result %{dep:impls6.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat --learning --dont-print-result %{dep:impls6.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat 
 --dont-print-result %{dep:select.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat --learning --dont-print-result %{dep:select.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat --learning --dont-print-result %{dep:select.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat 
 --dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat --learning --dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat --learning --dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat 
 --dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --check-status unsat --learning --dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat --learning --dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat 
 --dont-print-result %{dep:distinct.smt2})) (package colibri2))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:distinct.smt2})) (package colibri2))
@@ -313,48 +313,48 @@
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat 
 --dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat 
 --dont-print-result %{dep:distinct.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:distinct.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:distinct.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat 
 --dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat 
 --dont-print-result %{dep:eq2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:eq2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:eq2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat 
 --dont-print-result %{dep:eq3.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:eq3.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:eq3.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat 
 --dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat 
 --dont-print-result %{dep:eq4.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:eq4.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:eq4.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat 
 --dont-print-result %{dep:impls1.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls1.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat 
 --dont-print-result %{dep:impls2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat 
 --dont-print-result %{dep:impls3.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls3.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls3.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat 
 --dont-print-result %{dep:impls4.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls4.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls4.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat 
 --dont-print-result %{dep:impls5.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls5.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls5.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat 
 --dont-print-result %{dep:impls6.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls6.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:impls6.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat 
 --dont-print-result %{dep:select.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:select.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:select.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat 
 --dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat 
 --dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-diff-graph --array-choice --check-status unsat --learning --dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
diff --git a/colibri2/theories/array/GE_Array_DP.ml b/colibri2/theories/array/RWRules.ml
similarity index 98%
rename from colibri2/theories/array/GE_Array_DP.ml
rename to colibri2/theories/array/RWRules.ml
index d0d02e9f3d9658fe0f6f0d7ffbd892f254ef7315..9ec6a1bc206ce0b1c85d37f3d9c9c587d53aa68f 100644
--- a/colibri2/theories/array/GE_Array_DP.ml
+++ b/colibri2/theories/array/RWRules.ml
@@ -183,7 +183,7 @@ let apply_res_ext_1_2_aux env ind_gty val_gty l tyvt =
   let rec aux (tnl : (Expr.term * int) list) =
     match tnl with
     | (nterm, idn) :: t -> (
-        match DiffGraph.DG.find_opt env idn with
+        match WEGraph.WEG.find_opt env idn with
         | Some (_, m) ->
             let nterms =
               List.fold_left
@@ -204,7 +204,7 @@ let apply_res_ext_1_2_aux env ind_gty val_gty l tyvt =
         let anvt = Expr.Term.of_var anv in
         ( cnt + 1,
           (anv, node) :: tsubst,
-          (anvt, DiffGraph.Id_dom.get_id env node) :: tns ))
+          (anvt, WEGraph.Id_dom.get_id env node) :: tns ))
       (0, [], []) l
   in
   let tysubst = [ (STV.ind_ty_var, ind_gty); (STV.val_ty_var, val_gty) ] in
@@ -237,13 +237,13 @@ let apply_res_ext_1_1, apply_res_ext_1_2 =
 
 (** given a new foreign array and a set of all the other foreign arrays,
     applies res-ext-2 on the new foreign array and all the other foregin arrays
-    which are its neighbours in the DiffGraph *)
+    which are its neighbours in the WEGraph *)
 let get_foreign_neighbours env a arr_set =
-  let aid = DiffGraph.Id_dom.get_id env a in
-  let nps = DiffGraph.get_neighbours env aid in
+  let aid = WEGraph.Id_dom.get_id env a in
+  let nps = WEGraph.get_neighbours env aid in
   Node.S.fold
     (fun node acc ->
-      if DInt.S.mem (DiffGraph.Id_dom.get_id env node) nps then
+      if DInt.S.mem (WEGraph.Id_dom.get_id env node) nps then
         Node.S.add node acc
       else acc)
     arr_set Node.S.empty
@@ -262,7 +262,7 @@ let apply_res_ext_2_1, apply_res_ext_2_2 =
     if choice then
       Choice.register_global env
         {
-          Choice.print_cho = "Decision from DiffGraph_merge_neighbours.";
+          Choice.print_cho = "Decision from WEGraph_merge_neighbours.";
           Choice.prio = 1;
           choice =
             (fun env ->
diff --git a/colibri2/theories/array/GE_Array_DP.mli b/colibri2/theories/array/RWRules.mli
similarity index 100%
rename from colibri2/theories/array/GE_Array_DP.mli
rename to colibri2/theories/array/RWRules.mli
diff --git a/colibri2/theories/array/DiffGraph.ml b/colibri2/theories/array/WEGraph.ml
similarity index 87%
rename from colibri2/theories/array/DiffGraph.ml
rename to colibri2/theories/array/WEGraph.ml
index 184099176c442b977a4d754409537f8117de2d43..cc0538e12bb135d7426de65b8e27f4bf7ddd9bc3 100644
--- a/colibri2/theories/array/DiffGraph.ml
+++ b/colibri2/theories/array/WEGraph.ml
@@ -29,14 +29,14 @@ module EHT = MkIHT (struct
   type t = Node.t
 
   let pp = Node.pp
-  let name = "diffgraph_edges"
+  let name = "wegraph_edges"
 end)
 
 module VHT = MkIHT (struct
   type t = Node.t
 
   let pp = Node.pp
-  let name = "diffgraph_indices"
+  let name = "wegraph_indices"
 end)
 
 module Vertex = struct
@@ -66,23 +66,23 @@ module Vertices = MkIHT (struct
   let name = "index_vertices"
 end)
 
-module DG = struct
+module WEG = struct
   include MkIHT (struct
     type t = DInt.S.t DInt.M.t * DInt.t DInt.M.t
 
     let pp fmt (m, (_ : DInt.t DInt.M.t)) = DInt.M.pp DInt.S.pp fmt m
-    let name = "diffgraph_nodes"
+    let name = "wegraph_nodes"
   end)
 
-  let diffgraph_opt =
-    Debug.register_flag ~desc:"Print the entire DiffGraph into a dot file"
-      "diffgraph"
+  let wegraph_opt =
+    Debug.register_flag ~desc:"Print the entire WEGraph into a dot file"
+      "wegraph"
 
-  let pp_dot_diffgraph =
+  let pp_dot_wegraph =
     let cnt = ref 0 in
-    let dir = "debug_diffgraph.tmp" in
+    let dir = "debug_wegraph.tmp" in
     let fname () =
-      Fmt.str "%s/diffgraph_%d.dot" dir
+      Fmt.str "%s/wegraph_%d.dot" dir
         (incr cnt;
          !cnt)
     in
@@ -142,7 +142,7 @@ module DG = struct
       aux (fold (fun id (_, m) acc -> DInt.M.add id m acc) env DInt.M.empty)
     in
     fun env ?msg () ->
-      if Debug.test_flag diffgraph_opt then (
+      if Debug.test_flag wegraph_opt then (
         if not (Sys.file_exists dir) then Unix.mkdir dir 0o700;
         let oc = open_out (fname ()) in
         let foc = Format.formatter_of_out_channel oc in
@@ -169,7 +169,7 @@ module Id_dom = struct
 
   let new_id_hook env id n b =
     if b then (
-      DG.set env id (DInt.M.empty, DInt.M.empty);
+      WEG.set env id (DInt.M.empty, DInt.M.empty);
       EHT.set env id n)
 
   let set_id env n = set_id ~new_id_hook env n
@@ -216,23 +216,23 @@ let are_linked env id1 id2 =
         if b then (seen, b)
         else if id = id2 then (seen, true)
         else if DInt.S.mem id seen then (seen, false)
-        else aux (DInt.S.add id seen) (snd (DG.find env id)))
+        else aux (DInt.S.add id seen) (snd (WEG.find env id)))
       m (seen, false)
   in
-  match DG.find_opt env id1 with
+  match WEG.find_opt env id1 with
   | None -> false
   | Some (_, m) -> snd (aux (DInt.S.singleton id1) m)
 
 let are_neighbours env id1 id2 =
-  match DG.find_opt env id1 with
+  match WEG.find_opt env id1 with
   | None -> false
   | Some (_, m) -> DInt.M.mem id2 m
 
 let add_neighbour env (srcid, srcn) (destid, destn) ind ind_gty val_gty =
   let iid = Index_Id_dom.get_id env ind in
-  Debug.dprintf6 debug "DiffGraph: add_neighbour %a to %a through %a"
-    (pp_eid env) srcid (pp_eid env) destid (pp_vid env) iid;
-  DG.change env destid ~f:(function
+  Debug.dprintf6 debug "WEGraph: add_neighbour %a to %a through %a" (pp_eid env)
+    srcid (pp_eid env) destid (pp_vid env) iid;
+  WEG.change env destid ~f:(function
     | None ->
         Some
           ( DInt.M.singleton iid (DInt.S.singleton srcid),
@@ -286,7 +286,7 @@ let add_neighbour env (srcid, srcn) (destid, destn) ind ind_gty val_gty =
                           }
                       else Boolean.set_true env disj;
                       Debug.dprintf10 debug
-                        "DiffGraph: adding %a as a neighbour to %a through %a: \
+                        "WEGraph: adding %a as a neighbour to %a through %a: \
                          setting %a = %a to true"
                         Node.pp srcn Node.pp destn Node.pp ind Node.pp ind
                         Node.pp ind');
@@ -316,9 +316,9 @@ let empty_neighbour_set kn rn k =
 
 let rm_neighbour env (kid, knode) (rid, rnode) iid =
   let ind = VHT.find env iid in
-  Debug.dprintf6 debug "DiffGraph: rm_neighbour %a of %a through %a"
-    (pp_eid env) rid (pp_eid env) kid (pp_vid env) iid;
-  DG.change env kid ~f:(function
+  Debug.dprintf6 debug "WEGraph: rm_neighbour %a of %a through %a" (pp_eid env)
+    rid (pp_eid env) kid (pp_vid env) iid;
+  WEG.change env kid ~f:(function
     | None -> empty_neighbour_set knode rnode ind
     | Some (m1, m2) ->
         let nm1 =
@@ -335,7 +335,7 @@ let rm_neighbour env (kid, knode) (rid, rnode) iid =
               | Some iid' ->
                   let ind' = VHT.find env iid' in
                   Debug.dprintf4 debug
-                    "DiffGraph: rm_neighbour found %a (should be equal to %a)"
+                    "WEGraph: rm_neighbour found %a (should be equal to %a)"
                     (pp_vid env) iid' (pp_vid env) iid;
                   assert (Egraph.is_equal env ind ind');
                   None
@@ -345,7 +345,7 @@ let rm_neighbour env (kid, knode) (rid, rnode) iid =
         Some (nm1, nm2))
 
 let get_k_neighbours env np iid =
-  match DG.find_opt env np with
+  match WEG.find_opt env np with
   | None -> DInt.S.empty
   | Some (m, _) -> (
       match DInt.M.find_opt iid m with None -> DInt.S.empty | Some s -> s)
@@ -354,7 +354,7 @@ let add_edge env aid bid iid =
   (* when adding a node dest as a neighbour to a node src, dest is also added
      as a neighbour to all the nodes in the complete graph formed by all the
      array nodes which differ on the same index k. *)
-  Debug.dprintf6 debug "DiffGraph: adding the edge %a between %a and %a"
+  Debug.dprintf6 debug "WEGraph: adding the edge %a between %a and %a"
     (pp_vid env) iid (pp_eid env) aid (pp_eid env) bid;
   if aid <> bid then
     let ind_gty, val_gty =
@@ -379,8 +379,8 @@ let add_edge env aid bid iid =
       ank
 
 let rm_edge env aid bid iid =
-  Debug.dprintf6 debug "DiffGraph: rm_edge %a between %a and %a" (pp_vid env)
-    iid (pp_eid env) aid (pp_eid env) bid;
+  Debug.dprintf6 debug "WEGraph: rm_edge %a between %a and %a" (pp_vid env) iid
+    (pp_eid env) aid (pp_eid env) bid;
   if aid <> bid then (
     let an = EHT.find env aid in
     let bn = EHT.find env bid in
@@ -392,8 +392,8 @@ let rm_edge env aid bid iid =
 
 let add_edge_aux knp rnode env aid bid iid =
   add_edge env aid bid iid;
-  if Debug.test_flag DG.diffgraph_opt then
-    DG.pp_dot_diffgraph
+  if Debug.test_flag WEG.wegraph_opt then
+    WEG.pp_dot_wegraph
       ~msg:
         (Fmt.str
            "_merge_neighbours %a to %a\\n add edge between %a and %a with %a"
@@ -403,8 +403,8 @@ let add_edge_aux knp rnode env aid bid iid =
 
 let rm_edge_aux env aid bid iid =
   rm_edge env aid bid iid;
-  if Debug.test_flag DG.diffgraph_opt then
-    DG.pp_dot_diffgraph
+  if Debug.test_flag WEG.wegraph_opt then
+    WEG.pp_dot_wegraph
       ~msg:
         (Fmt.str
            "_merge_neighbours %a -> %a\\n rm_edge between %a and %a linked \
@@ -419,8 +419,8 @@ let merge_neigbours_aux env (kn, kid) (rn, rid) nid kk_opt kr_opt () =
       let ind1 = VHT.find env iid1 in
       let ind2 = VHT.find env iid2 in
       Debug.dprintf6 debug
-        "DiffGraph: _merge_neigbours_aux: iter1: found the neighbour %a \
-         through %a and %a"
+        "WEGraph: _merge_neigbours_aux: iter1: found the neighbour %a through \
+         %a and %a"
         (pp_eid env) nid (pp_vid env) iid1 (pp_vid env) iid2;
       (* if a node X is a neighbour of both A and B through the edges
          ind1 and ind2 (resp.) then (ind1 = ind2) must be set to true, and
@@ -435,7 +435,7 @@ let merge_neigbours_aux env (kn, kid) (rn, rid) nid kk_opt kr_opt () =
         if Options.get env use_choice then
           Choice.register_global env
             {
-              Choice.print_cho = "Decision from DiffGraph_merge_neighbours.";
+              Choice.print_cho = "Decision from WEGraph_merge_neighbours.";
               Choice.prio = 1;
               choice =
                 (fun env ->
@@ -453,19 +453,19 @@ let merge_neigbours_aux env (kn, kid) (rn, rid) nid kk_opt kr_opt () =
       rm_edge_aux env nid rid iid2
   | None, Some iid ->
       Debug.dprintf4 debug
-        "DiffGraph: _merge_neigbours_aux: iter2: found the neighbour %a \
-         through %a"
+        "WEGraph: _merge_neigbours_aux: iter2: found the neighbour %a through \
+         %a"
         (pp_eid env) nid (pp_vid env) iid;
       rm_edge_aux env nid rid iid;
       add_edge_aux kn rn env nid kid iid
   | _ -> ()
 
 let merge_neighbours env (kn, kid) (rn, rid) b =
-  Debug.dprintf5 debug "DiffGraph: _merge_neighbours %b [kn=%a; rn=%a]" b
+  Debug.dprintf5 debug "WEGraph: _merge_neighbours %b [kn=%a; rn=%a]" b
     (pp_eid env) kid (pp_eid env) rid;
   (* Add all the neighbours of rnode to knp, removes rnode as a neighbour from the
      others and adds knp as a neighbour to them if it isn't already. *)
-  (match (DG.find_opt env kid, DG.find_opt env rid) with
+  (match (WEG.find_opt env kid, WEG.find_opt env rid) with
   | Some (_, knm), Some (_, rnm) ->
       let m1 = DInt.M.remove rid knm in
       let m2 = DInt.M.remove kid rnm in
@@ -475,9 +475,9 @@ let merge_neighbours env (kn, kid) (rn, rid) b =
          | None -> ()
          | Some iid -> rm_edge_aux env kid rid iid
        with Not_a_neighbour _ -> ());
-      DG.remove env rid;
-      if Debug.test_flag DG.diffgraph_opt then
-        DG.pp_dot_diffgraph
+      WEG.remove env rid;
+      if Debug.test_flag WEG.wegraph_opt then
+        WEG.pp_dot_wegraph
           ~msg:
             (Fmt.str "_merge_neighbours %b | %a | %a\\n remove %a" b
                (pp_eid env) rid (pp_eid env) kid (pp_eid env) rid)
@@ -487,8 +487,8 @@ let merge_neighbours env (kn, kid) (rn, rid) b =
       DInt.M.iter
         (fun nid iid ->
           Debug.dprintf4 debug
-            "DiffGraph: _merge_neighbours: iter3: found the neighbour %a \
-             through %a"
+            "WEGraph: _merge_neighbours: iter3: found the neighbour %a through \
+             %a"
             (pp_eid env) nid (pp_vid env) iid;
           rm_edge_aux env nid rid iid;
           add_edge_aux kn rn env nid kid iid)
@@ -496,24 +496,24 @@ let merge_neighbours env (kn, kid) (rn, rid) b =
   | _ -> ());
   if not b then (
     EHT.set env kid rn;
-    if Debug.test_flag DG.diffgraph_opt then
-      DG.pp_dot_diffgraph
+    if Debug.test_flag WEG.wegraph_opt then
+      WEG.pp_dot_wegraph
         ~msg:
           (Fmt.str "_merge_neighbours %b | %a | %a\\n replace %a <- %a" b
              (pp_eid env) rid (pp_eid env) kid (pp_eid env) kid (pp_eid env) rid)
         env ())
 
 let eq_arrays_norm env (kn, kid) (rn, rid) b =
-  Debug.dprintf4 debug "DiffGraph: eq_arrays_norm %a %a" (pp_eid env) kid
+  Debug.dprintf4 debug "WEGraph: eq_arrays_norm %a %a" (pp_eid env) kid
     (pp_eid env) rid;
   merge_neighbours env (kn, kid) (rn, rid) b;
-  if Debug.test_flag DG.diffgraph_opt then
-    DG.pp_dot_diffgraph
+  if Debug.test_flag WEG.wegraph_opt then
+    WEG.pp_dot_wegraph
       ~msg:(Fmt.str "eq_arrays_norm %a %a" (pp_eid env) kid (pp_eid env) rid)
       env ()
 
 let eq_indices_norm env (_kn, kid) (rn, rid) b =
-  Debug.dprintf4 debug "DiffGraph: eq_indices_norm %a %a" (pp_eid env) kid
+  Debug.dprintf4 debug "WEGraph: eq_indices_norm %a %a" (pp_eid env) kid
     (pp_eid env) rid;
   (match (Vertices.find_opt env kid, Vertices.find_opt env rid) with
   | Some _, Some sr | None, Some sr ->
@@ -525,21 +525,21 @@ let eq_indices_norm env (_kn, kid) (rn, rid) b =
   | _ -> ());
   VHT.remove env rid;
   if not b then VHT.set env kid rn;
-  if Debug.test_flag DG.diffgraph_opt then
-    DG.pp_dot_diffgraph
+  if Debug.test_flag WEG.wegraph_opt then
+    WEG.pp_dot_wegraph
       ~msg:(Fmt.str "eq_indices_norm %a %a" (pp_eid env) kid (pp_eid env) rid)
       env ()
 
 let update env a b k _v =
   let aid = Id_dom.get_id env a in
   let bid = Id_dom.get_id env b in
-  Debug.dprintf6 debug "DiffGraph.update: %a %a %a" (pp_eid env) aid
-    (pp_eid env) bid Node.pp k;
+  Debug.dprintf6 debug "WEGraph.update: %a %a %a" (pp_eid env) aid (pp_eid env)
+    bid Node.pp k;
   add_edge env aid bid (Index_Id_dom.get_id env k);
-  if Debug.test_flag DG.diffgraph_opt then
-    DG.pp_dot_diffgraph
+  if Debug.test_flag WEG.wegraph_opt then
+    WEG.pp_dot_wegraph
       ~msg:
-        (Fmt.str "DiffGraph.update: %a %a %a" (pp_eid env) aid (pp_eid env) bid
+        (Fmt.str "WEGraph.update: %a %a %a" (pp_eid env) aid (pp_eid env) bid
            Node.pp k)
       env ()
 
@@ -548,13 +548,13 @@ let get_neighbours env nid =
     if DInt.S.mem inp acc then acc
     else
       let nacc = DInt.S.add inp acc in
-      match DG.find_opt env inp with
+      match WEG.find_opt env inp with
       | None -> nacc
       | Some (m, _) -> (
           match DInt.M.find_opt k m with
           | None -> nacc
           | Some s -> DInt.S.fold (aux k) s nacc)
   in
-  match DG.find_opt env nid with
+  match WEG.find_opt env nid with
   | None -> DInt.S.empty
   | Some (m, _) -> DInt.M.fold (fun k -> DInt.S.fold (aux k)) m DInt.S.empty
diff --git a/colibri2/theories/array/DiffGraph.mli b/colibri2/theories/array/WEGraph.mli
similarity index 99%
rename from colibri2/theories/array/DiffGraph.mli
rename to colibri2/theories/array/WEGraph.mli
index 2d551184e1c94abe0b34569eb1bdb5d796c7822c..50185276974ad7a8ce3b866c6e712256e2478f50 100644
--- a/colibri2/theories/array/DiffGraph.mli
+++ b/colibri2/theories/array/WEGraph.mli
@@ -23,7 +23,7 @@ open Colibri2_core
 open Colibri2_popop_lib
 open Popop_stdlib
 
-module DG : sig
+module WEG : sig
   val find_opt :
     Egraph.wt -> int -> (DInt.S.t DInt.M.t * DInt.t DInt.M.t) option
 end
diff --git a/colibri2/theories/array/array.ml b/colibri2/theories/array/array.ml
index 2129642107e796d625a28467fd79dc9b04e5ecef..5d5e7e6e367ae1359354dead856bc4bafcf657eb 100644
--- a/colibri2/theories/array/array.ml
+++ b/colibri2/theories/array/array.ml
@@ -23,7 +23,7 @@ open Colibri2_core
 open Colibri2_popop_lib
 open Common
 open Colibri2_theories_quantifiers
-open GE_Array_DP
+open RWRules
 
 (*
   Command line options:
@@ -35,7 +35,7 @@ open GE_Array_DP
     (const, map, def_ind, def_val)
   - "--array-blast-rule": uses the blast rule when it suits
   - "--array-def-values": suppots the rules on the default values
-  - "--array-diff-graph": uses the diff graph
+  - "--array-wegraph": uses the weak equivalency graph
 *)
 
 let converter env (f : Ground.t) =
@@ -45,7 +45,7 @@ let converter env (f : Ground.t) =
     match s.ty with
     | { app = { builtin = Expr.Array; _ }; args = [ ind_gty; val_gty ]; _ } ->
         add_array_gty env fn ind_gty val_gty;
-        DiffGraph.Id_dom.set_id env fn;
+        WEGraph.Id_dom.set_id env fn;
         new_array env ind_gty val_gty f;
         true
     | _ -> false
@@ -89,7 +89,7 @@ let converter env (f : Ground.t) =
       Egraph.register env a;
       Egraph.register env i;
       add_array_gty env a ind_gty val_gty;
-      DiffGraph.Id_dom.set_id env a;
+      WEGraph.Id_dom.set_id env a;
       (* update of the Foreign domain *)
       if Options.get env restrict_ext && ind_gty.app.builtin == Expr.Array then (
         Ground.add_ty env i ind_gty;
@@ -129,9 +129,9 @@ let converter env (f : Ground.t) =
       Egraph.register env v;
       add_array_gty env a ind_gty val_gty;
       add_array_gty env b ind_gty val_gty;
-      DiffGraph.Id_dom.set_id env a;
-      DiffGraph.Id_dom.set_id env b;
-      DiffGraph.Index_Id_dom.set_id env k;
+      WEGraph.Id_dom.set_id env a;
+      WEGraph.Id_dom.set_id env b;
+      WEGraph.Index_Id_dom.set_id env k;
       (* update of the Linearity domain *)
       if Options.get env restrict_aup then
         Linearity_dom.upd_dom env fn (Linear b);
@@ -146,7 +146,7 @@ let converter env (f : Ground.t) =
         let eq_node = mk_eq env store_n b agty in
         Egraph.register env eq_node;
         Boolean.set_true env eq_node);
-      if Options.get env use_diff_graph then (
+      if Options.get env use_wegraph then (
         let ak = mk_select env a k ind_gty val_gty in
         Egraph.register env ak;
         if not (Egraph.is_equal env ak v) then (
@@ -163,7 +163,7 @@ let converter env (f : Ground.t) =
           let eqn = mk_eq env a b (Ground.Ty.array ind_gty val_gty) in
           Egraph.register env eqn;
           Boolean.set_true env eqn)
-        else DiffGraph.update env a b k v)
+        else WEGraph.update env a b k v)
   | {
    app = { builtin = Builtin.Array_diff; _ };
    args;
@@ -174,8 +174,8 @@ let converter env (f : Ground.t) =
       let a, b = IArray.extract2_exn args in
       Egraph.register env a;
       Egraph.register env b;
-      DiffGraph.Id_dom.set_id env a;
-      DiffGraph.Id_dom.set_id env b;
+      WEGraph.Id_dom.set_id env a;
+      WEGraph.Id_dom.set_id env b;
       add_array_gty env a ind_gty val_gty;
       add_array_gty env b ind_gty val_gty
   | {
@@ -210,7 +210,7 @@ let converter env (f : Ground.t) =
        let f_arity = IArray.length args - 1 in
        IArray.iteri args ~f:(fun i n ->
            if i > 0 then (
-             DiffGraph.Id_dom.set_id env n;
+             WEGraph.Id_dom.set_id env n;
              add_array_gty env n bi_ind_ty bi_val_ty;
              Array_dom.add_map_parent env n f
                { bi_ind_ty; bi_val_ty; a_val_ty; f_arity })));
@@ -221,14 +221,14 @@ let init env =
   Array_value.init_ty env;
   Array_value.init_check env;
   Ground.register_converter env converter;
-  if Options.get env use_diff_graph then (
-    DiffGraph.Id_dom.register_merge_hook env DiffGraph.eq_arrays_norm;
-    DiffGraph.Index_Id_dom.register_merge_hook env DiffGraph.eq_indices_norm);
+  if Options.get env use_wegraph then (
+    WEGraph.Id_dom.register_merge_hook env WEGraph.eq_arrays_norm;
+    WEGraph.Index_Id_dom.register_merge_hook env WEGraph.eq_indices_norm);
   (* extáµ£ (restricted extensionality):
      - (a = b) ≡ false |> (a[k] ≠ b[k])
      - a, b, {a,b} ⊆ foreign |> (a = b) ⋁ (a[k] ≠ b[k]) *)
   if Options.get env restrict_ext then
-    if Options.get env use_diff_graph then (
+    if Options.get env use_wegraph then (
       (* (a = b) ≡ false |> (a[k] ≠ b[k]) (when a and b are neighbours) *)
       Equality.register_hook_new_disequality env (apply_res_ext_1_2 env);
       (* a, b, {a,b} ⊆ foreign |> (a = b) ⋁ (a[k] ≠ b[k])
diff --git a/colibri2/theories/array/common.ml b/colibri2/theories/array/common.ml
index e46769b7975c91e254a6b7838da54c823facdf73..b6ffb23bdb62a0e5527622718e3b12be54a81773 100644
--- a/colibri2/theories/array/common.ml
+++ b/colibri2/theories/array/common.ml
@@ -54,11 +54,11 @@ let default_values =
       & info [ "array-def-values" ]
           ~doc:"Use inference rules for default values")
 
-let use_diff_graph =
-  Options.register ~pp:Fmt.bool "Array.diff-graph"
+let use_wegraph =
+  Options.register ~pp:Fmt.bool "Array.wegraph"
     Cmdliner.Arg.(
       value & flag
-      & info [ "array-diff-graph" ] ~doc:"Use the array's diff graph")
+      & info [ "array-wegraph" ] ~doc:"Use the array's weak equivalency graph")
 
 let use_choice =
   Options.register ~pp:Fmt.bool "Array.choice"
diff --git a/colibri2/theories/array/common.mli b/colibri2/theories/array/common.mli
index a4efe23ae37e0a682734672c5f7fc7e4fddc110a..dec274a869336fff6ac0c10fdcf5f8173def4300 100644
--- a/colibri2/theories/array/common.mli
+++ b/colibri2/theories/array/common.mli
@@ -24,7 +24,7 @@ val restrict_aup : bool Options.t
 val extended_comb : bool Options.t
 val blast_rule : bool Options.t
 val default_values : bool Options.t
-val use_diff_graph : bool Options.t
+val use_wegraph : bool Options.t
 val use_choice : bool Options.t
 val debug : Debug.flag
 val convert : subst:Ground.Subst.t -> 'a Egraph.t -> Expr.term -> Node.t