Fix invariant_set elements schema in YAML witnesses

goblint · Nov 21, 2023 · 8b79948 · 8b79948
1 parent 0ee71a0
commit 8b79948
Showing 1 changed file with 7 additions and 4 deletions.
diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml
@@ -311,13 +311,16 @@ struct
     }
 
     let to_yaml {invariant_type} =
-      `O ([
-          ("type", `String (InvariantType.invariant_type invariant_type));
-        ] @ InvariantType.to_yaml' invariant_type)
+      `O [
+        ("invariant", `O ([
+             ("type", `String (InvariantType.invariant_type invariant_type));
+           ] @ InvariantType.to_yaml' invariant_type)
+        )
+      ]
 
     let of_yaml y =
       let open GobYaml in
-      let+ invariant_type = y |> InvariantType.of_yaml in
+      let+ invariant_type = y |> find "invariant" >>= InvariantType.of_yaml in
       {invariant_type}
   end