From d97504bf08c8f79e04539665432ad05ffd843523 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 7 Sep 2023 16:13:29 +0300
Subject: [PATCH] Fix YAML witness unassume indentation (PR #1124)

---
 src/analyses/base.ml   |  6 +++--
 src/witness/witness.ml | 58 +++++++++++++++++++++---------------------
 2 files changed, 33 insertions(+), 31 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 4a49b9eed0..b74555b7ad 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2297,8 +2297,10 @@ struct
           let sizeval = eval_int (Analyses.ask_of_ctx ctx) gs st size in
           let countval = eval_int (Analyses.ask_of_ctx ctx) gs st n in
           if ID.to_int countval = Some Z.one then (
-            set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(add_null (AD.of_var heap_var), TVoid [], Blob (VD.bot (), sizeval, false));
-          (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_var heap_var)))]
+            set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [
+              add_null (AD.of_var heap_var), TVoid [], Blob (VD.bot (), sizeval, false);
+              eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_var heap_var))
+            ]
           )
           else (
             let blobsize = ID.mul (ID.cast_to ik @@ sizeval) (ID.cast_to ik @@ countval) in
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index f73a2755c8..baa465a1b3 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -306,35 +306,35 @@ struct
   let determine_result entrystates (module Task:Task): (module WitnessTaskResult) =
     let module Arg: BiArgInvariant =
       (val if GobConfig.get_bool "witness.enabled" then (
-          let module Arg = (val ArgTool.create entrystates) in
-          let module Arg =
-          struct
-            include Arg
-
-            let find_invariant (n, c, i) =
-              let context = {Invariant.default_context with path = Some i} in
-              ask_local (n, c) (Invariant context)
-          end
-          in
-          (module Arg: BiArgInvariant)
-        )
-        else (
-          let module Arg =
-          struct
-            module Node = ArgTool.Node
-            module Edge = MyARG.InlineEdge
-            let next _ = []
-            let prev _ = []
-            let find_invariant _ = Invariant.none
-            let main_entry =
-              let lvar = WitnessUtil.find_main_entry entrystates in
-              (fst lvar, snd lvar, -1)
-            let iter_nodes f = f main_entry
-            let query _ q = Queries.Result.top q
-          end
-          in
-          (module Arg: BiArgInvariant)
-        )
+           let module Arg = (val ArgTool.create entrystates) in
+           let module Arg =
+           struct
+             include Arg
+
+             let find_invariant (n, c, i) =
+               let context = {Invariant.default_context with path = Some i} in
+               ask_local (n, c) (Invariant context)
+           end
+           in
+           (module Arg: BiArgInvariant)
+         )
+         else (
+           let module Arg =
+           struct
+             module Node = ArgTool.Node
+             module Edge = MyARG.InlineEdge
+             let next _ = []
+             let prev _ = []
+             let find_invariant _ = Invariant.none
+             let main_entry =
+               let lvar = WitnessUtil.find_main_entry entrystates in
+               (fst lvar, snd lvar, -1)
+             let iter_nodes f = f main_entry
+             let query _ q = Queries.Result.top q
+           end
+           in
+           (module Arg: BiArgInvariant)
+         )
       )
     in