diff --git a/tests/dune.inc b/tests/dune.inc index 3d4a7d522b..1e65836d95 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -175626,6 +175626,191 @@ ; 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)) @@ -175648,6 +175833,27 @@ (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)) @@ -176459,31 +176665,9 @@ (action (diff 645.expected 645_fpa.output))) (rule - (target 555.models_tableaux.output) + (target 555.models_ci_cdcl_no_minimal_bj.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} @@ -176498,14 +176682,14 @@ --no-minimal-bj %{input}))))))) (rule - (deps 479_ci_cdcl_no_minimal_bj.output) + (deps 555.models_ci_cdcl_no_minimal_bj.output) (alias runtest-ci) (package alt-ergo) (action - (diff 479.expected 479_ci_cdcl_no_minimal_bj.output))) + (diff 555.models.expected 555.models_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)) + (target 555.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 555.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -176523,14 +176707,14 @@ --no-tableaux-cdcl-in-instantiation %{input}))))))) (rule - (deps 479_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps 555.models_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))) + (diff 555.models.expected 555.models_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)) + (target 555.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 555.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -176547,14 +176731,14 @@ --no-tableaux-cdcl-in-instantiation %{input}))))))) (rule - (deps 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps 555.models_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))) + (diff 555.models.expected 555.models_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)) + (target 555.models_ci_no_tableaux_cdcl_in_instantiation.output) + (deps (:input 555.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -176570,14 +176754,14 @@ --no-tableaux-cdcl-in-instantiation %{input}))))))) (rule - (deps 479_ci_no_tableaux_cdcl_in_instantiation.output) + (deps 555.models_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))) + (diff 555.models.expected 555.models_ci_no_tableaux_cdcl_in_instantiation.output))) (rule - (target 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) - (deps (:input 479.smt2)) + (target 555.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (deps (:input 555.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -176593,14 +176777,14 @@ --no-tableaux-cdcl-in-theories %{input}))))))) (rule - (deps 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (deps 555.models_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))) + (diff 555.models.expected 555.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) (rule - (target 479_ci_tableaux_cdcl_no_minimal_bj.output) - (deps (:input 479.smt2)) + (target 555.models_ci_tableaux_cdcl_no_minimal_bj.output) + (deps (:input 555.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -176616,14 +176800,14 @@ --no-minimal-bj %{input}))))))) (rule - (deps 479_ci_tableaux_cdcl_no_minimal_bj.output) + (deps 555.models_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))) + (diff 555.models.expected 555.models_ci_tableaux_cdcl_no_minimal_bj.output))) (rule - (target 479_cdcl.output) - (deps (:input 479.smt2)) + (target 555.models_cdcl.output) + (deps (:input 555.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -176638,14 +176822,14 @@ --sat-solver CDCL %{input}))))))) (rule - (deps 479_cdcl.output) + (deps 555.models_cdcl.output) (alias runtest-quick) (package alt-ergo) (action - (diff 479.expected 479_cdcl.output))) + (diff 555.models.expected 555.models_cdcl.output))) (rule - (target 479_tableaux_cdcl.output) - (deps (:input 479.smt2)) + (target 555.models_tableaux_cdcl.output) + (deps (:input 555.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -176660,14 +176844,14 @@ --sat-solver Tableaux-CDCL %{input}))))))) (rule - (deps 479_tableaux_cdcl.output) + (deps 555.models_tableaux_cdcl.output) (alias runtest-quick) (package alt-ergo) (action - (diff 479.expected 479_tableaux_cdcl.output))) + (diff 555.models.expected 555.models_tableaux_cdcl.output))) (rule - (target 479_tableaux.output) - (deps (:input 479.smt2)) + (target 555.models_tableaux.output) + (deps (:input 555.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -176682,14 +176866,14 @@ --sat-solver Tableaux %{input}))))))) (rule - (deps 479_tableaux.output) + (deps 555.models_tableaux.output) (alias runtest-quick) (package alt-ergo) (action - (diff 479.expected 479_tableaux.output))) + (diff 555.models.expected 555.models_tableaux.output))) (rule - (target 479_legacy.output) - (deps (:input 479.smt2)) + (target 555.models_dolmen.output) + (deps (:input 555.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -176700,16 +176884,244 @@ --timelimit=2 --enable-assertions --output=smtlib2 - --frontend legacy + --frontend dolmen %{input}))))))) (rule - (deps 479_legacy.output) + (deps 555.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff 479.expected 479_legacy.output))) + (diff 555.models.expected 555.models_dolmen.output))) (rule - (target 479_dolmen.output) + (target 479_ci_cdcl_no_minimal_bj.output) + (deps (:input 479.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + --no-minimal-bj + %{input}))))))) + (rule + (deps 479_ci_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 479.expected 479_ci_cdcl_no_minimal_bj.output))) + (rule + (target 479_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 479.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (deps 479_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 479.expected 479_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (rule + (target 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 479.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (deps 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 479.expected 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (rule + (target 479_ci_no_tableaux_cdcl_in_instantiation.output) + (deps (:input 479.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (deps 479_ci_no_tableaux_cdcl_in_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 479.expected 479_ci_no_tableaux_cdcl_in_instantiation.output))) + (rule + (target 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (deps (:input 479.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + %{input}))))))) + (rule + (deps 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 479.expected 479_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) + (rule + (target 479_ci_tableaux_cdcl_no_minimal_bj.output) + (deps (:input 479.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + %{input}))))))) + (rule + (deps 479_ci_tableaux_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff 479.expected 479_ci_tableaux_cdcl_no_minimal_bj.output))) + (rule + (target 479_cdcl.output) + (deps (:input 479.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + %{input}))))))) + (rule + (deps 479_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 479.expected 479_cdcl.output))) + (rule + (target 479_tableaux_cdcl.output) + (deps (:input 479.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux-CDCL + %{input}))))))) + (rule + (deps 479_tableaux_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 479.expected 479_tableaux_cdcl.output))) + (rule + (target 479_tableaux.output) + (deps (:input 479.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) + (rule + (deps 479_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 479.expected 479_tableaux.output))) + (rule + (target 479_legacy.output) + (deps (:input 479.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend legacy + %{input}))))))) + (rule + (deps 479_legacy.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff 479.expected 479_legacy.output))) + (rule + (target 479_dolmen.output) (deps (:input 479.smt2)) (package alt-ergo) (action @@ -192213,7 +192625,7 @@ ; Auto-generated part begin (subdir models (rule - (target check_sat.models_tableaux.output) + (target check_sat.models_ci_cdcl_no_minimal_bj.output) (deps (:input check_sat.models.ae)) (package alt-ergo) (action @@ -192226,22 +192638,18 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux + --sat-solver CDCL + --no-minimal-bj %{input}))))))) (rule - (deps check_sat.models_tableaux.output) - (alias runtest-quick) + (deps check_sat.models_ci_cdcl_no_minimal_bj.output) + (alias runtest-ci) (package alt-ergo) (action - (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 + (diff check_sat.models.expected check_sat.models_ci_cdcl_no_minimal_bj.output))) (rule - (target arith2.models_tableaux.output) - (deps (:input arith2.models.smt2)) + (target check_sat.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input check_sat.models.ae)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192253,17 +192661,20 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux + --sat-solver CDCL-Tableaux + --no-minimal-bj + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation %{input}))))))) (rule - (deps arith2.models_tableaux.output) - (alias runtest-quick) + (deps check_sat.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_tableaux.output))) + (diff check_sat.models.expected check_sat.models_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) (rule - (target arith1.models_tableaux.output) - (deps (:input arith1.models.smt2)) + (target check_sat.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input check_sat.models.ae)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192275,22 +192686,19 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation %{input}))))))) (rule - (deps arith1.models_tableaux.output) - (alias runtest-quick) + (deps check_sat.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_tableaux.output)))) -; Auto-generated part end -; File auto-generated by gentests - -; Auto-generated part begin -(subdir models/bool + (diff check_sat.models.expected check_sat.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) (rule - (target bool2.models_tableaux.output) - (deps (:input bool2.models.smt2)) + (target check_sat.models_ci_no_tableaux_cdcl_in_instantiation.output) + (deps (:input check_sat.models.ae)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192302,17 +192710,18 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-instantiation %{input}))))))) (rule - (deps bool2.models_tableaux.output) - (alias runtest-quick) + (deps check_sat.models_ci_no_tableaux_cdcl_in_instantiation.output) + (alias runtest-ci) (package alt-ergo) (action - (diff bool2.models.expected bool2.models_tableaux.output))) + (diff check_sat.models.expected check_sat.models_ci_no_tableaux_cdcl_in_instantiation.output))) (rule - (target bool1.models_tableaux.output) - (deps (:input bool1.models.smt2)) + (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} @@ -192324,22 +192733,63 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories %{input}))))))) (rule - (deps bool1.models_tableaux.output) + (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 + %{input}))))))) + (rule + (deps check_sat.models_cdcl.output) (alias runtest-quick) (package alt-ergo) (action - (diff bool1.models.expected bool1.models_tableaux.output)))) -; Auto-generated part end -; File auto-generated by gentests - -; Auto-generated part begin -(subdir models/issues + (diff check_sat.models.expected check_sat.models_cdcl.output))) (rule - (target 719.models_tableaux.output) - (deps (:input 719.models.smt2)) + (target check_sat.models_tableaux_cdcl.output) + (deps (:input check_sat.models.ae)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192351,22 +192801,17 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux + --sat-solver Tableaux-CDCL %{input}))))))) (rule - (deps 719.models_tableaux.output) + (deps check_sat.models_tableaux_cdcl.output) (alias runtest-quick) (package alt-ergo) (action - (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 + (diff check_sat.models.expected check_sat.models_tableaux_cdcl.output))) (rule - (target 715_2.models_tableaux.output) - (deps (:input 715_2.models.smt2)) + (target check_sat.models_tableaux.output) + (deps (:input check_sat.models.ae)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192381,14 +192826,14 @@ --sat-solver Tableaux %{input}))))))) (rule - (deps 715_2.models_tableaux.output) + (deps check_sat.models_tableaux.output) (alias runtest-quick) (package alt-ergo) (action - (diff 715_2.models.expected 715_2.models_tableaux.output))) + (diff check_sat.models.expected check_sat.models_tableaux.output))) (rule - (target 715_1.models_tableaux.output) - (deps (:input 715_1.models.ae)) + (target check_sat.models_dolmen.output) + (deps (:input check_sat.models.ae)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192400,22 +192845,21 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux %{input}))))))) (rule - (deps 715_1.models_tableaux.output) + (deps check_sat.models_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff 715_1.models.expected 715_1.models_tableaux.output)))) + (diff check_sat.models.expected check_sat.models_dolmen.output)))) ; Auto-generated part end ; File auto-generated by gentests ; Auto-generated part begin -(subdir models/records +(subdir models/arith (rule - (target record1.models_tableaux.output) - (deps (:input record1.models.smt2)) + (target arith2.models_ci_cdcl_no_minimal_bj.output) + (deps (:input arith2.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192427,22 +192871,158 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux + --sat-solver CDCL + --no-minimal-bj %{input}))))))) (rule - (deps record1.models_tableaux.output) + (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))) + (rule + (target arith2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.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 + %{input}))))))) + (rule + (deps arith2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff arith2.models.expected arith2.models_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) + (rule + (target arith2.models_ci_tableaux_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-Tableaux + --no-minimal-bj + %{input}))))))) + (rule + (deps arith2.models_ci_tableaux_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff arith2.models.expected arith2.models_ci_tableaux_cdcl_no_minimal_bj.output))) + (rule + (target arith2.models_cdcl.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 + %{input}))))))) + (rule + (deps arith2.models_cdcl.output) (alias runtest-quick) (package alt-ergo) (action - (diff record1.models.expected record1.models_tableaux.output)))) -; Auto-generated part end -; File auto-generated by gentests - -; Auto-generated part begin -(subdir models/uf + (diff arith2.models.expected arith2.models_cdcl.output))) (rule - (target uf2.models_tableaux.output) - (deps (:input uf2.models.smt2)) + (target arith2.models_tableaux_cdcl.output) + (deps (:input arith2.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192454,17 +193034,17 @@ --enable-assertions --output=smtlib2 --frontend dolmen - --sat-solver Tableaux + --sat-solver Tableaux-CDCL %{input}))))))) (rule - (deps uf2.models_tableaux.output) + (deps arith2.models_tableaux_cdcl.output) (alias runtest-quick) (package alt-ergo) (action - (diff uf2.models.expected uf2.models_tableaux.output))) + (diff arith2.models.expected arith2.models_tableaux_cdcl.output))) (rule - (target uf1.models_tableaux.output) - (deps (:input uf1.models.smt2)) + (target arith2.models_tableaux.output) + (deps (:input arith2.models.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -192479,11 +193059,2109 @@ --sat-solver Tableaux %{input}))))))) (rule - (deps uf1.models_tableaux.output) + (deps arith2.models_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff arith2.models.expected arith2.models_tableaux.output))) + (rule + (target arith2.models_dolmen.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 + %{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/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 + %{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_tableaux.output)))) + (diff uf1.models.expected uf1.models_dolmen.output)))) ; Auto-generated part end ; File auto-generated by gentests diff --git a/tools/gentest.ml b/tools/gentest.ml index 7938a7847f..04cbfb872e 100644 --- a/tools/gentest.ml +++ b/tools/gentest.ml @@ -219,8 +219,8 @@ end = struct Some ["dolmen"], should_succeed | "models" -> - exclude, - Some ["tableaux"], + "legacy" :: "fpa" :: exclude, + filters_opt, should_succeed | "fpa" -> exclude,