From 9aec94b668d9de54e14eba3f19c0421b9b17e545 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 10 Aug 2023 13:56:40 +0200 Subject: [PATCH] Check ground models with Dolmen --- Makefile | 2 +- alt-ergo-lib.opam | 1 + dune-project | 1 + tests/dune.inc | 4408 +++++++++++++++++++++++---------------------- tools/gentest.ml | 34 +- 5 files changed, 2293 insertions(+), 2153 deletions(-) diff --git a/Makefile b/Makefile index 13b5157ac5..ffc393c55f 100644 --- a/Makefile +++ b/Makefile @@ -124,7 +124,7 @@ runtest: gentest bin # Run non-regression tests for the CI. runtest-ci: gentest bin - dune build @runtest @runtest-quick @runtest-ci + dune build @runtest @runtest-quick @runtest-ci @check-models # Promote new outputs of the tests. promote: diff --git a/alt-ergo-lib.opam b/alt-ergo-lib.opam index a1f4a97c48..37deda2138 100644 --- a/alt-ergo-lib.opam +++ b/alt-ergo-lib.opam @@ -20,6 +20,7 @@ depends: [ "dolmen" {>= "0.9"} "dolmen_type" {>= "0.9"} "dolmen_loop" {>= "0.9"} + "dolmen_bin" {with-test} "ocplib-simplex" {>= "0.5"} "zarith" {>= "1.11"} "seq" diff --git a/dune-project b/dune-project index ead928dd40..d48ae312ce 100644 --- a/dune-project +++ b/dune-project @@ -80,6 +80,7 @@ See more details on http://alt-ergo.ocamlpro.com/" (dolmen (>= 0.9)) (dolmen_type (>= 0.9)) (dolmen_loop (>= 0.9)) + (dolmen_bin :with-test) (ocplib-simplex (>= 0.5)) (zarith (>= 1.11)) seq diff --git a/tests/dune.inc b/tests/dune.inc index 3b21d9a7f6..0fd4063dc1 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -175773,1923 +175773,1936 @@ (alias runtest-quick) (package alt-ergo) (action - (diff 777.models.expected 777.models_tableaux.output))) - (rule - (target 696_ci_cdcl_no_minimal_bj.output) - (deps (:input 696.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL - --no-minimal-bj - %{input}))))))) - (rule - (deps 696_ci_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 696.expected 696_ci_cdcl_no_minimal_bj.output))) - (rule - (target 696_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input 696.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-minimal-bj - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 696_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 696.expected 696_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input 696.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 696.expected 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target 696_ci_no_tableaux_cdcl_in_instantiation.output) - (deps (:input 696.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 696_ci_no_tableaux_cdcl_in_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 696.expected 696_ci_no_tableaux_cdcl_in_instantiation.output))) - (rule - (target 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (deps (:input 696.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-tableaux-cdcl-in-theories - %{input}))))))) - (rule - (deps 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 696.expected 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) - (rule - (target 696_ci_tableaux_cdcl_no_minimal_bj.output) - (deps (:input 696.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-minimal-bj - %{input}))))))) - (rule - (deps 696_ci_tableaux_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 696.expected 696_ci_tableaux_cdcl_no_minimal_bj.output))) - (rule - (target 696_cdcl.output) - (deps (:input 696.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL - %{input}))))))) - (rule - (deps 696_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 696.expected 696_cdcl.output))) - (rule - (target 696_tableaux_cdcl.output) - (deps (:input 696.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver Tableaux-CDCL - %{input}))))))) - (rule - (deps 696_tableaux_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 696.expected 696_tableaux_cdcl.output))) - (rule - (target 696_tableaux.output) - (deps (:input 696.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver Tableaux - %{input}))))))) - (rule - (deps 696_tableaux.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 696.expected 696_tableaux.output))) - (rule - (target 696_legacy.output) - (deps (:input 696.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend legacy - %{input}))))))) - (rule - (deps 696_legacy.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 696.expected 696_legacy.output))) - (rule - (target 696_dolmen.output) - (deps (:input 696.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - %{input}))))))) - (rule - (deps 696_dolmen.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 696.expected 696_dolmen.output))) - (rule - (target 696_fpa.output) - (deps (:input 696.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --enable-theories fpa - %{input}))))))) - (rule - (deps 696_fpa.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 696.expected 696_fpa.output))) - (rule - (target 695_ci_cdcl_no_minimal_bj.output) - (deps (:input 695.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL - --no-minimal-bj - %{input}))))))) - (rule - (deps 695_ci_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 695.expected 695_ci_cdcl_no_minimal_bj.output))) - (rule - (target 695_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input 695.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-minimal-bj - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 695_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 695.expected 695_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input 695.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 695.expected 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target 695_ci_no_tableaux_cdcl_in_instantiation.output) - (deps (:input 695.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 695_ci_no_tableaux_cdcl_in_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 695.expected 695_ci_no_tableaux_cdcl_in_instantiation.output))) - (rule - (target 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (deps (:input 695.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-tableaux-cdcl-in-theories - %{input}))))))) - (rule - (deps 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 695.expected 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) - (rule - (target 695_ci_tableaux_cdcl_no_minimal_bj.output) - (deps (:input 695.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-minimal-bj - %{input}))))))) - (rule - (deps 695_ci_tableaux_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 695.expected 695_ci_tableaux_cdcl_no_minimal_bj.output))) - (rule - (target 695_cdcl.output) - (deps (:input 695.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL - %{input}))))))) - (rule - (deps 695_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 695.expected 695_cdcl.output))) - (rule - (target 695_tableaux_cdcl.output) - (deps (:input 695.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver Tableaux-CDCL - %{input}))))))) - (rule - (deps 695_tableaux_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 695.expected 695_tableaux_cdcl.output))) - (rule - (target 695_tableaux.output) - (deps (:input 695.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver Tableaux - %{input}))))))) - (rule - (deps 695_tableaux.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 695.expected 695_tableaux.output))) - (rule - (target 695_legacy.output) - (deps (:input 695.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend legacy - %{input}))))))) - (rule - (deps 695_legacy.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 695.expected 695_legacy.output))) - (rule - (target 695_dolmen.output) - (deps (:input 695.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - %{input}))))))) - (rule - (deps 695_dolmen.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 695.expected 695_dolmen.output))) - (rule - (target 695_fpa.output) - (deps (:input 695.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --enable-theories fpa - %{input}))))))) - (rule - (deps 695_fpa.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 695.expected 695_fpa.output))) - (rule - (target 645_ci_cdcl_no_minimal_bj.output) - (deps (:input 645.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL - --no-minimal-bj - %{input}))))))) - (rule - (deps 645_ci_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 645.expected 645_ci_cdcl_no_minimal_bj.output))) - (rule - (target 645_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input 645.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-minimal-bj - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 645_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 645.expected 645_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input 645.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 645.expected 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target 645_ci_no_tableaux_cdcl_in_instantiation.output) - (deps (:input 645.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 645_ci_no_tableaux_cdcl_in_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 645.expected 645_ci_no_tableaux_cdcl_in_instantiation.output))) - (rule - (target 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (deps (:input 645.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-tableaux-cdcl-in-theories - %{input}))))))) - (rule - (deps 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 645.expected 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) - (rule - (target 645_ci_tableaux_cdcl_no_minimal_bj.output) - (deps (:input 645.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-minimal-bj - %{input}))))))) - (rule - (deps 645_ci_tableaux_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 645.expected 645_ci_tableaux_cdcl_no_minimal_bj.output))) - (rule - (target 645_cdcl.output) - (deps (:input 645.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL - %{input}))))))) - (rule - (deps 645_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 645.expected 645_cdcl.output))) - (rule - (target 645_tableaux_cdcl.output) - (deps (:input 645.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver Tableaux-CDCL - %{input}))))))) - (rule - (deps 645_tableaux_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 645.expected 645_tableaux_cdcl.output))) - (rule - (target 645_tableaux.output) - (deps (:input 645.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver Tableaux - %{input}))))))) - (rule - (deps 645_tableaux.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 645.expected 645_tableaux.output))) - (rule - (target 645_legacy.output) - (deps (:input 645.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend legacy - %{input}))))))) - (rule - (deps 645_legacy.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 645.expected 645_legacy.output))) - (rule - (target 645_dolmen.output) - (deps (:input 645.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - %{input}))))))) - (rule - (deps 645_dolmen.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 645.expected 645_dolmen.output))) - (rule - (target 645_fpa.output) - (deps (:input 645.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --enable-theories fpa - %{input}))))))) - (rule - (deps 645_fpa.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 645.expected 645_fpa.output))) - (rule - (target 555.models_tableaux.output) - (deps (:input 555.models.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver Tableaux - %{input}))))))) - (rule - (deps 555.models_tableaux.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 555.models.expected 555.models_tableaux.output))) - (rule - (target 479_ci_cdcl_no_minimal_bj.output) - (deps (:input 479.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL - --no-minimal-bj - %{input}))))))) - (rule - (deps 479_ci_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 479.expected 479_ci_cdcl_no_minimal_bj.output))) - (rule - (target 479_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input 479.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-minimal-bj - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 479_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 479.expected 479_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input 479.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 479.expected 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target 479_ci_no_tableaux_cdcl_in_instantiation.output) - (deps (:input 479.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 479_ci_no_tableaux_cdcl_in_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 479.expected 479_ci_no_tableaux_cdcl_in_instantiation.output))) - (rule - (target 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (deps (:input 479.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-tableaux-cdcl-in-theories - %{input}))))))) - (rule - (deps 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 479.expected 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) - (rule - (target 479_ci_tableaux_cdcl_no_minimal_bj.output) - (deps (:input 479.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-minimal-bj - %{input}))))))) - (rule - (deps 479_ci_tableaux_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 479.expected 479_ci_tableaux_cdcl_no_minimal_bj.output))) - (rule - (target 479_cdcl.output) - (deps (:input 479.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL - %{input}))))))) - (rule - (deps 479_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 479.expected 479_cdcl.output))) - (rule - (target 479_tableaux_cdcl.output) - (deps (:input 479.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver Tableaux-CDCL - %{input}))))))) - (rule - (deps 479_tableaux_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 479.expected 479_tableaux_cdcl.output))) - (rule - (target 479_tableaux.output) - (deps (:input 479.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver Tableaux - %{input}))))))) - (rule - (deps 479_tableaux.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 479.expected 479_tableaux.output))) - (rule - (target 479_legacy.output) - (deps (:input 479.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend legacy - %{input}))))))) - (rule - (deps 479_legacy.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 479.expected 479_legacy.output))) - (rule - (target 479_dolmen.output) - (deps (:input 479.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - %{input}))))))) - (rule - (deps 479_dolmen.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 479.expected 479_dolmen.output))) - (rule - (target 479_fpa.output) - (deps (:input 479.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --enable-theories fpa - %{input}))))))) - (rule - (deps 479_fpa.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 479.expected 479_fpa.output))) - (rule - (target 460_ci_cdcl_no_minimal_bj.output) - (deps (:input 460.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL - --no-minimal-bj - %{input}))))))) - (rule - (deps 460_ci_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 460.expected 460_ci_cdcl_no_minimal_bj.output))) - (rule - (target 460_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input 460.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-minimal-bj - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 460_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 460.expected 460_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input 460.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 460.expected 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target 460_ci_no_tableaux_cdcl_in_instantiation.output) - (deps (:input 460.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 460_ci_no_tableaux_cdcl_in_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 460.expected 460_ci_no_tableaux_cdcl_in_instantiation.output))) - (rule - (target 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (deps (:input 460.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-tableaux-cdcl-in-theories - %{input}))))))) - (rule - (deps 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 460.expected 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) - (rule - (target 460_ci_tableaux_cdcl_no_minimal_bj.output) - (deps (:input 460.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-minimal-bj - %{input}))))))) - (rule - (deps 460_ci_tableaux_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 460.expected 460_ci_tableaux_cdcl_no_minimal_bj.output))) - (rule - (target 460_cdcl.output) - (deps (:input 460.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL - %{input}))))))) - (rule - (deps 460_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 460.expected 460_cdcl.output))) - (rule - (target 460_tableaux_cdcl.output) - (deps (:input 460.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver Tableaux-CDCL - %{input}))))))) - (rule - (deps 460_tableaux_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 460.expected 460_tableaux_cdcl.output))) - (rule - (target 460_tableaux.output) - (deps (:input 460.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver Tableaux - %{input}))))))) - (rule - (deps 460_tableaux.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 460.expected 460_tableaux.output))) - (rule - (target 460_legacy.output) - (deps (:input 460.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend legacy - %{input}))))))) - (rule - (deps 460_legacy.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 460.expected 460_legacy.output))) - (rule - (target 460_dolmen.output) - (deps (:input 460.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - %{input}))))))) - (rule - (deps 460_dolmen.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 460.expected 460_dolmen.output))) - (rule - (target 460_fpa.output) - (deps (:input 460.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --enable-theories fpa - %{input}))))))) - (rule - (deps 460_fpa.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 460.expected 460_fpa.output))) - (rule - (target 350_ci_cdcl_no_minimal_bj.output) - (deps (:input 350.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL - --no-minimal-bj - %{input}))))))) - (rule - (deps 350_ci_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 350.expected 350_ci_cdcl_no_minimal_bj.output))) - (rule - (target 350_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input 350.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-minimal-bj - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 350_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 350.expected 350_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input 350.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 350.expected 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target 350_ci_no_tableaux_cdcl_in_instantiation.output) - (deps (:input 350.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 350_ci_no_tableaux_cdcl_in_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 350.expected 350_ci_no_tableaux_cdcl_in_instantiation.output))) - (rule - (target 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (deps (:input 350.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-tableaux-cdcl-in-theories - %{input}))))))) - (rule - (deps 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 350.expected 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) - (rule - (target 350_ci_tableaux_cdcl_no_minimal_bj.output) - (deps (:input 350.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-minimal-bj - %{input}))))))) - (rule - (deps 350_ci_tableaux_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 350.expected 350_ci_tableaux_cdcl_no_minimal_bj.output))) - (rule - (target 350_cdcl.output) - (deps (:input 350.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL - %{input}))))))) - (rule - (deps 350_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 350.expected 350_cdcl.output))) - (rule - (target 350_tableaux_cdcl.output) - (deps (:input 350.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver Tableaux-CDCL - %{input}))))))) - (rule - (deps 350_tableaux_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 350.expected 350_tableaux_cdcl.output))) - (rule - (target 350_tableaux.output) - (deps (:input 350.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver Tableaux - %{input}))))))) - (rule - (deps 350_tableaux.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 350.expected 350_tableaux.output))) - (rule - (target 350_legacy.output) - (deps (:input 350.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend legacy - %{input}))))))) - (rule - (deps 350_legacy.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 350.expected 350_legacy.output))) - (rule - (target 350_dolmen.output) - (deps (:input 350.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - %{input}))))))) - (rule - (deps 350_dolmen.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 350.expected 350_dolmen.output))) - (rule - (target 350_fpa.output) - (deps (:input 350.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --enable-theories fpa - %{input}))))))) - (rule - (deps 350_fpa.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 350.expected 350_fpa.output))) - (rule - (target 340_ci_cdcl_no_minimal_bj.output) - (deps (:input 340.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL - --no-minimal-bj - %{input}))))))) - (rule - (deps 340_ci_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 340.expected 340_ci_cdcl_no_minimal_bj.output))) - (rule - (target 340_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input 340.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-minimal-bj - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 340_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 340.expected 340_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input 340.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 340.expected 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target 340_ci_no_tableaux_cdcl_in_instantiation.output) - (deps (:input 340.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 340_ci_no_tableaux_cdcl_in_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 340.expected 340_ci_no_tableaux_cdcl_in_instantiation.output))) - (rule - (target 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (deps (:input 340.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-tableaux-cdcl-in-theories - %{input}))))))) - (rule - (deps 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 340.expected 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) - (rule - (target 340_ci_tableaux_cdcl_no_minimal_bj.output) - (deps (:input 340.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL-Tableaux - --no-minimal-bj - %{input}))))))) - (rule - (deps 340_ci_tableaux_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 340.expected 340_ci_tableaux_cdcl_no_minimal_bj.output))) - (rule - (target 340_cdcl.output) - (deps (:input 340.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver CDCL - %{input}))))))) - (rule - (deps 340_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 340.expected 340_cdcl.output))) - (rule - (target 340_tableaux_cdcl.output) - (deps (:input 340.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver Tableaux-CDCL - %{input}))))))) - (rule - (deps 340_tableaux_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 340.expected 340_tableaux_cdcl.output))) - (rule - (target 340_tableaux.output) - (deps (:input 340.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver Tableaux - %{input}))))))) - (rule - (deps 340_tableaux.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 340.expected 340_tableaux.output))) - (rule - (target 340_legacy.output) - (deps (:input 340.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend legacy - %{input}))))))) - (rule - (deps 340_legacy.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 340.expected 340_legacy.output))) - (rule - (target 340_dolmen.output) - (deps (:input 340.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - %{input}))))))) - (rule - (deps 340_dolmen.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 340.expected 340_dolmen.output))) - (rule - (target 340_fpa.output) - (deps (:input 340.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --enable-theories fpa - %{input}))))))) - (rule - (deps 340_fpa.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 340.expected 340_fpa.output)))) -; Auto-generated part end -; File auto-generated by gentests + (diff 777.models.expected 777.models_tableaux.output)))(rule + (alias check-models) + (deps (:input 777.models_tableaux.output) (:test 777.models.smt2)) + (package alt-ergo) + (action + (with-accepted-exit-codes 0 + (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}")))) -; Auto-generated part begin + +(rule + (target 696_ci_cdcl_no_minimal_bj.output) + (deps (:input 696.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + --no-minimal-bj + %{input}))))))) +(rule + (deps 696_ci_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 696.expected 696_ci_cdcl_no_minimal_bj.output))) +(rule + (target 696_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 696.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) +(rule + (deps 696_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 696.expected 696_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) +(rule + (target 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 696.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) +(rule + (deps 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 696.expected 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) +(rule + (target 696_ci_no_tableaux_cdcl_in_instantiation.output) + (deps (:input 696.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-instantiation + %{input}))))))) +(rule + (deps 696_ci_no_tableaux_cdcl_in_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 696.expected 696_ci_no_tableaux_cdcl_in_instantiation.output))) +(rule + (target 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (deps (:input 696.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + %{input}))))))) +(rule + (deps 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 696.expected 696_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) +(rule + (target 696_ci_tableaux_cdcl_no_minimal_bj.output) + (deps (:input 696.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + %{input}))))))) +(rule + (deps 696_ci_tableaux_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 696.expected 696_ci_tableaux_cdcl_no_minimal_bj.output))) +(rule + (target 696_cdcl.output) + (deps (:input 696.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + %{input}))))))) +(rule + (deps 696_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 696.expected 696_cdcl.output))) +(rule + (target 696_tableaux_cdcl.output) + (deps (:input 696.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux-CDCL + %{input}))))))) +(rule + (deps 696_tableaux_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 696.expected 696_tableaux_cdcl.output))) +(rule + (target 696_tableaux.output) + (deps (:input 696.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) +(rule + (deps 696_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 696.expected 696_tableaux.output))) +(rule + (target 696_legacy.output) + (deps (:input 696.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend legacy + %{input}))))))) +(rule + (deps 696_legacy.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 696.expected 696_legacy.output))) +(rule + (target 696_dolmen.output) + (deps (:input 696.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) +(rule + (deps 696_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 696.expected 696_dolmen.output))) +(rule + (target 696_fpa.output) + (deps (:input 696.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --enable-theories fpa + %{input}))))))) +(rule + (deps 696_fpa.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 696.expected 696_fpa.output))) +(rule + (target 695_ci_cdcl_no_minimal_bj.output) + (deps (:input 695.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + --no-minimal-bj + %{input}))))))) +(rule + (deps 695_ci_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 695.expected 695_ci_cdcl_no_minimal_bj.output))) +(rule + (target 695_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 695.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) +(rule + (deps 695_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 695.expected 695_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) +(rule + (target 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 695.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) +(rule + (deps 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 695.expected 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) +(rule + (target 695_ci_no_tableaux_cdcl_in_instantiation.output) + (deps (:input 695.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-instantiation + %{input}))))))) +(rule + (deps 695_ci_no_tableaux_cdcl_in_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 695.expected 695_ci_no_tableaux_cdcl_in_instantiation.output))) +(rule + (target 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (deps (:input 695.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + %{input}))))))) +(rule + (deps 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 695.expected 695_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) +(rule + (target 695_ci_tableaux_cdcl_no_minimal_bj.output) + (deps (:input 695.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + %{input}))))))) +(rule + (deps 695_ci_tableaux_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 695.expected 695_ci_tableaux_cdcl_no_minimal_bj.output))) +(rule + (target 695_cdcl.output) + (deps (:input 695.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + %{input}))))))) +(rule + (deps 695_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 695.expected 695_cdcl.output))) +(rule + (target 695_tableaux_cdcl.output) + (deps (:input 695.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux-CDCL + %{input}))))))) +(rule + (deps 695_tableaux_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 695.expected 695_tableaux_cdcl.output))) +(rule + (target 695_tableaux.output) + (deps (:input 695.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) +(rule + (deps 695_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 695.expected 695_tableaux.output))) +(rule + (target 695_legacy.output) + (deps (:input 695.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend legacy + %{input}))))))) +(rule + (deps 695_legacy.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 695.expected 695_legacy.output))) +(rule + (target 695_dolmen.output) + (deps (:input 695.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) +(rule + (deps 695_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 695.expected 695_dolmen.output))) +(rule + (target 695_fpa.output) + (deps (:input 695.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --enable-theories fpa + %{input}))))))) +(rule + (deps 695_fpa.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 695.expected 695_fpa.output))) +(rule + (target 645_ci_cdcl_no_minimal_bj.output) + (deps (:input 645.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + --no-minimal-bj + %{input}))))))) +(rule + (deps 645_ci_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 645.expected 645_ci_cdcl_no_minimal_bj.output))) +(rule + (target 645_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 645.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) +(rule + (deps 645_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 645.expected 645_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) +(rule + (target 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 645.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) +(rule + (deps 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 645.expected 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) +(rule + (target 645_ci_no_tableaux_cdcl_in_instantiation.output) + (deps (:input 645.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-instantiation + %{input}))))))) +(rule + (deps 645_ci_no_tableaux_cdcl_in_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 645.expected 645_ci_no_tableaux_cdcl_in_instantiation.output))) +(rule + (target 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (deps (:input 645.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + %{input}))))))) +(rule + (deps 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 645.expected 645_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) +(rule + (target 645_ci_tableaux_cdcl_no_minimal_bj.output) + (deps (:input 645.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + %{input}))))))) +(rule + (deps 645_ci_tableaux_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 645.expected 645_ci_tableaux_cdcl_no_minimal_bj.output))) +(rule + (target 645_cdcl.output) + (deps (:input 645.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + %{input}))))))) +(rule + (deps 645_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 645.expected 645_cdcl.output))) +(rule + (target 645_tableaux_cdcl.output) + (deps (:input 645.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux-CDCL + %{input}))))))) +(rule + (deps 645_tableaux_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 645.expected 645_tableaux_cdcl.output))) +(rule + (target 645_tableaux.output) + (deps (:input 645.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) +(rule + (deps 645_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 645.expected 645_tableaux.output))) +(rule + (target 645_legacy.output) + (deps (:input 645.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend legacy + %{input}))))))) +(rule + (deps 645_legacy.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 645.expected 645_legacy.output))) +(rule + (target 645_dolmen.output) + (deps (:input 645.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) +(rule + (deps 645_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 645.expected 645_dolmen.output))) +(rule + (target 645_fpa.output) + (deps (:input 645.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --enable-theories fpa + %{input}))))))) +(rule + (deps 645_fpa.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 645.expected 645_fpa.output))) +(rule + (target 555.models_tableaux.output) + (deps (:input 555.models.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) +(rule + (deps 555.models_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 555.models.expected 555.models_tableaux.output)))(rule + (alias check-models) + (deps (:input 555.models_tableaux.output) (:test 555.models.smt2)) + (package alt-ergo) + (action + (with-accepted-exit-codes 0 + (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}")))) + + +(rule + (target 479_ci_cdcl_no_minimal_bj.output) + (deps (:input 479.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + --no-minimal-bj + %{input}))))))) +(rule + (deps 479_ci_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 479.expected 479_ci_cdcl_no_minimal_bj.output))) +(rule + (target 479_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 479.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) +(rule + (deps 479_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 479.expected 479_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) +(rule + (target 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 479.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) +(rule + (deps 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 479.expected 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) +(rule + (target 479_ci_no_tableaux_cdcl_in_instantiation.output) + (deps (:input 479.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-instantiation + %{input}))))))) +(rule + (deps 479_ci_no_tableaux_cdcl_in_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 479.expected 479_ci_no_tableaux_cdcl_in_instantiation.output))) +(rule + (target 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (deps (:input 479.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + %{input}))))))) +(rule + (deps 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 479.expected 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) +(rule + (target 479_ci_tableaux_cdcl_no_minimal_bj.output) + (deps (:input 479.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + %{input}))))))) +(rule + (deps 479_ci_tableaux_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 479.expected 479_ci_tableaux_cdcl_no_minimal_bj.output))) +(rule + (target 479_cdcl.output) + (deps (:input 479.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + %{input}))))))) +(rule + (deps 479_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 479.expected 479_cdcl.output))) +(rule + (target 479_tableaux_cdcl.output) + (deps (:input 479.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux-CDCL + %{input}))))))) +(rule + (deps 479_tableaux_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 479.expected 479_tableaux_cdcl.output))) +(rule + (target 479_tableaux.output) + (deps (:input 479.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) +(rule + (deps 479_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 479.expected 479_tableaux.output))) +(rule + (target 479_legacy.output) + (deps (:input 479.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend legacy + %{input}))))))) +(rule + (deps 479_legacy.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 479.expected 479_legacy.output))) +(rule + (target 479_dolmen.output) + (deps (:input 479.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) +(rule + (deps 479_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 479.expected 479_dolmen.output))) +(rule + (target 479_fpa.output) + (deps (:input 479.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --enable-theories fpa + %{input}))))))) +(rule + (deps 479_fpa.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 479.expected 479_fpa.output))) +(rule + (target 460_ci_cdcl_no_minimal_bj.output) + (deps (:input 460.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + --no-minimal-bj + %{input}))))))) +(rule + (deps 460_ci_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 460.expected 460_ci_cdcl_no_minimal_bj.output))) +(rule + (target 460_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 460.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) +(rule + (deps 460_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 460.expected 460_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) +(rule + (target 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 460.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) +(rule + (deps 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 460.expected 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) +(rule + (target 460_ci_no_tableaux_cdcl_in_instantiation.output) + (deps (:input 460.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-instantiation + %{input}))))))) +(rule + (deps 460_ci_no_tableaux_cdcl_in_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 460.expected 460_ci_no_tableaux_cdcl_in_instantiation.output))) +(rule + (target 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (deps (:input 460.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + %{input}))))))) +(rule + (deps 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 460.expected 460_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) +(rule + (target 460_ci_tableaux_cdcl_no_minimal_bj.output) + (deps (:input 460.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + %{input}))))))) +(rule + (deps 460_ci_tableaux_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 460.expected 460_ci_tableaux_cdcl_no_minimal_bj.output))) +(rule + (target 460_cdcl.output) + (deps (:input 460.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + %{input}))))))) +(rule + (deps 460_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 460.expected 460_cdcl.output))) +(rule + (target 460_tableaux_cdcl.output) + (deps (:input 460.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux-CDCL + %{input}))))))) +(rule + (deps 460_tableaux_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 460.expected 460_tableaux_cdcl.output))) +(rule + (target 460_tableaux.output) + (deps (:input 460.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) +(rule + (deps 460_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 460.expected 460_tableaux.output))) +(rule + (target 460_legacy.output) + (deps (:input 460.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend legacy + %{input}))))))) +(rule + (deps 460_legacy.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 460.expected 460_legacy.output))) +(rule + (target 460_dolmen.output) + (deps (:input 460.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) +(rule + (deps 460_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 460.expected 460_dolmen.output))) +(rule + (target 460_fpa.output) + (deps (:input 460.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --enable-theories fpa + %{input}))))))) +(rule + (deps 460_fpa.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 460.expected 460_fpa.output))) +(rule + (target 350_ci_cdcl_no_minimal_bj.output) + (deps (:input 350.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + --no-minimal-bj + %{input}))))))) +(rule + (deps 350_ci_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 350.expected 350_ci_cdcl_no_minimal_bj.output))) +(rule + (target 350_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 350.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) +(rule + (deps 350_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 350.expected 350_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) +(rule + (target 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 350.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) +(rule + (deps 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 350.expected 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) +(rule + (target 350_ci_no_tableaux_cdcl_in_instantiation.output) + (deps (:input 350.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-instantiation + %{input}))))))) +(rule + (deps 350_ci_no_tableaux_cdcl_in_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 350.expected 350_ci_no_tableaux_cdcl_in_instantiation.output))) +(rule + (target 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (deps (:input 350.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + %{input}))))))) +(rule + (deps 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 350.expected 350_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) +(rule + (target 350_ci_tableaux_cdcl_no_minimal_bj.output) + (deps (:input 350.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + %{input}))))))) +(rule + (deps 350_ci_tableaux_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 350.expected 350_ci_tableaux_cdcl_no_minimal_bj.output))) +(rule + (target 350_cdcl.output) + (deps (:input 350.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + %{input}))))))) +(rule + (deps 350_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 350.expected 350_cdcl.output))) +(rule + (target 350_tableaux_cdcl.output) + (deps (:input 350.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux-CDCL + %{input}))))))) +(rule + (deps 350_tableaux_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 350.expected 350_tableaux_cdcl.output))) +(rule + (target 350_tableaux.output) + (deps (:input 350.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) +(rule + (deps 350_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 350.expected 350_tableaux.output))) +(rule + (target 350_legacy.output) + (deps (:input 350.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend legacy + %{input}))))))) +(rule + (deps 350_legacy.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 350.expected 350_legacy.output))) +(rule + (target 350_dolmen.output) + (deps (:input 350.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) +(rule + (deps 350_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 350.expected 350_dolmen.output))) +(rule + (target 350_fpa.output) + (deps (:input 350.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --enable-theories fpa + %{input}))))))) +(rule + (deps 350_fpa.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 350.expected 350_fpa.output))) +(rule + (target 340_ci_cdcl_no_minimal_bj.output) + (deps (:input 340.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + --no-minimal-bj + %{input}))))))) +(rule + (deps 340_ci_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 340.expected 340_ci_cdcl_no_minimal_bj.output))) +(rule + (target 340_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 340.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) +(rule + (deps 340_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 340.expected 340_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) +(rule + (target 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 340.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) +(rule + (deps 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 340.expected 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) +(rule + (target 340_ci_no_tableaux_cdcl_in_instantiation.output) + (deps (:input 340.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-instantiation + %{input}))))))) +(rule + (deps 340_ci_no_tableaux_cdcl_in_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 340.expected 340_ci_no_tableaux_cdcl_in_instantiation.output))) +(rule + (target 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (deps (:input 340.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + %{input}))))))) +(rule + (deps 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 340.expected 340_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) +(rule + (target 340_ci_tableaux_cdcl_no_minimal_bj.output) + (deps (:input 340.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + %{input}))))))) +(rule + (deps 340_ci_tableaux_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 340.expected 340_ci_tableaux_cdcl_no_minimal_bj.output))) +(rule + (target 340_cdcl.output) + (deps (:input 340.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + %{input}))))))) +(rule + (deps 340_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 340.expected 340_cdcl.output))) +(rule + (target 340_tableaux_cdcl.output) + (deps (:input 340.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux-CDCL + %{input}))))))) +(rule + (deps 340_tableaux_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 340.expected 340_tableaux_cdcl.output))) +(rule + (target 340_tableaux.output) + (deps (:input 340.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) +(rule + (deps 340_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 340.expected 340_tableaux.output))) +(rule + (target 340_legacy.output) + (deps (:input 340.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend legacy + %{input}))))))) +(rule + (deps 340_legacy.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 340.expected 340_legacy.output))) +(rule + (target 340_dolmen.output) + (deps (:input 340.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) +(rule + (deps 340_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 340.expected 340_dolmen.output))) +(rule + (target 340_fpa.output) + (deps (:input 340.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --enable-theories fpa + %{input}))))))) +(rule + (deps 340_fpa.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 340.expected 340_fpa.output)))) ; Auto-generated part end +; File auto-generated by gentests ; Auto-generated part begin (subdir issues/649 (rule (target 649.dolmen_dolmen.output) @@ -177981,11 +177994,8 @@ (alias runtest-quick) (package alt-ergo) (action - (diff 649.expected 649_fpa.output)))) -; Auto-generated part end -; File auto-generated by gentests - -; Auto-generated part begin + (diff 649.expected 649_fpa.output)))) ; Auto-generated part end +; File auto-generated by gentests ; Auto-generated part begin (subdir issues/664 (rule (target 664.dolmen_dolmen.output) @@ -178277,11 +178287,8 @@ (alias runtest-quick) (package alt-ergo) (action - (diff 664.expected 664_fpa.output)))) -; Auto-generated part end -; File auto-generated by gentests - -; Auto-generated part begin + (diff 664.expected 664_fpa.output)))) ; Auto-generated part end +; File auto-generated by gentests ; Auto-generated part begin (subdir issues/854 (rule (target twice_eq.models_tableaux.output) @@ -178306,52 +178313,76 @@ (action (diff twice_eq.models.expected twice_eq.models_tableaux.output))) (rule - (target original.models_tableaux.output) - (deps (:input original.models.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver Tableaux - %{input}))))))) - (rule - (deps original.models_tableaux.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff original.models.expected original.models_tableaux.output))) - (rule - (target function.models_tableaux.output) - (deps (:input function.models.smt2)) + (alias check-models) + (deps (:input twice_eq.models_tableaux.output) (:test twice_eq.models.smt2)) (package alt-ergo) (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver Tableaux - %{input}))))))) - (rule - (deps function.models_tableaux.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff function.models.expected function.models_tableaux.output)))) -; Auto-generated part end -; File auto-generated by gentests + (with-accepted-exit-codes 0 + (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}")))) + + +(rule + (target original.models_tableaux.output) + (deps (:input original.models.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) +(rule + (deps original.models_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff original.models.expected original.models_tableaux.output))) +(rule + (alias check-models) + (deps (:input original.models_tableaux.output) (:test original.models.smt2)) + (package alt-ergo) + (action + (with-accepted-exit-codes 0 + (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}")))) + +(rule + (target function.models_tableaux.output) + (deps (:input function.models.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) +(rule + (deps function.models_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff function.models.expected function.models_tableaux.output))) +(rule + (alias check-models) + (deps (:input function.models_tableaux.output) (:test function.models.smt2)) + (package alt-ergo) + (action + (with-accepted-exit-codes 0 + (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}")))) + +) ; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir ite (rule @@ -180783,11 +180814,8 @@ (alias runtest-quick) (package alt-ergo) (action - (diff ite-1.expected ite-1_fpa.output)))) -; Auto-generated part end -; File auto-generated by gentests - -; Auto-generated part begin + (diff ite-1.expected ite-1_fpa.output)))) ; Auto-generated part end +; File auto-generated by gentests ; Auto-generated part begin (subdir let (rule (target testfile-let016_ci_cdcl_no_minimal_bj.output) @@ -191859,9 +191887,7 @@ (package alt-ergo) (action (diff let--invalid-1.expected let--invalid-1_fpa.output)))) -; Auto-generated part end -; File auto-generated by gentests - +; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir misc (rule @@ -192404,9 +192430,7 @@ (package alt-ergo) (action (diff unzip.ae.expected unzip.ae_fpa.output)))) -; Auto-generated part end -; File auto-generated by gentests - +; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir models (rule @@ -192430,10 +192454,16 @@ (alias runtest-quick) (package alt-ergo) (action - (diff check_sat.models.expected check_sat.models_tableaux.output)))) -; Auto-generated part end -; File auto-generated by gentests + (diff check_sat.models.expected check_sat.models_tableaux.output))) + (rule + (alias check-models) + (deps (:input check_sat.models_tableaux.output) (:test check_sat.models.ae)) + (package alt-ergo) + (action + (with-accepted-exit-codes 0 + (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}")))) +) ; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir models/arith (rule @@ -192457,32 +192487,45 @@ (alias runtest-quick) (package alt-ergo) (action - (diff arith2.models.expected arith2.models_tableaux.output))) - (rule - (target arith1.models_tableaux.output) - (deps (:input arith1.models.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver Tableaux - %{input}))))))) - (rule - (deps arith1.models_tableaux.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff arith1.models.expected arith1.models_tableaux.output)))) -; Auto-generated part end -; File auto-generated by gentests + (diff arith2.models.expected arith2.models_tableaux.output)))(rule + (alias check-models) + (deps (:input arith2.models_tableaux.output) (:test arith2.models.smt2)) + (package alt-ergo) + (action + (with-accepted-exit-codes 0 + (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}")))) + +(rule + (target arith1.models_tableaux.output) + (deps (:input arith1.models.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) +(rule + (deps arith1.models_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff arith1.models.expected arith1.models_tableaux.output)))(rule + (alias check-models) + (deps (:input arith1.models_tableaux.output) (:test arith1.models.smt2)) + (package alt-ergo) + (action + (with-accepted-exit-codes 0 + (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}")))) + +) ; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir models/array (rule @@ -192506,10 +192549,15 @@ (alias runtest-quick) (package alt-ergo) (action - (diff array1.models.expected array1.models_tableaux.output)))) -; Auto-generated part end -; File auto-generated by gentests + (diff array1.models.expected array1.models_tableaux.output)))(rule + (alias check-models) + (deps (:input array1.models_tableaux.output) (:test array1.models.smt2)) + (package alt-ergo) + (action + (with-accepted-exit-codes 0 + (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}")))) +) ; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir models/bitv (rule @@ -192535,52 +192583,75 @@ (action (diff specified.models.expected specified.models_tableaux.output))) (rule - (target extract.models_tableaux.output) - (deps (:input extract.models.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver Tableaux - %{input}))))))) - (rule - (deps extract.models_tableaux.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff extract.models.expected extract.models_tableaux.output))) - (rule - (target cardinal.models_tableaux.output) - (deps (:input cardinal.models.smt2)) + (alias check-models) + (deps (:input specified.models_tableaux.output) (:test specified.models.smt2)) (package alt-ergo) (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver Tableaux - %{input}))))))) - (rule - (deps cardinal.models_tableaux.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff cardinal.models.expected cardinal.models_tableaux.output)))) -; Auto-generated part end -; File auto-generated by gentests + (with-accepted-exit-codes 0 + (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}")))) + + +(rule + (target extract.models_tableaux.output) + (deps (:input extract.models.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) +(rule + (deps extract.models_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff extract.models.expected extract.models_tableaux.output)))(rule + (alias check-models) + (deps (:input extract.models_tableaux.output) (:test extract.models.smt2)) + (package alt-ergo) + (action + (with-accepted-exit-codes 0 + (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}")))) + + +(rule + (target cardinal.models_tableaux.output) + (deps (:input cardinal.models.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) +(rule + (deps cardinal.models_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff cardinal.models.expected cardinal.models_tableaux.output))) +(rule + (alias check-models) + (deps (:input cardinal.models_tableaux.output) (:test cardinal.models.smt2)) + (package alt-ergo) + (action + (with-accepted-exit-codes 0 + (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}")))) +) ; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir models/bool (rule @@ -192604,32 +192675,45 @@ (alias runtest-quick) (package alt-ergo) (action - (diff bool2.models.expected bool2.models_tableaux.output))) - (rule - (target bool1.models_tableaux.output) - (deps (:input bool1.models.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver Tableaux - %{input}))))))) - (rule - (deps bool1.models_tableaux.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff bool1.models.expected bool1.models_tableaux.output)))) -; Auto-generated part end -; File auto-generated by gentests + (diff bool2.models.expected bool2.models_tableaux.output)))(rule + (alias check-models) + (deps (:input bool2.models_tableaux.output) (:test bool2.models.smt2)) + (package alt-ergo) + (action + (with-accepted-exit-codes 0 + (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}")))) + +(rule + (target bool1.models_tableaux.output) + (deps (:input bool1.models.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) +(rule + (deps bool1.models_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff bool1.models.expected bool1.models_tableaux.output)))(rule + (alias check-models) + (deps (:input bool1.models_tableaux.output) (:test bool1.models.smt2)) + (package alt-ergo) + (action + (with-accepted-exit-codes 0 + (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}")))) + +) ; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir models/issues (rule @@ -192653,10 +192737,16 @@ (alias runtest-quick) (package alt-ergo) (action - (diff 719.models.err.expected 719.models.err_tableaux.output)))) -; Auto-generated part end -; File auto-generated by gentests + (diff 719.models.err.expected 719.models.err_tableaux.output))) + (rule + (alias check-models) + (deps (:input 719.models.err_tableaux.output) (:test 719.models.err.smt2)) + (package alt-ergo) + (action + (with-accepted-exit-codes 0 + (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}")))) +) ; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir models/issues/715 (rule @@ -192680,32 +192770,45 @@ (alias runtest-quick) (package alt-ergo) (action - (diff 715_2.models.expected 715_2.models_tableaux.output))) - (rule - (target 715_1.models_tableaux.output) - (deps (:input 715_1.models.ae)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver Tableaux - %{input}))))))) - (rule - (deps 715_1.models_tableaux.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 715_1.models.expected 715_1.models_tableaux.output)))) -; Auto-generated part end -; File auto-generated by gentests + (diff 715_2.models.expected 715_2.models_tableaux.output)))(rule + (alias check-models) + (deps (:input 715_2.models_tableaux.output) (:test 715_2.models.smt2)) + (package alt-ergo) + (action + (with-accepted-exit-codes 0 + (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}")))) + +(rule + (target 715_1.models_tableaux.output) + (deps (:input 715_1.models.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) +(rule + (deps 715_1.models_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 715_1.models.expected 715_1.models_tableaux.output)))(rule + (alias check-models) + (deps (:input 715_1.models_tableaux.output) (:test 715_1.models.ae)) + (package alt-ergo) + (action + (with-accepted-exit-codes 0 + (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}")))) + +) ; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir models/records (rule @@ -192729,10 +192832,16 @@ (alias runtest-quick) (package alt-ergo) (action - (diff record1.models.expected record1.models_tableaux.output)))) -; Auto-generated part end -; File auto-generated by gentests + (diff record1.models.expected record1.models_tableaux.output))) + (rule + (alias check-models) + (deps (:input record1.models_tableaux.output) (:test record1.models.smt2)) + (package alt-ergo) + (action + (with-accepted-exit-codes 0 + (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}")))) +) ; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir models/uf (rule @@ -192756,32 +192865,45 @@ (alias runtest-quick) (package alt-ergo) (action - (diff uf2.models.expected uf2.models_tableaux.output))) - (rule - (target uf1.models_tableaux.output) - (deps (:input uf1.models.smt2)) - (package alt-ergo) - (action - (chdir %{workspace_root} - (with-stdout-to %{target} - (ignore-stderr - (with-accepted-exit-codes 0 - (run %{bin:alt-ergo} - --timelimit=2 - --enable-assertions - --output=smtlib2 - --frontend dolmen - --sat-solver Tableaux - %{input}))))))) - (rule - (deps uf1.models_tableaux.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff uf1.models.expected uf1.models_tableaux.output)))) -; Auto-generated part end -; File auto-generated by gentests + (diff uf2.models.expected uf2.models_tableaux.output)))(rule + (alias check-models) + (deps (:input uf2.models_tableaux.output) (:test uf2.models.smt2)) + (package alt-ergo) + (action + (with-accepted-exit-codes 0 + (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}")))) + + +(rule + (target uf1.models_tableaux.output) + (deps (:input uf1.models.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) +(rule + (deps uf1.models_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff uf1.models.expected uf1.models_tableaux.output)))(rule + (alias check-models) + (deps (:input uf1.models_tableaux.output) (:test uf1.models.smt2)) + (package alt-ergo) + (action + (with-accepted-exit-codes 0 + (bash "sed 's/^unknown/sat/' %{input} | opam exec -- dolmen --check-model true %{test}")))) +) ; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir polymorphism (rule @@ -194944,9 +195066,7 @@ (package alt-ergo) (action (diff testfile-polymorphism001.expected testfile-polymorphism001_fpa.output)))) -; Auto-generated part end -; File auto-generated by gentests - +; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir quantifiers (rule @@ -203319,9 +203439,7 @@ (package alt-ergo) (action (diff testfile-github001.expected testfile-github001_fpa.output)))) -; Auto-generated part end -; File auto-generated by gentests - +; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir smtlib (rule @@ -203990,9 +204108,7 @@ (package alt-ergo) (action (diff testfile-exit.dolmen.expected testfile-exit.dolmen_dolmen.output)))) -; Auto-generated part end -; File auto-generated by gentests - +; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir sum (rule @@ -209125,9 +209241,7 @@ (package alt-ergo) (action (diff testfile-sum001.expected testfile-sum001_fpa.output)))) -; Auto-generated part end -; File auto-generated by gentests - +; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin (subdir typing (rule diff --git a/tools/gentest.ml b/tools/gentest.ml index c7ced91e37..38d08016ec 100644 --- a/tools/gentest.ml +++ b/tools/gentest.ml @@ -118,13 +118,15 @@ module Test : sig type t = private { cmd: Cmd.t; pb_file: string; - params: params + params: params; + check_model: bool; } (** Type of a test. *) val base_params : params - val make: cmd: Cmd.t -> pb_file: string -> params:params -> t + val make: cmd: Cmd.t -> pb_file: string -> check_model: bool -> + params: params -> t (** Set up the test. *) val pp_expected_output: t printer @@ -145,6 +147,7 @@ end = struct cmd: Cmd.t; pb_file: string; params: params; + check_model: bool; } let base_params = { @@ -154,7 +157,8 @@ end = struct ae_should_succeed = true; } - let make ~cmd ~pb_file ~params = {cmd; pb_file; params} + let make ~cmd ~pb_file ~check_model ~params = + {cmd; pb_file; check_model; params} let pp_output fmt tst = let filename = Filename.chop_extension tst.pb_file in @@ -205,7 +209,23 @@ end = struct Cmd.pp tst.cmd pp_output tst (Cmd.group tst.cmd) - pp_diff_command tst + pp_diff_command tst; + let () = + if tst.check_model then + Format.fprintf fmt "\ +@[\ +(rule@,\ +(alias check-models)@,\ +(deps (:input %a) (:test %s))@,\ +(package alt-ergo)@,\ +@[(action@,\ +@[(with-accepted-exit-codes 0@,\ +@[(bash \"sed 's/^unknown/sat/' %%{input} | \ +opam exec -- dolmen --check-model true %%{test}\"))))@]@]@]@]\n@." + pp_output tst + tst.pb_file + in + () end module Batch : sig @@ -265,7 +285,11 @@ end = struct in List.fold_left (fun acc2 cmd -> if filter params cmd then - Test.make ~cmd ~pb_file ~params :: acc2 + let check_model = + List.exists (String.equal "models") + (String.split_on_char '.' pb_file) + in + Test.make ~cmd ~pb_file ~check_model ~params :: acc2 else acc2 ) acc1 cmds) [] pb_files