Commit ca099b36 authored by Sylvain Dailler's avatar Sylvain Dailler

fix #282

Replace split_all_full by split_vc as first transformation used by Auto
parent e58d9baf
...@@ -352,7 +352,7 @@ let generate_auto_strategies config = ...@@ -352,7 +352,7 @@ let generate_auto_strategies config =
in in
fprintf str_formatter "start:@\n"; fprintf str_formatter "start:@\n";
List.iter (fun s -> fprintf str_formatter "c %s 1 1000@\n" s) provers_level1; List.iter (fun s -> fprintf str_formatter "c %s 1 1000@\n" s) provers_level1;
fprintf str_formatter "t split_all_full start@\n"; fprintf str_formatter "t split_vc start@\n";
List.iter (fun s -> fprintf str_formatter "c %s 10 4000@\n" s) provers_level1; List.iter (fun s -> fprintf str_formatter "c %s 10 4000@\n" s) provers_level1;
let code = flush_str_formatter () in let code = flush_str_formatter () in
let auto1 = { let auto1 = {
...@@ -371,7 +371,7 @@ let generate_auto_strategies config = ...@@ -371,7 +371,7 @@ let generate_auto_strategies config =
in in
fprintf str_formatter "start:@\n"; fprintf str_formatter "start:@\n";
List.iter (fun s -> fprintf str_formatter "c %s 1 1000@\n" s) provers_level2; List.iter (fun s -> fprintf str_formatter "c %s 1 1000@\n" s) provers_level2;
fprintf str_formatter "t split_all_full start@\n"; fprintf str_formatter "t split_vc start@\n";
List.iter (fun s -> fprintf str_formatter "c %s 5 2000@\n" s) provers_level2; List.iter (fun s -> fprintf str_formatter "c %s 5 2000@\n" s) provers_level2;
fprintf str_formatter "t introduce_premises afterintro@\n"; fprintf str_formatter "t introduce_premises afterintro@\n";
fprintf str_formatter "afterintro:@\n"; fprintf str_formatter "afterintro:@\n";
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment