From 4a36e432aa9a6e4c274d7530ff1d4a6d8f49da5c Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Tue, 23 May 2023 21:44:05 +0200
Subject: [PATCH] [verification] Add other cases which abcrown may be used for.
---
src/verification.ml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/verification.ml b/src/verification.ml
index 860a969..dda279e 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 ->
--
GitLab