From ea061ee06feca2d7f2d0d7e22b44bd4aac41a6f8 Mon Sep 17 00:00:00 2001
From: "Hichem R. A" <hichem.ait-el-hara@ocamlpro.com>
Date: Mon, 3 Apr 2023 15:05:44 +0200
Subject: [PATCH] [Array] new cmdline options

---
 colibri2/tests/solve/smt_array/sat/dune       |  12 +-
 colibri2/tests/solve/smt_array/sat/dune.inc   | 168 ++++----
 .../tests/solve/smt_array/sat/sat-res/dune    |   8 +-
 .../solve/smt_array/sat/sat-res/dune.inc      |  16 +-
 .../smt_array/step_limit_reached/notes.txt    |  12 +-
 colibri2/tests/solve/smt_array/unsat/dune     |  12 +-
 colibri2/tests/solve/smt_array/unsat/dune.inc | 384 +++++++++---------
 colibri2/theories/array/RWRules.ml            |   2 +-
 colibri2/theories/array/array.ml              |  25 +-
 colibri2/theories/array/common.ml             |  30 +-
 colibri2/theories/array/common.mli            |   6 +-
 11 files changed, 340 insertions(+), 335 deletions(-)

diff --git a/colibri2/tests/solve/smt_array/sat/dune b/colibri2/tests/solve/smt_array/sat/dune
index 1a9a66cd4..d73569121 100644
--- a/colibri2/tests/solve/smt_array/sat/dune
+++ b/colibri2/tests/solve/smt_array/sat/dune
@@ -11,17 +11,17 @@
    (run
     %{exe:../../../generate_tests/generate_dune_tests.exe}
     --options
-    ""
+    "no-wegraph no-res-ext no-res-aup"
     --options
-    "array-res-ext"
+    "no-wegraph no-res-aup"
     --options
-    "array-res-ext array-res-aup"
+    "no-wegraph"
     --options
-    "array-wegraph"
+    "no-res-ext no-res-aup"
     --options
-    "array-wegraph array-res-ext"
+    "no-res-aup"
     --options
-    "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 ab36f9f7b..e7b5902c9 100644
--- a/colibri2/tests/solve/smt_array/sat/dune.inc
+++ b/colibri2/tests/solve/smt_array/sat/dune.inc
@@ -1,126 +1,126 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --check-status sat 
 --dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --check-status sat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --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 --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 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --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 --no-wegraph --no-res-ext --no-res-aup --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 --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 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --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 --no-wegraph --no-res-ext --no-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 --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 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-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 --no-wegraph --no-res-ext --no-res-aup --check-status sat 
 --dont-print-result %{dep:test2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:test2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --check-status sat --learning --dont-print-result %{dep:test2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --check-status sat 
 --dont-print-result %{dep:test5.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:test5.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --check-status sat --learning --dont-print-result %{dep:test5.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --check-status sat 
 --dont-print-result %{dep:test7.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:test7.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --check-status sat --learning --dont-print-result %{dep:test7.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --check-status sat 
 --dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status sat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --check-status sat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --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-res-ext --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-res-ext --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --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 --no-wegraph --no-res-aup --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-res-ext --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-res-ext --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --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 --no-wegraph --no-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 --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-res-ext --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-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 --no-wegraph --no-res-aup --check-status sat 
 --dont-print-result %{dep:test2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status sat --learning --dont-print-result %{dep:test2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --check-status sat --learning --dont-print-result %{dep:test2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --check-status sat 
 --dont-print-result %{dep:test5.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status sat --learning --dont-print-result %{dep:test5.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --check-status sat --learning --dont-print-result %{dep:test5.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --check-status sat 
 --dont-print-result %{dep:test7.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status sat --learning --dont-print-result %{dep:test7.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --check-status sat --learning --dont-print-result %{dep:test7.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --check-status sat 
 --dont-print-result %{dep:eq.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:eq.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --check-status sat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-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-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-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 --no-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-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-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 --no-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-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-res-ext --array-res-aup --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-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 --no-wegraph --check-status sat 
 --dont-print-result %{dep:test2.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:test2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --check-status sat --learning --dont-print-result %{dep:test2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --check-status sat 
 --dont-print-result %{dep:test5.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:test5.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --check-status sat --learning --dont-print-result %{dep:test5.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --check-status sat 
 --dont-print-result %{dep:test7.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:test7.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --check-status sat --learning --dont-print-result %{dep:test7.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --check-status sat 
 --dont-print-result %{dep:eq.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:eq.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --check-status sat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --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-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 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --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 --no-res-ext --no-res-aup --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-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 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --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 --no-res-ext --no-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-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-wegraph --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-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 --no-res-ext --no-res-aup --check-status sat 
 --dont-print-result %{dep:test2.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:test2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --check-status sat --learning --dont-print-result %{dep:test2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --check-status sat 
 --dont-print-result %{dep:test5.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:test5.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --check-status sat --learning --dont-print-result %{dep:test5.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --check-status sat 
 --dont-print-result %{dep:test7.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:test7.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --check-status sat --learning --dont-print-result %{dep:test7.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --check-status sat 
 --dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --check-status sat --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-res-ext --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --check-status sat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --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-wegraph --array-res-ext --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-res-ext --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --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 --no-res-aup --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-wegraph --array-res-ext --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-res-ext --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --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 --no-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-wegraph --array-res-ext --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-wegraph --array-res-ext --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-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 --no-res-aup --check-status sat 
 --dont-print-result %{dep:test2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --check-status sat --learning --dont-print-result %{dep:test2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --check-status sat --learning --dont-print-result %{dep:test2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --check-status sat 
 --dont-print-result %{dep:test5.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --check-status sat --learning --dont-print-result %{dep:test5.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --check-status sat --learning --dont-print-result %{dep:test5.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --check-status sat 
 --dont-print-result %{dep:test7.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --check-status sat --learning --dont-print-result %{dep:test7.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --array-res-aup --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --check-status sat --learning --dont-print-result %{dep:test7.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:eq.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --array-res-aup --check-status sat --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-res-ext --array-res-aup --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --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-wegraph --array-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --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 --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-wegraph --array-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --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 --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-wegraph --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-wegraph --array-res-ext --array-res-aup --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --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 --check-status sat 
 --dont-print-result %{dep:test2.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --array-res-aup --check-status sat --learning --dont-print-result %{dep:test2.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --array-res-aup --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:test2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:test5.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --array-res-aup --check-status sat --learning --dont-print-result %{dep:test5.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --array-res-aup --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:test5.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:test7.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --array-res-aup --check-status sat --learning --dont-print-result %{dep:test7.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:test7.smt2})) (package colibri2))
diff --git a/colibri2/tests/solve/smt_array/sat/sat-res/dune b/colibri2/tests/solve/smt_array/sat/sat-res/dune
index 71929eb7a..127fe276b 100644
--- a/colibri2/tests/solve/smt_array/sat/sat-res/dune
+++ b/colibri2/tests/solve/smt_array/sat/sat-res/dune
@@ -11,13 +11,13 @@
    (run
     %{exe:../../../../generate_tests/generate_dune_tests.exe}
     --options
-    "array-res-ext"
+    "no-wegraph no-res-aup"
     --options
-    "array-res-ext array-res-aup"
+    "no-wegraph"
     --options
-    "array-wegraph array-res-ext"
+    "no-res-aup"
     --options
-    "array-wegraph array-res-ext array-res-aup"
+    ""
     .
     sat)))
  (mode promote))
diff --git a/colibri2/tests/solve/smt_array/sat/sat-res/dune.inc b/colibri2/tests/solve/smt_array/sat/sat-res/dune.inc
index 855a01945..f809f5e1b 100644
--- a/colibri2/tests/solve/smt_array/sat/sat-res/dune.inc
+++ b/colibri2/tests/solve/smt_array/sat/sat-res/dune.inc
@@ -1,12 +1,12 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status sat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --check-status sat 
 --dont-print-result %{dep:test6.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status sat --learning --dont-print-result %{dep:test6.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --check-status sat --learning --dont-print-result %{dep:test6.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --check-status sat 
 --dont-print-result %{dep:test6.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:test6.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --check-status sat --learning --dont-print-result %{dep:test6.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --check-status sat 
 --dont-print-result %{dep:test6.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --check-status sat --learning --dont-print-result %{dep:test6.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --array-res-aup --check-status sat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --check-status sat --learning --dont-print-result %{dep:test6.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat 
 --dont-print-result %{dep:test6.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --array-res-aup --check-status sat --learning --dont-print-result %{dep:test6.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:test6.smt2})) (package colibri2))
diff --git a/colibri2/tests/solve/smt_array/step_limit_reached/notes.txt b/colibri2/tests/solve/smt_array/step_limit_reached/notes.txt
index 375d1b5fa..d9e53205e 100644
--- a/colibri2/tests/solve/smt_array/step_limit_reached/notes.txt
+++ b/colibri2/tests/solve/smt_array/step_limit_reached/notes.txt
@@ -1,16 +1,16 @@
 - sat/test3.smt2:
   works with:
-  - "--array-res-ext"
-  - "--array-wegraph --array-res-ext"
+  - "--no-wegraph --no-res-aup"
+  - "--no-res-aup"
 
 - sat/test4.smt2:
   works with:
-  - ""
-  - "--array-wegraph"
+  - "--no-wegraph --no-res-ext --no-res-aup"
+  - "--no-res-ext --no-res-aup"
 
 - unsat/distinct2:
   fails with:
-  - ""
-  - "--array-wegraph"
+  - "--no-wegraph --no-res-ext --no-res-aup"
+  - "--no-res-ext --no-res-aup"
 
 - sat/test4.smt2
diff --git a/colibri2/tests/solve/smt_array/unsat/dune b/colibri2/tests/solve/smt_array/unsat/dune
index 96fdbfc04..06bd30988 100644
--- a/colibri2/tests/solve/smt_array/unsat/dune
+++ b/colibri2/tests/solve/smt_array/unsat/dune
@@ -11,17 +11,17 @@
    (run
     %{exe:../../../generate_tests/generate_dune_tests.exe}
     --options
-    ""
+    "no-wegraph no-res-ext no-res-aup"
     --options
-    "array-res-ext"
+    "no-wegraph no-res-aup"
     --options
-    "array-res-ext array-res-aup"
+    "no-wegraph"
     --options
-    "array-wegraph"
+    "no-res-ext no-res-aup"
     --options
-    "array-wegraph array-res-ext"
+    "no-res-aup"
     --options
-    "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 f8226e2dc..0f51dc27f 100644
--- a/colibri2/tests/solve/smt_array/unsat/dune.inc
+++ b/colibri2/tests/solve/smt_array/unsat/dune.inc
@@ -1,288 +1,288 @@
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --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 --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 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --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 --no-wegraph --no-res-ext --no-res-aup --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 --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 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --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 --no-wegraph --no-res-ext --no-res-aup --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 --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 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --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 --no-wegraph --no-res-ext --no-res-aup --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 --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 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --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 --no-wegraph --no-res-ext --no-res-aup --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 --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 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --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 --no-wegraph --no-res-ext --no-res-aup --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 --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 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --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 --no-wegraph --no-res-ext --no-res-aup --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 --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 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --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 --no-wegraph --no-res-ext --no-res-aup --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 --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 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --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 --no-wegraph --no-res-ext --no-res-aup --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 --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 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --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 --no-wegraph --no-res-ext --no-res-aup --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 --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 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --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 --no-wegraph --no-res-ext --no-res-aup --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 --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 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --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 --no-wegraph --no-res-ext --no-res-aup --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 --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 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --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 --no-wegraph --no-res-ext --no-res-aup --check-status unsat 
 --dont-print-result %{dep:ite.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:ite.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --check-status unsat --learning --dont-print-result %{dep:ite.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --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 --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 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --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 --no-wegraph --no-res-ext --no-res-aup --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 --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 --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-res-aup --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 --no-wegraph --no-res-ext --no-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 --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-ext --no-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 --no-wegraph --no-res-aup --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-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --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 --no-wegraph --no-res-aup --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-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --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 --no-wegraph --no-res-aup --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-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --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 --no-wegraph --no-res-aup --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-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --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 --no-wegraph --no-res-aup --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-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --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 --no-wegraph --no-res-aup --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-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --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 --no-wegraph --no-res-aup --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-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --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 --no-wegraph --no-res-aup --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-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --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 --no-wegraph --no-res-aup --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-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --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 --no-wegraph --no-res-aup --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-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --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 --no-wegraph --no-res-aup --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-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --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 --no-wegraph --no-res-aup --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-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --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 --no-wegraph --no-res-aup --check-status unsat 
 --dont-print-result %{dep:ite.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status unsat --learning --dont-print-result %{dep:ite.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --check-status unsat --learning --dont-print-result %{dep:ite.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --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-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --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 --no-wegraph --no-res-aup --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-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-res-aup --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 --no-wegraph --no-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 --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --no-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 --no-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-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-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 --no-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-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-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 --no-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-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-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 --no-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-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-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 --no-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-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-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 --no-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-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-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 --no-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-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-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 --no-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-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-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 --no-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-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-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 --no-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-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-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 --no-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-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-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 --no-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-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-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 --no-wegraph --check-status unsat 
 --dont-print-result %{dep:ite.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:ite.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-wegraph --check-status unsat --learning --dont-print-result %{dep:ite.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-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-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-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 --no-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-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-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 --no-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-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-wegraph --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-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 --no-res-ext --no-res-aup --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-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 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --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 --no-res-ext --no-res-aup --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-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 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --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 --no-res-ext --no-res-aup --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-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 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --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 --no-res-ext --no-res-aup --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-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 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --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 --no-res-ext --no-res-aup --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-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 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --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 --no-res-ext --no-res-aup --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-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 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --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 --no-res-ext --no-res-aup --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-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 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --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 --no-res-ext --no-res-aup --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-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 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --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 --no-res-ext --no-res-aup --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-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 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --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 --no-res-ext --no-res-aup --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-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 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --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 --no-res-ext --no-res-aup --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-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 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --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 --no-res-ext --no-res-aup --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-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 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --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 --no-res-ext --no-res-aup --check-status unsat 
 --dont-print-result %{dep:ite.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:ite.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --check-status unsat --learning --dont-print-result %{dep:ite.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --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-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 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --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 --no-res-ext --no-res-aup --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-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 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-res-aup --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 --no-res-ext --no-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-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-wegraph --array-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-ext --no-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 --no-res-aup --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-wegraph --array-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --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 --no-res-aup --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-wegraph --array-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --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 --no-res-aup --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-wegraph --array-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --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 --no-res-aup --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-wegraph --array-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --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 --no-res-aup --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-wegraph --array-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --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 --no-res-aup --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-wegraph --array-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --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 --no-res-aup --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-wegraph --array-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --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 --no-res-aup --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-wegraph --array-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --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 --no-res-aup --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-wegraph --array-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --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 --no-res-aup --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-wegraph --array-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --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 --no-res-aup --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-wegraph --array-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --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 --no-res-aup --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-wegraph --array-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --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 --no-res-aup --check-status unsat 
 --dont-print-result %{dep:ite.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --check-status unsat --learning --dont-print-result %{dep:ite.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --check-status unsat --learning --dont-print-result %{dep:ite.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --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-wegraph --array-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --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 --no-res-aup --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-wegraph --array-res-ext --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-res-ext --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-res-aup --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 --no-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-wegraph --array-res-ext --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-wegraph --array-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --no-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 --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-wegraph --array-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --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 --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-wegraph --array-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --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 --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-wegraph --array-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --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 --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-wegraph --array-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --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 --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-wegraph --array-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --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 --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-wegraph --array-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --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 --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-wegraph --array-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --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 --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-wegraph --array-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --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 --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-wegraph --array-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --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 --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-wegraph --array-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --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 --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-wegraph --array-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --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 --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-wegraph --array-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --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 --check-status unsat 
 --dont-print-result %{dep:ite.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --array-res-aup --check-status unsat --learning --dont-print-result %{dep:ite.smt2})) (package colibri2))
-(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:ite.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --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-wegraph --array-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --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 --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-wegraph --array-res-ext --array-res-aup --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-res-ext --array-res-aup --check-status unsat 
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --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 --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-wegraph --array-res-ext --array-res-aup --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 --check-status unsat --learning --dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
diff --git a/colibri2/theories/array/RWRules.ml b/colibri2/theories/array/RWRules.ml
index b0b5a11f7..73ec3f8f9 100644
--- a/colibri2/theories/array/RWRules.ml
+++ b/colibri2/theories/array/RWRules.ml
@@ -318,7 +318,7 @@ let new_array =
   fun env ind_gty val_gty f ->
     (* Extensionality rule ext: a, b ⇒ (a = b) ⋁ (a[k] ≠ b[k]) *)
     let agty = Ground.Ty.array ind_gty val_gty in
-    (if not (Options.get env restrict_ext) then
+    (if Options.get env no_res_ext then
      match GHT.find_opt db_gty env agty with
      | Some s ->
          Ground.S.iter
diff --git a/colibri2/theories/array/array.ml b/colibri2/theories/array/array.ml
index 3e537d4d4..e13bd6cac 100644
--- a/colibri2/theories/array/array.ml
+++ b/colibri2/theories/array/array.ml
@@ -28,14 +28,14 @@ open RWRules
 (*
   Command line options:
   - "None": uses RW1(adown), RW2(aup), idx and extensionality
-  - "--array-res-ext": restricts the extrensionality rule using the foreign
+  - "--no-wegraph": don't use the weak equivalency graph
+  - "--no-res-ext": don't restrict the extrensionality rule using the foreign
     domain
-  - "--array-res-aup": restricts the RW2 rule using the linearity domain
+  - "--no-res-aup": don't restrict the RW2 rule using the linearity domain
   - "--array-ext-comb": to support additional combinators
     (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-wegraph": uses the weak equivalency graph
 *)
 
 let converter env (f : Ground.t) =
@@ -53,10 +53,10 @@ let converter env (f : Ground.t) =
   match s with
   | { app = { builtin = Expr.Base; id_ty; _ }; args; tyargs; _ } ->
       if IArray.is_empty args then (
-        if Options.get env restrict_aup && f_is_array then
+        if (not (Options.get env no_res_aup)) && f_is_array then
           (* update of the Linearity domain *)
           Linearity_dom.upd_dom env fn Empty)
-      else if Options.get env restrict_ext then (
+      else if not (Options.get env no_res_ext) then (
         (* update of the Foreign domain *)
         let subst, arg_tys =
           match id_ty.ty_descr with
@@ -94,9 +94,10 @@ let converter env (f : Ground.t) =
       Id.Array.set_id env a;
       Id.Index.set_id env i;
       Ground.add_ty env i ind_gty;
-      if Options.get env use_wegraph then WEGraph.new_select env fn a i;
+      if not (Options.get env no_wegraph) then WEGraph.new_select env fn a i;
       (* update of the Foreign domain *)
-      if Options.get env restrict_ext && ind_gty.app.builtin == Expr.Array then
+      if (not (Options.get env no_res_ext)) && ind_gty.app.builtin == Expr.Array
+      then
         (* id and ground type are set during registration *)
         Foreign_dom.set_dom env (Ground.Ty.array ind_gty val_gty) i IsForeign;
       if Options.get env extended_comb then (
@@ -139,7 +140,7 @@ let converter env (f : Ground.t) =
       Id.Index.set_id env k;
       Id.Value.set_id env v;
       (* update of the Linearity domain *)
-      if Options.get env restrict_aup then
+      if not (Options.get env no_res_aup) then
         Linearity_dom.upd_dom env fn (Linear b);
       (* application of the `idx` rule *)
       let rn = Equality.equality env [ mk_select env a k ind_gty val_gty; v ] in
@@ -158,7 +159,7 @@ let converter env (f : Ground.t) =
         in
         Egraph.register env eq_node;
         Boolean.set_true env eq_node);
-      if Options.get env use_wegraph then WEGraph.new_store env a b k v
+      if not (Options.get env no_wegraph) then WEGraph.new_store env a b k v
   | {
    app = { builtin = Builtin.Array_diff; _ };
    args;
@@ -216,7 +217,7 @@ let init env =
   Array_value.init_ty env;
   Array_value.init_check env;
   Ground.register_converter env converter;
-  if Options.get env use_wegraph then (
+  if not (Options.get env no_wegraph) then (
     Id.Array.register_new_id_hook env WEGraph.new_id_hook;
     Id.Array.register_merge_hook env WEGraph.eq_arrays_norm;
     Id.Index.register_new_id_hook env WEGraph.new_index_id_hook;
@@ -227,7 +228,7 @@ let init env =
   (* 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 not (Options.get env no_res_ext) 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;
@@ -241,7 +242,7 @@ let init env =
     Foreign_dom.register_hook_new_foreign_array env apply_res_ext_2_1);
   let l = [ (adown_pattern, adown_run) ] in
   let l =
-    if Options.get env restrict_aup then (raup_pattern, raup_run) :: l
+    if not (Options.get env no_res_aup) then (raup_pattern, raup_run) :: l
     else (aup_pattern, aup_run) :: l
   in
   let l =
diff --git a/colibri2/theories/array/common.ml b/colibri2/theories/array/common.ml
index dee5a19d7..4e35ab627 100644
--- a/colibri2/theories/array/common.ml
+++ b/colibri2/theories/array/common.ml
@@ -24,16 +24,26 @@ open Colibri2_popop_lib
 open Popop_stdlib
 module HT = Datastructure.Hashtbl (DInt)
 
-let restrict_ext =
-  Options.register ~pp:Fmt.bool "Array.res-ext"
+let no_wegraph =
+  Options.register ~pp:Fmt.bool "Array.no-wegraph"
     Cmdliner.Arg.(
       value & flag
-      & info [ "array-res-ext" ] ~doc:"Restrict the extensionality rule")
+      & info [ "no-wegraph" ]
+          ~doc:"Don't use the array theory's weak equivalency graph")
 
-let restrict_aup =
+let no_res_ext =
+  Options.register ~pp:Fmt.bool "Array.no-res-ext"
+    Cmdliner.Arg.(
+      value & flag
+      & info [ "no-res-ext" ]
+          ~doc:"Don't restrict the array extensionality rule")
+
+let no_res_aup =
   Options.register ~pp:Fmt.bool "Array.res-aup"
     Cmdliner.Arg.(
-      value & flag & info [ "array-res-aup" ] ~doc:"Restrict the ⇑ rule")
+      value & flag
+      & info [ "no-res-aup" ]
+          ~doc:"Don't restrict the array's ⇑ (select over store) rule")
 
 let extended_comb =
   Options.register ~pp:Fmt.bool "Array.res-comb"
@@ -54,12 +64,6 @@ let default_values =
       & info [ "array-def-values" ]
           ~doc:"Use inference rules for default values")
 
-let use_wegraph =
-  Options.register ~pp:Fmt.bool "Array.wegraph"
-    Cmdliner.Arg.(
-      value & flag
-      & info [ "array-wegraph" ] ~doc:"Use the array's weak equivalency graph")
-
 let debug =
   Debug.register_info_flag ~desc:"Debugging messages of the array theory"
     "Array"
@@ -455,8 +459,8 @@ end) : IdDomSig = struct
       | Some id1, n1, Some id2, n2 ->
           Datastructure.Push.iter merge_hooks env ~f:(fun f ->
               f env (n1, id1) (n2, id2) b)
-          (* id1 always stays, b allows to determine which one will become the
-             representative *)
+      (* id1 always stays, b allows to determine which one will become the
+         representative *)
       | _ ->
           (* Ideally, should be unreachable, but it is with the test
              "./colibri2/tests/solve/smt_array/unsat/ite1.smt2"? *)
diff --git a/colibri2/theories/array/common.mli b/colibri2/theories/array/common.mli
index 646df4138..101a6a0ef 100644
--- a/colibri2/theories/array/common.mli
+++ b/colibri2/theories/array/common.mli
@@ -19,12 +19,12 @@
 (*  for more details (enclosed in the file licenses/LGPLv2.1).           *)
 (*************************************************************************)
 
-val restrict_ext : bool Options.t
-val restrict_aup : bool Options.t
+val no_wegraph : bool Options.t
+val no_res_ext : bool Options.t
+val no_res_aup : bool Options.t
 val extended_comb : bool Options.t
 val blast_rule : bool Options.t
 val default_values : bool Options.t
-val use_wegraph : bool Options.t
 val debug : Debug.flag
 val convert : subst:Ground.Subst.t -> 'a Egraph.t -> Expr.term -> Node.t
 
-- 
GitLab