Remove optimize test suite

bclement-ocp · Jun 3, 2024 · 9478d0e · 9478d0e
1 parent 8a07ae2
commit 9478d0e
Show file tree

Hide file tree

Showing 22 changed files with 51 additions and 16,691 deletions.
diff --git a/tests/dune.inc b/tests/dune.inc
diff --git a/tests/models/arith/arith10.optimize.expected → tests/models/arith/arith10.dolmen.expected b/tests/models/arith/arith10.optimize.expected → tests/models/arith/arith10.dolmen.expected
diff --git a/tests/models/arith/arith10.optimize.smt2 → tests/models/arith/arith10.dolmen.smt2 b/tests/models/arith/arith10.optimize.smt2 → tests/models/arith/arith10.dolmen.smt2
diff --git a/tests/models/arith/arith11.optimize.expected → tests/models/arith/arith11.dolmen.expected b/tests/models/arith/arith11.optimize.expected → tests/models/arith/arith11.dolmen.expected
diff --git a/tests/models/arith/arith11.optimize.smt2 → tests/models/arith/arith11.dolmen.smt2 b/tests/models/arith/arith11.optimize.smt2 → tests/models/arith/arith11.dolmen.smt2
diff --git a/tests/models/arith/arith12.optimize.expected → tests/models/arith/arith12.dolmen.expected b/tests/models/arith/arith12.optimize.expected → tests/models/arith/arith12.dolmen.expected
diff --git a/tests/models/arith/arith12.optimize.smt2 → tests/models/arith/arith12.dolmen.smt2 b/tests/models/arith/arith12.optimize.smt2 → tests/models/arith/arith12.dolmen.smt2
diff --git a/tests/models/arith/arith3.optimize.expected → tests/models/arith/arith3.dolmen.expected b/tests/models/arith/arith3.optimize.expected → tests/models/arith/arith3.dolmen.expected
diff --git a/tests/models/arith/arith3.optimize.smt2 → tests/models/arith/arith3.dolmen.smt2 b/tests/models/arith/arith3.optimize.smt2 → tests/models/arith/arith3.dolmen.smt2
diff --git a/tests/models/arith/arith4.optimize.expected → tests/models/arith/arith4.dolmen.expected b/tests/models/arith/arith4.optimize.expected → tests/models/arith/arith4.dolmen.expected
diff --git a/tests/models/arith/arith4.optimize.smt2 → tests/models/arith/arith4.dolmen.smt2 b/tests/models/arith/arith4.optimize.smt2 → tests/models/arith/arith4.dolmen.smt2
diff --git a/tests/models/arith/arith5.optimize.expected → tests/models/arith/arith5.dolmen.expected b/tests/models/arith/arith5.optimize.expected → tests/models/arith/arith5.dolmen.expected
diff --git a/tests/models/arith/arith5.optimize.smt2 → tests/models/arith/arith5.dolmen.smt2 b/tests/models/arith/arith5.optimize.smt2 → tests/models/arith/arith5.dolmen.smt2
diff --git a/tests/models/arith/arith6.optimize.expected → tests/models/arith/arith6.dolmen.expected b/tests/models/arith/arith6.optimize.expected → tests/models/arith/arith6.dolmen.expected
diff --git a/tests/models/arith/arith6.optimize.smt2 → tests/models/arith/arith6.dolmen.smt2 b/tests/models/arith/arith6.optimize.smt2 → tests/models/arith/arith6.dolmen.smt2
diff --git a/tests/models/arith/arith7.optimize.expected → tests/models/arith/arith7.dolmen.expected b/tests/models/arith/arith7.optimize.expected → tests/models/arith/arith7.dolmen.expected
diff --git a/tests/models/arith/arith7.optimize.smt2 → tests/models/arith/arith7.dolmen.smt2 b/tests/models/arith/arith7.optimize.smt2 → tests/models/arith/arith7.dolmen.smt2
diff --git a/tests/models/arith/arith8.optimize.expected → tests/models/arith/arith8.dolmen.expected b/tests/models/arith/arith8.optimize.expected → tests/models/arith/arith8.dolmen.expected
diff --git a/tests/models/arith/arith8.optimize.smt2 → tests/models/arith/arith8.dolmen.smt2 b/tests/models/arith/arith8.optimize.smt2 → tests/models/arith/arith8.dolmen.smt2
diff --git a/tests/models/arith/arith9.optimize.expected → tests/models/arith/arith9.dolmen.expected b/tests/models/arith/arith9.optimize.expected → tests/models/arith/arith9.dolmen.expected
diff --git a/tests/models/arith/arith9.optimize.smt2 → tests/models/arith/arith9.dolmen.smt2 b/tests/models/arith/arith9.optimize.smt2 → tests/models/arith/arith9.dolmen.smt2
diff --git a/tools/gentest.ml b/tools/gentest.ml
@@ -262,11 +262,6 @@ end = struct
                 }
               | "fpa" ->
                 {acc with filters = Some ["fpa"]}
-              | "optimize" -> {
-                  acc with
-                  exclude = "legacy" :: acc.exclude;
-                  filters = Some ["optimize"]
-                }
               | _ -> acc
           )
             Test.base_params
@@ -395,10 +390,7 @@ let () =
      [ "--output=smtlib2"
      ; "--frontend dolmen"
      ; "--sat-solver CDCL"
-     ; "--no-minimal-bj" ])
-  ; ("runtest", "optimize",
-     [ "--output=smtlib2"
-     ; "--frontend dolmen" ])]
+     ; "--no-minimal-bj" ])]
   in
   let cmds = List.map (fun (group, name, args) ->
       let args = shared @ args in