diff --git a/src/verification.ml b/src/verification.ml index 860a96948eb65f5e6d80636e1a57e212cee6c3b7..dda279e25450552e858d16965c5abb978f978d90 100644 --- a/src/verification.ml +++ b/src/verification.ml @@ -240,7 +240,7 @@ let answer_generic limit config env prover config_prover driver ~proof_strategy tasks. *) match prover with | Prover.Marabou -> Trans.apply Split.split_all task - | Pyrat | Nnenum -> Trans.apply Split.split_premises task + | Pyrat | Nnenum | ABCrown -> Trans.apply Split.split_premises task | _ -> [ task ] in let command = @@ -259,7 +259,7 @@ let call_prover ~cwd ~limit config env prover config_prover driver ?dataset task match prover with | Prover.Saver -> answer_saver limit config env config_prover dataset task | Aimos -> answer_aimos limit config env config_prover dataset task - | (Marabou | Pyrat | Nnenum) when Option.is_some dataset -> + | (Marabou | Pyrat | Nnenum | ABCrown) when Option.is_some dataset -> let dataset = Unix.realpath (Option.value_exn dataset) in answer_dataset limit config env prover config_prover driver dataset task | Marabou | Pyrat | Nnenum | ABCrown ->