Fix ARG enabled without ana.sv-comp.enabled

goblint · Aug 2, 2023 · 95aafbc · 95aafbc
1 parent 43a3437
commit 95aafbc
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/framework/control.ml b/src/framework/control.ml
@@ -14,7 +14,7 @@ module type S2S = functor (X : Spec) -> Spec
 (* spec is lazy, so HConsed table in Hashcons lifters is preserved between analyses in server mode *)
 let spec_module: (module Spec) Lazy.t = lazy (
   GobConfig.building_spec := true;
-  let arg_enabled = get_bool "witness.enabled" || get_bool "exp.arg" in
+  let arg_enabled = (get_bool "ana.sv-comp.enabled" && get_bool "witness.enabled") || get_bool "exp.arg" in
   let open Batteries in
   (* apply functor F on module X if opt is true *)
   let lift opt (module F : S2S) (module X : Spec) = (module (val if opt then (module F (X)) else (module X) : Spec) : Spec) in