diff --git a/src/cdomain/value/domains/invariantCil.ml b/src/cdomain/value/domains/invariantCil.ml
index ef0687d6eb..813ec25818 100644
--- a/src/cdomain/value/domains/invariantCil.ml
+++ b/src/cdomain/value/domains/invariantCil.ml
@@ -13,15 +13,24 @@ class exp_replace_original_name_visitor = object
   method! vvrbl (vi: varinfo) =
     ChangeTo (var_replace_original_name vi)
 end
-let exp_replace_original_name e =
+let exp_replace_original_name =
   let visitor = new exp_replace_original_name_visitor in
-  visitCilExpr visitor e
+  visitCilExpr visitor
+
+class exp_deep_unroll_types_visitor = object
+  inherit nopCilVisitor
+  method! vtype (t: typ) =
+    ChangeTo (unrollTypeDeep t)
+end
+let exp_deep_unroll_types =
+  let visitor = new exp_deep_unroll_types_visitor in
+  visitCilExpr visitor
 
 
 let var_is_in_scope scope vi =
   match Cilfacade.find_scope_fundec vi with
   | None -> vi.vstorage <> Static (* CIL pulls static locals into globals, but they aren't syntactically in global scope *)
-  | Some fd -> 
+  | Some fd ->
     if CilType.Fundec.equal fd scope then
       GobConfig.get_bool "witness.invariant.all-locals" || (not @@ hasAttribute "goblint_cil_nested" vi.vattr)
     else
@@ -75,6 +84,23 @@ let exp_contains_tmp e =
   ignore (visitCilExpr visitor e);
   !acc
 
+class exp_contains_anon_type_visitor = object
+  inherit nopCilVisitor
+  method! vtype (t: typ) =
+    match t with
+    | TComp ({cname; _}, _) when BatString.starts_with_stdlib ~prefix:"__anon" cname ->
+      raise Stdlib.Exit
+    | _ ->
+      DoChildren
+end
+let exp_contains_anon_type =
+  let visitor = new exp_contains_anon_type_visitor in
+  fun e ->
+    match visitCilExpr visitor e with
+    | _ -> false
+    | exception Stdlib.Exit -> true
+
+
 (* TODO: synchronize magic constant with BaseDomain *)
 let var_is_heap {vname; _} = BatString.starts_with vname "(alloc@"
 
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index a01a5bdb31..c3d21be874 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -2474,6 +2474,12 @@
               "description": "Emit non-standard Goblint-specific invariants. Currently array invariants with all_index offsets.",
               "type": "boolean",
               "default": false
+            },
+            "typedefs": {
+              "title": "witness.invariant.typedefs",
+              "description": "Emit invariants with typedef-ed types (e.g. in casts). Our validator cannot parse these.",
+              "type": "boolean",
+              "default": true
             }
           },
           "additionalProperties": false
diff --git a/src/witness/witnessUtil.ml b/src/witness/witnessUtil.ml
index 6c02546168..24316cbee4 100644
--- a/src/witness/witnessUtil.ml
+++ b/src/witness/witnessUtil.ml
@@ -160,9 +160,20 @@ struct
     | e -> to_conjunct_set e
 
   let process_exp inv =
-    let inv' = InvariantCil.exp_replace_original_name inv in
+    let exp_deep_unroll_types =
+      if GobConfig.get_bool "witness.invariant.typedefs" then
+        Fun.id
+      else
+        InvariantCil.exp_deep_unroll_types
+    in
+    let inv' =
+      inv
+      |> exp_deep_unroll_types
+      |> InvariantCil.exp_replace_original_name
+    in
     if GobConfig.get_bool "witness.invariant.split-conjunction" then
       ES.elements (pullOutCommonConjuncts inv')
+      |> List.filter (Fun.negate InvariantCil.exp_contains_anon_type)
     else
       [inv']
 end
diff --git a/tests/regression/witness/typedef.t/run.t b/tests/regression/witness/typedef.t/run.t
new file mode 100644
index 0000000000..b06164743b
--- /dev/null
+++ b/tests/regression/witness/typedef.t/run.t
@@ -0,0 +1,316 @@
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable witness.invariant.typedefs typedef.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 6
+    dead: 0
+    total lines: 6
+  [Info][Witness] witness generation summary:
+    total generation entries: 13
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 42
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: q == (void *)(& a)
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: p == (void *)(& x)
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: a.f == 43
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: '*((int *)p) == 42'
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 42
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 2
+      function: main
+    location_invariant:
+      string: p == (void *)(& x)
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 2
+      function: main
+    location_invariant:
+      string: a.f == 43
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 2
+      function: main
+    location_invariant:
+      string: '*((int *)p) == 42'
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 12
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 42
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 12
+      column: 2
+      function: main
+    location_invariant:
+      string: p == (void *)(& x)
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 12
+      column: 2
+      function: main
+    location_invariant:
+      string: '*((int *)p) == 42'
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 9
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 42
+      type: assertion
+      format: C
+
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --enable witness.invariant.typedefs typedef.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 6
+    dead: 0
+    total lines: 6
+  [Info][Witness] witness generation summary:
+    total generation entries: 14
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 42
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: q == (void *)(& a)
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: p == (void *)(& x)
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: a.f == 43
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: '*((myint *)p) == 42'
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 14
+      column: 2
+      function: main
+    location_invariant:
+      string: ((s *)q)->f == 43
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 42
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 2
+      function: main
+    location_invariant:
+      string: p == (void *)(& x)
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 2
+      function: main
+    location_invariant:
+      string: a.f == 43
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 13
+      column: 2
+      function: main
+    location_invariant:
+      string: '*((myint *)p) == 42'
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 12
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 42
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 12
+      column: 2
+      function: main
+    location_invariant:
+      string: p == (void *)(& x)
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 12
+      column: 2
+      function: main
+    location_invariant:
+      string: '*((myint *)p) == 42'
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: typedef.c
+      file_hash: $FILE_HASH
+      line: 9
+      column: 2
+      function: main
+    location_invariant:
+      string: x == 42
+      type: assertion
+      format: C
diff --git a/tests/regression/witness/typedef.t/typedef.c b/tests/regression/witness/typedef.t/typedef.c
new file mode 100644
index 0000000000..1e60ad084d
--- /dev/null
+++ b/tests/regression/witness/typedef.t/typedef.c
@@ -0,0 +1,15 @@
+typedef int myint;
+
+typedef struct {
+  int f;
+} s;
+
+int main() {
+  myint x = 42;
+  void *p = &x;
+
+  s a;
+  a.f = 43;
+  void *q = &a;
+  return 0;
+}