diff --git a/config/abcrown/acasxu.yaml b/config/abcrown/acasxu.yaml
new file mode 100644
index 0000000000000000000000000000000000000000..22d1141cdfff58bc5ce8ee42717c49ce66ce4474
--- /dev/null
+++ b/config/abcrown/acasxu.yaml
@@ -0,0 +1,27 @@
+# Configuration file for running the ACASXu benchmark (all properties).
+general:
+  enable_incomplete_verification: False
+  loss_reduction_func: max
+data:
+  num_outputs: 5
+solver:
+  batch_size: 1000  # Number of parallel domains to compute on GPU.
+  bound_prop_method: crown
+  beta-crown:
+    iteration: 10  # Iterations for computing intermediate layer bounds.
+  alpha-crown:
+    iteration: 10
+    share_slopes: True  # This produces slightly looser bounds, but faster.
+bab:
+  branching:
+    method: naive  # Split on input space.
+    candidates: 3
+    sb_coeff_thresh: 0.01
+    input_split:
+      enable: True
+      enhanced_bound_prop_method: alpha-crown
+      enhanced_bound_patience: 20
+      enhanced_branching_method: sb
+      attack_patience: 80
+attack:
+  pgd_order: after
diff --git a/config/caisar-detection-data.conf b/config/caisar-detection-data.conf
index 47825ee8ee8aba4c4be6ccdccf79129c051cac80..b762961a1b08cc4b4d89244ae64457b62ea329b2 100644
--- a/config/caisar-detection-data.conf
+++ b/config/caisar-detection-data.conf
@@ -108,6 +108,17 @@ command = "%e --device cpu --onnx_path %{nnet-onnx} --vnnlib_path %f --timeout %
 driver = "caisar_drivers/abcrown.drv"
 use_at_auto_level = 1
 
+[ATP abcrown]
+name = "alpha-beta-CROWN"
+alternative = "ACAS"
+exec = "abcrown.sh"
+version_switch = "--version"
+version_regexp = "\\(dummy-version\\)"
+version_ok  = "dummy-version"
+command = "%e --device cpu --onnx_path %{nnet-onnx} --vnnlib_path %f --config %{config}/abcrown/acasxu.yaml --timeout %t"
+driver = "caisar_drivers/abcrown.drv"
+use_at_auto_level = 1
+
 [ATP saver]
 name = "SAVer"
 exec = "saver"
diff --git a/config/dune b/config/dune
index 3bf2582372a65f9b69fd3891854e84d270a0dd46..54012928ddb1adf9a192e6a4a935d506cbbea18a 100644
--- a/config/dune
+++ b/config/dune
@@ -3,8 +3,9 @@
   (site
    (caisar config)))
  (files
-  custom_transformations.py
   caisar-detection-data.conf
+  custom_transformations.py
+  (abcrown/acasxu.yaml as abcrown/acasxu.yaml)
   (drivers/pyrat.drv as drivers/pyrat.drv)
   (drivers/marabou.drv as drivers/marabou.drv)
   (drivers/saver.drv as drivers/saver.drv)
diff --git a/src/verification.ml b/src/verification.ml
index ce6f2f785397ca3674d272bdd8b631c13fc366a6..f7c49143a7e6e1186ec1cbdbd76a3fb82cf66de6 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -150,6 +150,8 @@ let answer_aimos limit config env config_prover dataset task =
   (answer, additional_info)
 
 let nnet_or_onnx = Re__Core.(compile (str "%{nnet-onnx}"))
+let config_re = Re__Core.(compile (str "%{config}"))
+let config_site = List.hd_exn Dirs.Sites.config
 
 let call_prover_on_task limit config command driver task =
   let prover_call =
@@ -247,6 +249,7 @@ let answer_generic limit config prover config_prover driver ~proof_strategy task
         Whyconf.get_complete_command ~with_steps:false config_prover
       in
       let command = Re__Core.replace_string nnet_or_onnx ~by:nn_file command in
+      let command = Re__Core.replace_string config_re ~by:config_site command in
       List.map tasks ~f:(call_prover_on_task limit config command driver))
   in
   let prover_answer = combine_prover_answers answers in
diff --git a/tests/autodetect.t b/tests/autodetect.t
index 6c4a2f42f3537c048f43893961845f5d02870233..cd2e8efe01d966b015262f540b62f7773338cf02 100644
--- a/tests/autodetect.t
+++ b/tests/autodetect.t
@@ -53,9 +53,10 @@ Test autodetect
   <autodetect>Found prover PyRAT version 1.1 (alternative: ACAS)
   <autodetect>Found prover nnenum version dummy-version, OK.
   <autodetect>Found prover alpha-beta-CROWN version dummy-version, OK.
+  <autodetect>Found prover alpha-beta-CROWN version dummy-version (alternative: ACAS)
   <autodetect>Found prover SAVer version v1.0, OK.
   <autodetect>Found prover AIMOS version 1.0, OK.
-  <autodetect>10 prover(s) added
+  <autodetect>11 prover(s) added
   [caisar] AIMOS 1.0
            Alt-Ergo 2.4.0
            CVC5 1.0.2
@@ -65,4 +66,5 @@ Test autodetect
            PyRAT 1.1 (VNNLIB)
            SAVer v1.0
            alpha-beta-CROWN dummy-version
+           alpha-beta-CROWN dummy-version (ACAS)
            nnenum dummy-version