diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test.ml b/src/plugins/wp/tests/wp/stmtcompiler_test.ml index ab8fd28f71adf5fe5a631056ae2ad39533d5a421..e104a2e5c46ffcf840cd1aa225581605ace3763d 100644 --- a/src/plugins/wp/tests/wp/stmtcompiler_test.ml +++ b/src/plugins/wp/tests/wp/stmtcompiler_test.ml @@ -22,7 +22,7 @@ let run () = (fun pname prvs -> match VCS.parse_prover pname with | None -> prvs | Some VCS.Tactical -> prvs - | Some prv -> (VCS.BatchMode, prv) :: prvs) + | Some prv -> (VCS.Batch, prv) :: prvs) ["qed"] [] in diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml index ee5548356cc7a0037c3bc2f56dd2c86f7b62b228..9770e9b429591c4fd76ac2b451398371b0909a64 100644 --- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml +++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml @@ -21,7 +21,7 @@ let run () = (fun pname prvs -> match VCS.parse_prover pname with | None -> prvs | Some VCS.Tactical -> prvs - | Some prv -> (VCS.BatchMode, prv) :: prvs) + | Some prv -> (VCS.Batch, prv) :: prvs) ["alt-ergo"] [] in