diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml
index a71f2544e3..6f2d941ce0 100644
--- a/src/common/util/cilfacade.ml
+++ b/src/common/util/cilfacade.ml
@@ -49,12 +49,11 @@ let init_options () =
   Cil.gnu89inline := get_bool "cil.gnu89inline";
   Cabs2cil.addNestedScopeAttr := get_bool "cil.addNestedScopeAttr";
 
-  if get_bool "ana.sv-comp.enabled" then (
-    Cil.envMachine := match get_string "exp.architecture" with
-      | "32bit" -> Machdep.gcc32
-      | "64bit" -> Machdep.gcc64
-      | _ -> assert false
-  )
+  Cil.envMachine := match get_string "exp.architecture" with
+    | "host" -> Some Machdep.gcc
+    | "32bit" -> Machdep.gcc32
+    | "64bit" -> Machdep.gcc64
+    | _ -> assert false
 
 let init () =
   initCIL ();
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index 7b07c3ca35..358bb796ea 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -1819,10 +1819,10 @@
         },
         "architecture": {
           "title": "exp.architecture",
-          "description": "Architecture for analysis, currently for witness",
+          "description": "Architecture for analysis",
           "type": "string",
-          "enum": ["64bit", "32bit"],
-          "default": "64bit"
+          "enum": ["host", "64bit", "32bit"],
+          "default": "host"
         },
         "gcc_path": {
           "title": "exp.gcc_path",
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 95849bce36..4fee8b11dc 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -275,14 +275,12 @@ let preprocess_files () =
   (* Preprocessor flags *)
   let cppflags = ref (get_string_list "pre.cppflags") in
 
-  if get_bool "ana.sv-comp.enabled" then (
-    let architecture_flag = match get_string "exp.architecture" with
-      | "32bit" -> "-m32"
-      | "64bit" -> "-m64"
-      | _ -> assert false
-    in
-    cppflags := architecture_flag :: !cppflags
-  );
+  cppflags := begin match get_string "exp.architecture" with
+    | "host" -> !cppflags
+    | "32bit" -> "-m32" :: !cppflags
+    | "64bit" -> "-m64" :: !cppflags
+    | _ -> assert false
+  end;
 
   (* the base include directory *)
   (* TODO: any better way? dune executable promotion doesn't add _build sites *)
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index 7b0213b601..1fb1d8d576 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -124,7 +124,11 @@ let write_file filename (module Task:Task) (module TaskResult:WitnessTaskResult)
   GML.write_metadata g "programfile" programfile;
   let programhash = Sha256.(to_hex (file programfile)) in
   GML.write_metadata g "programhash" programhash;
-  GML.write_metadata g "architecture" (get_string "exp.architecture");
+  let architecture = match GobConfig.get_string "exp.architecture" with
+    | ("64bit" | "32bit") as architecture -> architecture
+    | _ -> failwith "invalid SV-COMP architecture"
+  in
+  GML.write_metadata g "architecture" architecture;
   GML.write_metadata g "creationtime" (TimeUtil.iso8601_now ());
 
   let write_node ?(entry=false) node =
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 2bdd2ced4c..1e1914c2f6 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -203,7 +203,7 @@ struct
     let data_model = match GobConfig.get_string "exp.architecture" with
       | "64bit" -> "LP64"
       | "32bit" -> "ILP32"
-      | _ -> failwith "invalid architecture"
+      | _ -> failwith "invalid SV-COMP architecture"
     in
     let specification = Option.map (fun (module Task: Svcomp.Task) ->
         Svcomp.Specification.to_string Task.specification