diff --git a/tests/dune.inc b/tests/dune.inc index ac01873cf..1413e9191 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -175626,191 +175626,6 @@ ; Auto-generated part begin (subdir issues - (rule - (target 777.models_ci_cdcl_no_minimal_bj.output) - (deps (:input 777.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 CDCL - --no-minimal-bj - %{input}))))))) - (rule - (deps 777.models_ci_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 777.models.expected 777.models_ci_cdcl_no_minimal_bj.output))) - (rule - (target 777.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input 777.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 CDCL-Tableaux - --no-minimal-bj - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 777.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 777.models.expected 777.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target 777.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input 777.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 777.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 777.models.expected 777.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target 777.models_ci_no_tableaux_cdcl_in_instantiation.output) - (deps (:input 777.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 CDCL-Tableaux - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 777.models_ci_no_tableaux_cdcl_in_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 777.models.expected 777.models_ci_no_tableaux_cdcl_in_instantiation.output))) - (rule - (target 777.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (deps (:input 777.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - %{input}))))))) - (rule - (deps 777.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 777.models.expected 777.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) - (rule - (target 777.models_ci_tableaux_cdcl_no_minimal_bj.output) - (deps (:input 777.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 CDCL-Tableaux - --no-minimal-bj - %{input}))))))) - (rule - (deps 777.models_ci_tableaux_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 777.models.expected 777.models_ci_tableaux_cdcl_no_minimal_bj.output))) - (rule - (target 777.models_cdcl.output) - (deps (:input 777.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 CDCL - %{input}))))))) - (rule - (deps 777.models_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 777.models.expected 777.models_cdcl.output))) - (rule - (target 777.models_tableaux_cdcl.output) - (deps (:input 777.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-CDCL - %{input}))))))) - (rule - (deps 777.models_tableaux_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 777.models.expected 777.models_tableaux_cdcl.output))) (rule (target 777.models_tableaux.output) (deps (:input 777.models.smt2)) @@ -175833,27 +175648,6 @@ (package alt-ergo) (action (diff 777.models.expected 777.models_tableaux.output))) - (rule - (target 777.models_dolmen.output) - (deps (:input 777.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 - %{input}))))))) - (rule - (deps 777.models_dolmen.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 777.models.expected 777.models_dolmen.output))) (rule (target 696_ci_cdcl_no_minimal_bj.output) (deps (:input 696.ae)) @@ -176665,9 +176459,31 @@ (action (diff 645.expected 645_fpa.output))) (rule - (target 555.models_ci_cdcl_no_minimal_bj.output) + (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} @@ -176682,14 +176498,14 @@ --no-minimal-bj %{input}))))))) (rule - (deps 555.models_ci_cdcl_no_minimal_bj.output) + (deps 479_ci_cdcl_no_minimal_bj.output) (alias runtest-ci) (package alt-ergo) (action - (diff 555.models.expected 555.models_ci_cdcl_no_minimal_bj.output))) + (diff 479.expected 479_ci_cdcl_no_minimal_bj.output))) (rule - (target 555.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input 555.models.smt2)) + (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} @@ -176707,14 +176523,14 @@ --no-tableaux-cdcl-in-instantiation %{input}))))))) (rule - (deps 555.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps 479_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) (alias runtest-ci) (package alt-ergo) (action - (diff 555.models.expected 555.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (diff 479.expected 479_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) (rule - (target 555.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input 555.models.smt2)) + (target 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 479.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -176731,14 +176547,14 @@ --no-tableaux-cdcl-in-instantiation %{input}))))))) (rule - (deps 555.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) (alias runtest-ci) (package alt-ergo) (action - (diff 555.models.expected 555.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (diff 479.expected 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) (rule - (target 555.models_ci_no_tableaux_cdcl_in_instantiation.output) - (deps (:input 555.models.smt2)) + (target 479_ci_no_tableaux_cdcl_in_instantiation.output) + (deps (:input 479.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -176754,14 +176570,14 @@ --no-tableaux-cdcl-in-instantiation %{input}))))))) (rule - (deps 555.models_ci_no_tableaux_cdcl_in_instantiation.output) + (deps 479_ci_no_tableaux_cdcl_in_instantiation.output) (alias runtest-ci) (package alt-ergo) (action - (diff 555.models.expected 555.models_ci_no_tableaux_cdcl_in_instantiation.output))) + (diff 479.expected 479_ci_no_tableaux_cdcl_in_instantiation.output))) (rule - (target 555.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (deps (:input 555.models.smt2)) + (target 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (deps (:input 479.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -176777,14 +176593,14 @@ --no-tableaux-cdcl-in-theories %{input}))))))) (rule - (deps 555.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (deps 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) (alias runtest-ci) (package alt-ergo) (action - (diff 555.models.expected 555.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) + (diff 479.expected 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) (rule - (target 555.models_ci_tableaux_cdcl_no_minimal_bj.output) - (deps (:input 555.models.smt2)) + (target 479_ci_tableaux_cdcl_no_minimal_bj.output) + (deps (:input 479.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -176800,14 +176616,14 @@ --no-minimal-bj %{input}))))))) (rule - (deps 555.models_ci_tableaux_cdcl_no_minimal_bj.output) + (deps 479_ci_tableaux_cdcl_no_minimal_bj.output) (alias runtest-ci) (package alt-ergo) (action - (diff 555.models.expected 555.models_ci_tableaux_cdcl_no_minimal_bj.output))) + (diff 479.expected 479_ci_tableaux_cdcl_no_minimal_bj.output))) (rule - (target 555.models_cdcl.output) - (deps (:input 555.models.smt2)) + (target 479_cdcl.output) + (deps (:input 479.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -176822,14 +176638,14 @@ --sat-solver CDCL %{input}))))))) (rule - (deps 555.models_cdcl.output) + (deps 479_cdcl.output) (alias runtest-quick) (package alt-ergo) (action - (diff 555.models.expected 555.models_cdcl.output))) + (diff 479.expected 479_cdcl.output))) (rule - (target 555.models_tableaux_cdcl.output) - (deps (:input 555.models.smt2)) + (target 479_tableaux_cdcl.output) + (deps (:input 479.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -176844,14 +176660,14 @@ --sat-solver Tableaux-CDCL %{input}))))))) (rule - (deps 555.models_tableaux_cdcl.output) + (deps 479_tableaux_cdcl.output) (alias runtest-quick) (package alt-ergo) (action - (diff 555.models.expected 555.models_tableaux_cdcl.output))) + (diff 479.expected 479_tableaux_cdcl.output))) (rule - (target 555.models_tableaux.output) - (deps (:input 555.models.smt2)) + (target 479_tableaux.output) + (deps (:input 479.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -176866,14 +176682,14 @@ --sat-solver Tableaux %{input}))))))) (rule - (deps 555.models_tableaux.output) + (deps 479_tableaux.output) (alias runtest-quick) (package alt-ergo) (action - (diff 555.models.expected 555.models_tableaux.output))) + (diff 479.expected 479_tableaux.output))) (rule - (target 555.models_dolmen.output) - (deps (:input 555.models.smt2)) + (target 479_legacy.output) + (deps (:input 479.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -176884,244 +176700,16 @@ --timelimit=2 --enable-assertions --output=smtlib2 - --frontend dolmen + --frontend legacy %{input}))))))) (rule - (deps 555.models_dolmen.output) + (deps 479_legacy.output) (alias runtest-quick) (package alt-ergo) (action - (diff 555.models.expected 555.models_dolmen.output))) + (diff 479.expected 479_legacy.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) + (target 479_dolmen.output) (deps (:input 479.smt2)) (package alt-ergo) (action @@ -192625,7 +192213,7 @@ ; Auto-generated part begin (subdir models (rule - (target check_sat.models_ci_cdcl_no_minimal_bj.output) + (target check_sat.models_tableaux.output) (deps (:input check_sat.models.ae)) (package alt-ergo) (action @@ -192638,18 +192226,22 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver CDCL - --no-minimal-bj + --sat-solver Tableaux %{input}))))))) (rule - (deps check_sat.models_ci_cdcl_no_minimal_bj.output) - (alias runtest-ci) + (deps check_sat.models_tableaux.output) + (alias runtest-quick) (package alt-ergo) (action - (diff check_sat.models.expected check_sat.models_ci_cdcl_no_minimal_bj.output))) + (diff check_sat.models.expected check_sat.models_tableaux.output)))) +; Auto-generated part end +; File auto-generated by gentests + +; Auto-generated part begin +(subdir models/arith (rule - (target check_sat.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input check_sat.models.ae)) + (target arith2.models_tableaux.output) + (deps (:input arith2.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192661,20 +192253,17 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver CDCL-Tableaux - --no-minimal-bj - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation + --sat-solver Tableaux %{input}))))))) (rule - (deps check_sat.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) + (deps arith2.models_tableaux.output) + (alias runtest-quick) (package alt-ergo) (action - (diff check_sat.models.expected check_sat.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (diff arith2.models.expected arith2.models_tableaux.output))) (rule - (target check_sat.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input check_sat.models.ae)) + (target arith1.models_tableaux.output) + (deps (:input arith1.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192686,110 +192275,22 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver CDCL-Tableaux - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps check_sat.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff check_sat.models.expected check_sat.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target check_sat.models_ci_no_tableaux_cdcl_in_instantiation.output) - (deps (:input check_sat.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 CDCL-Tableaux - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps check_sat.models_ci_no_tableaux_cdcl_in_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff check_sat.models.expected check_sat.models_ci_no_tableaux_cdcl_in_instantiation.output))) - (rule - (target check_sat.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (deps (:input check_sat.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - %{input}))))))) - (rule - (deps check_sat.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff check_sat.models.expected check_sat.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) - (rule - (target check_sat.models_ci_tableaux_cdcl_no_minimal_bj.output) - (deps (:input check_sat.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 CDCL-Tableaux - --no-minimal-bj - %{input}))))))) - (rule - (deps check_sat.models_ci_tableaux_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff check_sat.models.expected check_sat.models_ci_tableaux_cdcl_no_minimal_bj.output))) - (rule - (target check_sat.models_cdcl.output) - (deps (:input check_sat.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 CDCL + --sat-solver Tableaux %{input}))))))) (rule - (deps check_sat.models_cdcl.output) + (deps arith1.models_tableaux.output) (alias runtest-quick) (package alt-ergo) (action - (diff check_sat.models.expected check_sat.models_cdcl.output))) + (diff arith1.models.expected arith1.models_tableaux.output)))) +; Auto-generated part end +; File auto-generated by gentests + +; Auto-generated part begin +(subdir models/array (rule - (target check_sat.models_tableaux_cdcl.output) - (deps (:input check_sat.models.ae)) + (target array1.models_tableaux.output) + (deps (:input array1.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192801,17 +192302,22 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux-CDCL + --sat-solver Tableaux %{input}))))))) (rule - (deps check_sat.models_tableaux_cdcl.output) + (deps array1.models_tableaux.output) (alias runtest-quick) (package alt-ergo) (action - (diff check_sat.models.expected check_sat.models_tableaux_cdcl.output))) + (diff array1.models.expected array1.models_tableaux.output)))) +; Auto-generated part end +; File auto-generated by gentests + +; Auto-generated part begin +(subdir models/bool (rule - (target check_sat.models_tableaux.output) - (deps (:input check_sat.models.ae)) + (target bool2.models_tableaux.output) + (deps (:input bool2.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192826,14 +192332,14 @@ --sat-solver Tableaux %{input}))))))) (rule - (deps check_sat.models_tableaux.output) + (deps bool2.models_tableaux.output) (alias runtest-quick) (package alt-ergo) (action - (diff check_sat.models.expected check_sat.models_tableaux.output))) + (diff bool2.models.expected bool2.models_tableaux.output))) (rule - (target check_sat.models_dolmen.output) - (deps (:input check_sat.models.ae)) + (target bool1.models_tableaux.output) + (deps (:input bool1.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192845,116 +192351,22 @@ --enable-assertions --output=smtlib2 --frontend dolmen + --sat-solver Tableaux %{input}))))))) (rule - (deps check_sat.models_dolmen.output) + (deps bool1.models_tableaux.output) (alias runtest-quick) (package alt-ergo) (action - (diff check_sat.models.expected check_sat.models_dolmen.output)))) + (diff bool1.models.expected bool1.models_tableaux.output)))) ; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin -(subdir models/arith - (rule - (target arith2.models_ci_cdcl_no_minimal_bj.output) - (deps (:input arith2.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 CDCL - --no-minimal-bj - %{input}))))))) - (rule - (deps arith2.models_ci_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff arith2.models.expected arith2.models_ci_cdcl_no_minimal_bj.output))) - (rule - (target arith2.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input arith2.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 CDCL-Tableaux - --no-minimal-bj - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps arith2.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff arith2.models.expected arith2.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target arith2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input arith2.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps arith2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff arith2.models.expected arith2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target arith2.models_ci_no_tableaux_cdcl_in_instantiation.output) - (deps (:input arith2.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 CDCL-Tableaux - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps arith2.models_ci_no_tableaux_cdcl_in_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff arith2.models.expected arith2.models_ci_no_tableaux_cdcl_in_instantiation.output))) +(subdir models/issues (rule - (target arith2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (deps (:input arith2.models.smt2)) + (target 719.models_tableaux.output) + (deps (:input 719.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192966,18 +192378,22 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver CDCL-Tableaux - --no-tableaux-cdcl-in-theories + --sat-solver Tableaux %{input}))))))) (rule - (deps arith2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (alias runtest-ci) + (deps 719.models_tableaux.output) + (alias runtest-quick) (package alt-ergo) (action - (diff arith2.models.expected arith2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) + (diff 719.models.expected 719.models_tableaux.output)))) +; Auto-generated part end +; File auto-generated by gentests + +; Auto-generated part begin +(subdir models/issues/715 (rule - (target arith2.models_ci_tableaux_cdcl_no_minimal_bj.output) - (deps (:input arith2.models.smt2)) + (target 715_2.models_tableaux.output) + (deps (:input 715_2.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192989,18 +192405,17 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver CDCL-Tableaux - --no-minimal-bj + --sat-solver Tableaux %{input}))))))) (rule - (deps arith2.models_ci_tableaux_cdcl_no_minimal_bj.output) - (alias runtest-ci) + (deps 715_2.models_tableaux.output) + (alias runtest-quick) (package alt-ergo) (action - (diff arith2.models.expected arith2.models_ci_tableaux_cdcl_no_minimal_bj.output))) + (diff 715_2.models.expected 715_2.models_tableaux.output))) (rule - (target arith2.models_cdcl.output) - (deps (:input arith2.models.smt2)) + (target 715_1.models_tableaux.output) + (deps (:input 715_1.models.ae)) (package alt-ergo) (action (chdir %{workspace_root} @@ -193012,17 +192427,22 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver CDCL + --sat-solver Tableaux %{input}))))))) (rule - (deps arith2.models_cdcl.output) + (deps 715_1.models_tableaux.output) (alias runtest-quick) (package alt-ergo) (action - (diff arith2.models.expected arith2.models_cdcl.output))) + (diff 715_1.models.expected 715_1.models_tableaux.output)))) +; Auto-generated part end +; File auto-generated by gentests + +; Auto-generated part begin +(subdir models/records (rule - (target arith2.models_tableaux_cdcl.output) - (deps (:input arith2.models.smt2)) + (target record1.models_tableaux.output) + (deps (:input record1.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -193034,17 +192454,22 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux-CDCL + --sat-solver Tableaux %{input}))))))) (rule - (deps arith2.models_tableaux_cdcl.output) + (deps record1.models_tableaux.output) (alias runtest-quick) (package alt-ergo) (action - (diff arith2.models.expected arith2.models_tableaux_cdcl.output))) + (diff record1.models.expected record1.models_tableaux.output)))) +; Auto-generated part end +; File auto-generated by gentests + +; Auto-generated part begin +(subdir models/uf (rule - (target arith2.models_tableaux.output) - (deps (:input arith2.models.smt2)) + (target uf2.models_tableaux.output) + (deps (:input uf2.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -193059,14 +192484,14 @@ --sat-solver Tableaux %{input}))))))) (rule - (deps arith2.models_tableaux.output) + (deps uf2.models_tableaux.output) (alias runtest-quick) (package alt-ergo) (action - (diff arith2.models.expected arith2.models_tableaux.output))) + (diff uf2.models.expected uf2.models_tableaux.output))) (rule - (target arith2.models_dolmen.output) - (deps (:input arith2.models.smt2)) + (target uf1.models_tableaux.output) + (deps (:input uf1.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -193078,2323 +192503,14 @@ --enable-assertions --output=smtlib2 --frontend dolmen - %{input}))))))) - (rule - (deps arith2.models_dolmen.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff arith2.models.expected arith2.models_dolmen.output))) - (rule - (target arith1.models_ci_cdcl_no_minimal_bj.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 CDCL - --no-minimal-bj - %{input}))))))) - (rule - (deps arith1.models_ci_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff arith1.models.expected arith1.models_ci_cdcl_no_minimal_bj.output))) - (rule - (target arith1.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.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 CDCL-Tableaux - --no-minimal-bj - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps arith1.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff arith1.models.expected arith1.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target arith1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps arith1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff arith1.models.expected arith1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target arith1.models_ci_no_tableaux_cdcl_in_instantiation.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 CDCL-Tableaux - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps arith1.models_ci_no_tableaux_cdcl_in_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff arith1.models.expected arith1.models_ci_no_tableaux_cdcl_in_instantiation.output))) - (rule - (target arith1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - %{input}))))))) - (rule - (deps arith1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff arith1.models.expected arith1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) - (rule - (target arith1.models_ci_tableaux_cdcl_no_minimal_bj.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 CDCL-Tableaux - --no-minimal-bj - %{input}))))))) - (rule - (deps arith1.models_ci_tableaux_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff arith1.models.expected arith1.models_ci_tableaux_cdcl_no_minimal_bj.output))) - (rule - (target arith1.models_cdcl.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 CDCL - %{input}))))))) - (rule - (deps arith1.models_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff arith1.models.expected arith1.models_cdcl.output))) - (rule - (target arith1.models_tableaux_cdcl.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-CDCL - %{input}))))))) - (rule - (deps arith1.models_tableaux_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff arith1.models.expected arith1.models_tableaux_cdcl.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))) - (rule - (target arith1.models_dolmen.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 - %{input}))))))) - (rule - (deps arith1.models_dolmen.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff arith1.models.expected arith1.models_dolmen.output)))) -; Auto-generated part end -; File auto-generated by gentests - -; Auto-generated part begin -(subdir models/array - (rule - (target array1.models_ci_cdcl_no_minimal_bj.output) - (deps (:input array1.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 CDCL - --no-minimal-bj - %{input}))))))) - (rule - (deps array1.models_ci_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff array1.models.expected array1.models_ci_cdcl_no_minimal_bj.output))) - (rule - (target array1.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input array1.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 CDCL-Tableaux - --no-minimal-bj - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps array1.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff array1.models.expected array1.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target array1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input array1.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps array1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff array1.models.expected array1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target array1.models_ci_no_tableaux_cdcl_in_instantiation.output) - (deps (:input array1.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 CDCL-Tableaux - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps array1.models_ci_no_tableaux_cdcl_in_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff array1.models.expected array1.models_ci_no_tableaux_cdcl_in_instantiation.output))) - (rule - (target array1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (deps (:input array1.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - %{input}))))))) - (rule - (deps array1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff array1.models.expected array1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) - (rule - (target array1.models_ci_tableaux_cdcl_no_minimal_bj.output) - (deps (:input array1.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 CDCL-Tableaux - --no-minimal-bj - %{input}))))))) - (rule - (deps array1.models_ci_tableaux_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff array1.models.expected array1.models_ci_tableaux_cdcl_no_minimal_bj.output))) - (rule - (target array1.models_cdcl.output) - (deps (:input array1.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 CDCL - %{input}))))))) - (rule - (deps array1.models_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff array1.models.expected array1.models_cdcl.output))) - (rule - (target array1.models_tableaux_cdcl.output) - (deps (:input array1.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-CDCL - %{input}))))))) - (rule - (deps array1.models_tableaux_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff array1.models.expected array1.models_tableaux_cdcl.output))) - (rule - (target array1.models_tableaux.output) - (deps (:input array1.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 array1.models_tableaux.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff array1.models.expected array1.models_tableaux.output))) - (rule - (target array1.models_dolmen.output) - (deps (:input array1.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 - %{input}))))))) - (rule - (deps array1.models_dolmen.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff array1.models.expected array1.models_dolmen.output)))) -; Auto-generated part end -; File auto-generated by gentests - -; Auto-generated part begin -(subdir models/bool - (rule - (target bool2.models_ci_cdcl_no_minimal_bj.output) - (deps (:input bool2.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 CDCL - --no-minimal-bj - %{input}))))))) - (rule - (deps bool2.models_ci_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff bool2.models.expected bool2.models_ci_cdcl_no_minimal_bj.output))) - (rule - (target bool2.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input bool2.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 CDCL-Tableaux - --no-minimal-bj - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps bool2.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff bool2.models.expected bool2.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target bool2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input bool2.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps bool2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff bool2.models.expected bool2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target bool2.models_ci_no_tableaux_cdcl_in_instantiation.output) - (deps (:input bool2.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 CDCL-Tableaux - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps bool2.models_ci_no_tableaux_cdcl_in_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff bool2.models.expected bool2.models_ci_no_tableaux_cdcl_in_instantiation.output))) - (rule - (target bool2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (deps (:input bool2.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - %{input}))))))) - (rule - (deps bool2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff bool2.models.expected bool2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) - (rule - (target bool2.models_ci_tableaux_cdcl_no_minimal_bj.output) - (deps (:input bool2.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 CDCL-Tableaux - --no-minimal-bj - %{input}))))))) - (rule - (deps bool2.models_ci_tableaux_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff bool2.models.expected bool2.models_ci_tableaux_cdcl_no_minimal_bj.output))) - (rule - (target bool2.models_cdcl.output) - (deps (:input bool2.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 CDCL - %{input}))))))) - (rule - (deps bool2.models_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff bool2.models.expected bool2.models_cdcl.output))) - (rule - (target bool2.models_tableaux_cdcl.output) - (deps (:input bool2.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-CDCL - %{input}))))))) - (rule - (deps bool2.models_tableaux_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff bool2.models.expected bool2.models_tableaux_cdcl.output))) - (rule - (target bool2.models_tableaux.output) - (deps (:input bool2.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 bool2.models_tableaux.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff bool2.models.expected bool2.models_tableaux.output))) - (rule - (target bool2.models_dolmen.output) - (deps (:input bool2.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 - %{input}))))))) - (rule - (deps bool2.models_dolmen.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff bool2.models.expected bool2.models_dolmen.output))) - (rule - (target bool1.models_ci_cdcl_no_minimal_bj.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 CDCL - --no-minimal-bj - %{input}))))))) - (rule - (deps bool1.models_ci_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff bool1.models.expected bool1.models_ci_cdcl_no_minimal_bj.output))) - (rule - (target bool1.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.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 CDCL-Tableaux - --no-minimal-bj - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps bool1.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff bool1.models.expected bool1.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target bool1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps bool1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff bool1.models.expected bool1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target bool1.models_ci_no_tableaux_cdcl_in_instantiation.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 CDCL-Tableaux - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps bool1.models_ci_no_tableaux_cdcl_in_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff bool1.models.expected bool1.models_ci_no_tableaux_cdcl_in_instantiation.output))) - (rule - (target bool1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - %{input}))))))) - (rule - (deps bool1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff bool1.models.expected bool1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) - (rule - (target bool1.models_ci_tableaux_cdcl_no_minimal_bj.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 CDCL-Tableaux - --no-minimal-bj - %{input}))))))) - (rule - (deps bool1.models_ci_tableaux_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff bool1.models.expected bool1.models_ci_tableaux_cdcl_no_minimal_bj.output))) - (rule - (target bool1.models_cdcl.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 CDCL - %{input}))))))) - (rule - (deps bool1.models_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff bool1.models.expected bool1.models_cdcl.output))) - (rule - (target bool1.models_tableaux_cdcl.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-CDCL - %{input}))))))) - (rule - (deps bool1.models_tableaux_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff bool1.models.expected bool1.models_tableaux_cdcl.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))) - (rule - (target bool1.models_dolmen.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 - %{input}))))))) - (rule - (deps bool1.models_dolmen.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff bool1.models.expected bool1.models_dolmen.output)))) -; Auto-generated part end -; File auto-generated by gentests - -; Auto-generated part begin -(subdir models/issues - (rule - (target 719.models_ci_cdcl_no_minimal_bj.output) - (deps (:input 719.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 CDCL - --no-minimal-bj - %{input}))))))) - (rule - (deps 719.models_ci_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 719.models.expected 719.models_ci_cdcl_no_minimal_bj.output))) - (rule - (target 719.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input 719.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 CDCL-Tableaux - --no-minimal-bj - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 719.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 719.models.expected 719.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target 719.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input 719.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 719.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 719.models.expected 719.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target 719.models_ci_no_tableaux_cdcl_in_instantiation.output) - (deps (:input 719.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 CDCL-Tableaux - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 719.models_ci_no_tableaux_cdcl_in_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 719.models.expected 719.models_ci_no_tableaux_cdcl_in_instantiation.output))) - (rule - (target 719.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (deps (:input 719.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - %{input}))))))) - (rule - (deps 719.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 719.models.expected 719.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) - (rule - (target 719.models_ci_tableaux_cdcl_no_minimal_bj.output) - (deps (:input 719.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 CDCL-Tableaux - --no-minimal-bj - %{input}))))))) - (rule - (deps 719.models_ci_tableaux_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 719.models.expected 719.models_ci_tableaux_cdcl_no_minimal_bj.output))) - (rule - (target 719.models_cdcl.output) - (deps (:input 719.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 CDCL - %{input}))))))) - (rule - (deps 719.models_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 719.models.expected 719.models_cdcl.output))) - (rule - (target 719.models_tableaux_cdcl.output) - (deps (:input 719.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-CDCL - %{input}))))))) - (rule - (deps 719.models_tableaux_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 719.models.expected 719.models_tableaux_cdcl.output))) - (rule - (target 719.models_tableaux.output) - (deps (:input 719.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 719.models_tableaux.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 719.models.expected 719.models_tableaux.output))) - (rule - (target 719.models_dolmen.output) - (deps (:input 719.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 - %{input}))))))) - (rule - (deps 719.models_dolmen.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 719.models.expected 719.models_dolmen.output)))) -; Auto-generated part end -; File auto-generated by gentests - -; Auto-generated part begin -(subdir models/issues/715 - (rule - (target 715_2.models_ci_cdcl_no_minimal_bj.output) - (deps (:input 715_2.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 CDCL - --no-minimal-bj - %{input}))))))) - (rule - (deps 715_2.models_ci_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 715_2.models.expected 715_2.models_ci_cdcl_no_minimal_bj.output))) - (rule - (target 715_2.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input 715_2.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 CDCL-Tableaux - --no-minimal-bj - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 715_2.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 715_2.models.expected 715_2.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target 715_2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input 715_2.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 715_2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 715_2.models.expected 715_2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target 715_2.models_ci_no_tableaux_cdcl_in_instantiation.output) - (deps (:input 715_2.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 CDCL-Tableaux - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 715_2.models_ci_no_tableaux_cdcl_in_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 715_2.models.expected 715_2.models_ci_no_tableaux_cdcl_in_instantiation.output))) - (rule - (target 715_2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (deps (:input 715_2.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - %{input}))))))) - (rule - (deps 715_2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 715_2.models.expected 715_2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) - (rule - (target 715_2.models_ci_tableaux_cdcl_no_minimal_bj.output) - (deps (:input 715_2.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 CDCL-Tableaux - --no-minimal-bj - %{input}))))))) - (rule - (deps 715_2.models_ci_tableaux_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 715_2.models.expected 715_2.models_ci_tableaux_cdcl_no_minimal_bj.output))) - (rule - (target 715_2.models_cdcl.output) - (deps (:input 715_2.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 CDCL - %{input}))))))) - (rule - (deps 715_2.models_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 715_2.models.expected 715_2.models_cdcl.output))) - (rule - (target 715_2.models_tableaux_cdcl.output) - (deps (:input 715_2.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-CDCL - %{input}))))))) - (rule - (deps 715_2.models_tableaux_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 715_2.models.expected 715_2.models_tableaux_cdcl.output))) - (rule - (target 715_2.models_tableaux.output) - (deps (:input 715_2.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 715_2.models_tableaux.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 715_2.models.expected 715_2.models_tableaux.output))) - (rule - (target 715_2.models_dolmen.output) - (deps (:input 715_2.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 - %{input}))))))) - (rule - (deps 715_2.models_dolmen.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 715_2.models.expected 715_2.models_dolmen.output))) - (rule - (target 715_1.models_ci_cdcl_no_minimal_bj.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 CDCL - --no-minimal-bj - %{input}))))))) - (rule - (deps 715_1.models_ci_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 715_1.models.expected 715_1.models_ci_cdcl_no_minimal_bj.output))) - (rule - (target 715_1.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.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 CDCL-Tableaux - --no-minimal-bj - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 715_1.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 715_1.models.expected 715_1.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target 715_1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 715_1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 715_1.models.expected 715_1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target 715_1.models_ci_no_tableaux_cdcl_in_instantiation.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 CDCL-Tableaux - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps 715_1.models_ci_no_tableaux_cdcl_in_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 715_1.models.expected 715_1.models_ci_no_tableaux_cdcl_in_instantiation.output))) - (rule - (target 715_1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - %{input}))))))) - (rule - (deps 715_1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 715_1.models.expected 715_1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) - (rule - (target 715_1.models_ci_tableaux_cdcl_no_minimal_bj.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 CDCL-Tableaux - --no-minimal-bj - %{input}))))))) - (rule - (deps 715_1.models_ci_tableaux_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff 715_1.models.expected 715_1.models_ci_tableaux_cdcl_no_minimal_bj.output))) - (rule - (target 715_1.models_cdcl.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 CDCL - %{input}))))))) - (rule - (deps 715_1.models_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 715_1.models.expected 715_1.models_cdcl.output))) - (rule - (target 715_1.models_tableaux_cdcl.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-CDCL - %{input}))))))) - (rule - (deps 715_1.models_tableaux_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 715_1.models.expected 715_1.models_tableaux_cdcl.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))) - (rule - (target 715_1.models_dolmen.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 - %{input}))))))) - (rule - (deps 715_1.models_dolmen.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff 715_1.models.expected 715_1.models_dolmen.output)))) -; Auto-generated part end -; File auto-generated by gentests - -; Auto-generated part begin -(subdir models/records - (rule - (target record1.models_ci_cdcl_no_minimal_bj.output) - (deps (:input record1.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 CDCL - --no-minimal-bj - %{input}))))))) - (rule - (deps record1.models_ci_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff record1.models.expected record1.models_ci_cdcl_no_minimal_bj.output))) - (rule - (target record1.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input record1.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 CDCL-Tableaux - --no-minimal-bj - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps record1.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff record1.models.expected record1.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target record1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input record1.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps record1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff record1.models.expected record1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target record1.models_ci_no_tableaux_cdcl_in_instantiation.output) - (deps (:input record1.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 CDCL-Tableaux - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps record1.models_ci_no_tableaux_cdcl_in_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff record1.models.expected record1.models_ci_no_tableaux_cdcl_in_instantiation.output))) - (rule - (target record1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (deps (:input record1.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - %{input}))))))) - (rule - (deps record1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff record1.models.expected record1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) - (rule - (target record1.models_ci_tableaux_cdcl_no_minimal_bj.output) - (deps (:input record1.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 CDCL-Tableaux - --no-minimal-bj - %{input}))))))) - (rule - (deps record1.models_ci_tableaux_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff record1.models.expected record1.models_ci_tableaux_cdcl_no_minimal_bj.output))) - (rule - (target record1.models_cdcl.output) - (deps (:input record1.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 CDCL - %{input}))))))) - (rule - (deps record1.models_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff record1.models.expected record1.models_cdcl.output))) - (rule - (target record1.models_tableaux_cdcl.output) - (deps (:input record1.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-CDCL - %{input}))))))) - (rule - (deps record1.models_tableaux_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff record1.models.expected record1.models_tableaux_cdcl.output))) - (rule - (target record1.models_tableaux.output) - (deps (:input record1.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 record1.models_tableaux.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff record1.models.expected record1.models_tableaux.output))) - (rule - (target record1.models_dolmen.output) - (deps (:input record1.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 - %{input}))))))) - (rule - (deps record1.models_dolmen.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff record1.models.expected record1.models_dolmen.output)))) -; Auto-generated part end -; File auto-generated by gentests - -; Auto-generated part begin -(subdir models/uf - (rule - (target uf2.models_ci_cdcl_no_minimal_bj.output) - (deps (:input uf2.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 CDCL - --no-minimal-bj - %{input}))))))) - (rule - (deps uf2.models_ci_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff uf2.models.expected uf2.models_ci_cdcl_no_minimal_bj.output))) - (rule - (target uf2.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input uf2.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 CDCL-Tableaux - --no-minimal-bj - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps uf2.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff uf2.models.expected uf2.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target uf2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (deps (:input uf2.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps uf2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff uf2.models.expected uf2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target uf2.models_ci_no_tableaux_cdcl_in_instantiation.output) - (deps (:input uf2.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 CDCL-Tableaux - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps uf2.models_ci_no_tableaux_cdcl_in_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff uf2.models.expected uf2.models_ci_no_tableaux_cdcl_in_instantiation.output))) - (rule - (target uf2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (deps (:input uf2.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - %{input}))))))) - (rule - (deps uf2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff uf2.models.expected uf2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) - (rule - (target uf2.models_ci_tableaux_cdcl_no_minimal_bj.output) - (deps (:input uf2.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 CDCL-Tableaux - --no-minimal-bj - %{input}))))))) - (rule - (deps uf2.models_ci_tableaux_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff uf2.models.expected uf2.models_ci_tableaux_cdcl_no_minimal_bj.output))) - (rule - (target uf2.models_cdcl.output) - (deps (:input uf2.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 CDCL - %{input}))))))) - (rule - (deps uf2.models_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff uf2.models.expected uf2.models_cdcl.output))) - (rule - (target uf2.models_tableaux_cdcl.output) - (deps (:input uf2.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-CDCL - %{input}))))))) - (rule - (deps uf2.models_tableaux_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff uf2.models.expected uf2.models_tableaux_cdcl.output))) - (rule - (target uf2.models_tableaux.output) - (deps (:input uf2.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 uf2.models_tableaux.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff uf2.models.expected uf2.models_tableaux.output))) - (rule - (target uf2.models_dolmen.output) - (deps (:input uf2.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 - %{input}))))))) - (rule - (deps uf2.models_dolmen.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff uf2.models.expected uf2.models_dolmen.output))) - (rule - (target uf1.models_ci_cdcl_no_minimal_bj.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 CDCL - --no-minimal-bj - %{input}))))))) - (rule - (deps uf1.models_ci_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff uf1.models.expected uf1.models_ci_cdcl_no_minimal_bj.output))) - (rule - (target uf1.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.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 CDCL-Tableaux - --no-minimal-bj - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps uf1.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff uf1.models.expected uf1.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target uf1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps uf1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff uf1.models.expected uf1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) - (rule - (target uf1.models_ci_no_tableaux_cdcl_in_instantiation.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 CDCL-Tableaux - --no-tableaux-cdcl-in-instantiation - %{input}))))))) - (rule - (deps uf1.models_ci_no_tableaux_cdcl_in_instantiation.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff uf1.models.expected uf1.models_ci_no_tableaux_cdcl_in_instantiation.output))) - (rule - (target uf1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.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 CDCL-Tableaux - --no-tableaux-cdcl-in-theories - %{input}))))))) - (rule - (deps uf1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff uf1.models.expected uf1.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) - (rule - (target uf1.models_ci_tableaux_cdcl_no_minimal_bj.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 CDCL-Tableaux - --no-minimal-bj - %{input}))))))) - (rule - (deps uf1.models_ci_tableaux_cdcl_no_minimal_bj.output) - (alias runtest-ci) - (package alt-ergo) - (action - (diff uf1.models.expected uf1.models_ci_tableaux_cdcl_no_minimal_bj.output))) - (rule - (target uf1.models_cdcl.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 CDCL - %{input}))))))) - (rule - (deps uf1.models_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff uf1.models.expected uf1.models_cdcl.output))) - (rule - (target uf1.models_tableaux_cdcl.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-CDCL - %{input}))))))) - (rule - (deps uf1.models_tableaux_cdcl.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff uf1.models.expected uf1.models_tableaux_cdcl.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 + --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 - (target uf1.models_dolmen.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 - %{input}))))))) - (rule - (deps uf1.models_dolmen.output) - (alias runtest-quick) - (package alt-ergo) - (action - (diff uf1.models.expected uf1.models_dolmen.output)))) + (diff uf1.models.expected uf1.models_tableaux.output)))) ; Auto-generated part end ; File auto-generated by gentests diff --git a/tools/gentest.ml b/tools/gentest.ml index 04cbfb872..92181b68a 100644 --- a/tools/gentest.ml +++ b/tools/gentest.ml @@ -220,7 +220,7 @@ end = struct should_succeed | "models" -> "legacy" :: "fpa" :: exclude, - filters_opt, + Some ["tableaux"], should_succeed | "fpa" -> exclude,