Skip to content
Snippets Groups Projects
Commit 76d20810 authored by Hichem R. A.'s avatar Hichem R. A. Committed by Hichem R. A.
Browse files

[Array] update tests

parent a2a7a3f7
No related branches found
No related tags found
1 merge request!32Update ocplib-simplex, some fixes
Pipeline #53655 passed
Stage: test
    Hide whitespace changes
    Inline Side-by-side
    colibri2/tests/solve/smt_array/errors/notes.txt deleted 100644 → 0
    + 0
    − 4
    View file @ a2a7a3f7
    - eq.smt2: timeout
    - out.smt2: unsound
    colibri2/tests/solve/smt_array/sat/dune.inc
    + 24
    − 0
    View file @ 76d20810
    (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 --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
    --dont-print-result %{dep:imp1.smt2})) (package colibri2)) --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-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) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat
    ...@@ -8,6 +11,9 @@ ...@@ -8,6 +11,9 @@
    --dont-print-result %{dep:test1.smt2})) (package colibri2)) --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-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 --array-res-ext --check-status sat (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --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
    --dont-print-result %{dep:imp1.smt2})) (package colibri2)) --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-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) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status sat
    ...@@ -17,6 +23,9 @@ ...@@ -17,6 +23,9 @@
    --dont-print-result %{dep:test1.smt2})) (package colibri2)) --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-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 --array-res-aup --check-status sat (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --check-status sat
    --dont-print-result %{dep: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
    --dont-print-result %{dep:imp1.smt2})) (package colibri2)) --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-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) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --check-status sat
    ...@@ -26,6 +35,9 @@ ...@@ -26,6 +35,9 @@
    --dont-print-result %{dep:test1.smt2})) (package colibri2)) --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-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-wegraph --check-status sat (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status sat
    --dont-print-result %{dep: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
    --dont-print-result %{dep:imp1.smt2})) (package colibri2)) --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-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) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status sat
    ...@@ -35,6 +47,9 @@ ...@@ -35,6 +47,9 @@
    --dont-print-result %{dep:test1.smt2})) (package colibri2)) --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-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
    (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --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-choice --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-choice --check-status sat
    --dont-print-result %{dep:imp1.smt2})) (package colibri2)) --dont-print-result %{dep:imp1.smt2})) (package colibri2))
    (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat --learning --dont-print-result %{dep:imp1.smt2})) (package colibri2)) (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat --learning --dont-print-result %{dep:imp1.smt2})) (package colibri2))
    (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat
    ...@@ -44,6 +59,9 @@ ...@@ -44,6 +59,9 @@
    --dont-print-result %{dep:test1.smt2})) (package colibri2)) --dont-print-result %{dep:test1.smt2})) (package colibri2))
    (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2)) (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
    (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --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-choice --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-choice --check-status sat
    --dont-print-result %{dep:imp1.smt2})) (package colibri2)) --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-choice --check-status sat --learning --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-choice --check-status sat --learning --dont-print-result %{dep:imp1.smt2})) (package colibri2))
    (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat
    ...@@ -53,6 +71,9 @@ ...@@ -53,6 +71,9 @@
    --dont-print-result %{dep:test1.smt2})) (package colibri2)) --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-choice --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2)) (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
    (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat
    --dont-print-result %{dep: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 --array-choice --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 --array-choice --check-status sat
    --dont-print-result %{dep:imp1.smt2})) (package colibri2)) --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 --array-choice --check-status sat --learning --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 --array-choice --check-status sat --learning --dont-print-result %{dep:imp1.smt2})) (package colibri2))
    (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat
    ...@@ -62,6 +83,9 @@ ...@@ -62,6 +83,9 @@
    --dont-print-result %{dep:test1.smt2})) (package colibri2)) --dont-print-result %{dep:test1.smt2})) (package colibri2))
    (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2)) (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status sat --learning --dont-print-result %{dep:test1.smt2})) (package colibri2))
    (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status sat (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status sat
    --dont-print-result %{dep:eq.smt2})) (package colibri2))
    (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status sat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
    (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status sat
    --dont-print-result %{dep:imp1.smt2})) (package colibri2)) --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-choice --check-status sat --learning --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-choice --check-status sat --learning --dont-print-result %{dep:imp1.smt2})) (package colibri2))
    (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status sat (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status sat
    ......
    colibri2/tests/solve/smt_array/unknown/test.smt2 0 → 100644
    + 5
    − 0
    View file @ 76d20810
    (set-logic ALIRA)
    (declare-fun s_ () (Array Int Real))
    (declare-fun s () (Array Int (Array Int Real)))
    (assert (and (forall ((_? Int)) false) (or false (exists ((_? Int)) (and true (exists ((__? Int)) (distinct (select s_ 0) (select (select s 0) 0))))))))
    (check-sat)
    colibri2/tests/solve/smt_array/unsat/dune.inc
    + 24
    − 0
    View file @ 76d20810
    ...@@ -35,6 +35,9 @@ ...@@ -35,6 +35,9 @@
    --dont-print-result %{dep:impls6.smt2})) (package colibri2)) --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-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) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
    --dont-print-result %{dep:out.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:out.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)) --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-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) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat
    ...@@ -80,6 +83,9 @@ ...@@ -80,6 +83,9 @@
    --dont-print-result %{dep:impls6.smt2})) (package colibri2)) --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-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) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status unsat
    --dont-print-result %{dep:out.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:out.smt2})) (package colibri2))
    (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status unsat
    --dont-print-result %{dep:select.smt2})) (package colibri2)) --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-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) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --check-status unsat
    ...@@ -125,6 +131,9 @@ ...@@ -125,6 +131,9 @@
    --dont-print-result %{dep:impls6.smt2})) (package colibri2)) --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-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) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --check-status unsat
    --dont-print-result %{dep:out.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:out.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
    --dont-print-result %{dep:select.smt2})) (package colibri2)) --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-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) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --check-status unsat
    ...@@ -170,6 +179,9 @@ ...@@ -170,6 +179,9 @@
    --dont-print-result %{dep:impls6.smt2})) (package colibri2)) --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-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) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat
    --dont-print-result %{dep:out.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:out.smt2})) (package colibri2))
    (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat
    --dont-print-result %{dep:select.smt2})) (package colibri2)) --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-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) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --check-status unsat
    ...@@ -215,6 +227,9 @@ ...@@ -215,6 +227,9 @@
    --dont-print-result %{dep:impls6.smt2})) (package colibri2)) --dont-print-result %{dep:impls6.smt2})) (package colibri2))
    (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:impls6.smt2})) (package colibri2)) (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:impls6.smt2})) (package colibri2))
    (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat
    --dont-print-result %{dep:out.smt2})) (package colibri2))
    (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:out.smt2})) (package colibri2))
    (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat
    --dont-print-result %{dep:select.smt2})) (package colibri2)) --dont-print-result %{dep:select.smt2})) (package colibri2))
    (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:select.smt2})) (package colibri2)) (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat --learning --dont-print-result %{dep:select.smt2})) (package colibri2))
    (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-choice --check-status unsat
    ...@@ -260,6 +275,9 @@ ...@@ -260,6 +275,9 @@
    --dont-print-result %{dep:impls6.smt2})) (package colibri2)) --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-choice --check-status unsat --learning --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-choice --check-status unsat --learning --dont-print-result %{dep:impls6.smt2})) (package colibri2))
    (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat
    --dont-print-result %{dep:out.smt2})) (package colibri2))
    (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat --learning --dont-print-result %{dep:out.smt2})) (package colibri2))
    (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat
    --dont-print-result %{dep:select.smt2})) (package colibri2)) --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-choice --check-status unsat --learning --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-choice --check-status unsat --learning --dont-print-result %{dep:select.smt2})) (package colibri2))
    (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-choice --check-status unsat
    ...@@ -305,6 +323,9 @@ ...@@ -305,6 +323,9 @@
    --dont-print-result %{dep:impls6.smt2})) (package colibri2)) --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 --array-choice --check-status unsat --learning --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 --array-choice --check-status unsat --learning --dont-print-result %{dep:impls6.smt2})) (package colibri2))
    (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat
    --dont-print-result %{dep:out.smt2})) (package colibri2))
    (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat --learning --dont-print-result %{dep:out.smt2})) (package colibri2))
    (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat
    --dont-print-result %{dep:select.smt2})) (package colibri2)) --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 --array-choice --check-status unsat --learning --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 --array-choice --check-status unsat --learning --dont-print-result %{dep:select.smt2})) (package colibri2))
    (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-res-ext --array-res-aup --array-choice --check-status unsat
    ...@@ -350,6 +371,9 @@ ...@@ -350,6 +371,9 @@
    --dont-print-result %{dep:impls6.smt2})) (package colibri2)) --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-choice --check-status unsat --learning --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-choice --check-status unsat --learning --dont-print-result %{dep:impls6.smt2})) (package colibri2))
    (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat
    --dont-print-result %{dep:out.smt2})) (package colibri2))
    (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat --learning --dont-print-result %{dep:out.smt2})) (package colibri2))
    (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat
    --dont-print-result %{dep:select.smt2})) (package colibri2)) --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-choice --check-status unsat --learning --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-choice --check-status unsat --learning --dont-print-result %{dep:select.smt2})) (package colibri2))
    (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --array-wegraph --array-choice --check-status unsat
    ......
    0% or .
    You are about to add 0 people to the discussion. Proceed with caution.
    Finish editing this message first!
    Please register or to comment