From 95aafbc4c909ac6016cb92afe27f6e1272553304 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 2 Aug 2023 10:22:39 +0300 Subject: [PATCH] Fix ARG enabled without ana.sv-comp.enabled --- src/framework/control.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/framework/control.ml b/src/framework/control.ml index cd3a8b5f74..5cefc1a7de 100644 --- 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