From 13e510e49495fbe31f3d4923e8696d2d08a6e8d5 Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko <protz@microsoft.com>
Date: Tue, 18 Oct 2022 11:05:47 -0700
Subject: [PATCH] Temporary fix for #293

---
 src/PrintC.ml      |  6 +++---
 test/IfDefKrml.fst | 25 +++++++++++++++++++++++++
 2 files changed, 28 insertions(+), 3 deletions(-)
 create mode 100644 test/IfDefKrml.fst

diff --git a/src/PrintC.ml b/src/PrintC.ml
index 595d498eb..d59c1a5b9 100644
--- a/src/PrintC.ml
+++ b/src/PrintC.ml
@@ -367,14 +367,14 @@ and p_stmt (s: stmt) =
         string (KPrint.bsprintf "%s %a" prefix pdoc doc)
       in
       group (mk_line "#if" (p_expr cond) ^^ hardline ^^
-        p_stmts then_block ^^ hardline ^^
+        p_stmt (Compound then_block) ^^ hardline ^^
         separate_map hardline (fun (cond, stmts) ->
           mk_line "#elif" (p_expr cond) ^^ hardline ^^
-          p_stmts stmts) elif_blocks ^^
+          p_stmt (Compound stmts)) elif_blocks ^^
         (if List.length elif_blocks > 0 then hardline else empty) ^^
         (if List.length else_block > 0 then
           string "#else" ^^ hardline ^^
-          p_stmts else_block ^^ hardline
+          p_stmt (Compound else_block) ^^ hardline
         else
           empty) ^^
         string "#endif")
diff --git a/test/IfDefKrml.fst b/test/IfDefKrml.fst
new file mode 100644
index 000000000..51881620f
--- /dev/null
+++ b/test/IfDefKrml.fst
@@ -0,0 +1,25 @@
+module IfDefKrml
+open FStar.HyperStack.ST
+open LowStar.Buffer
+[@@CIfDef]
+assume
+val flag : bool
+
+
+let something_effectful (x:bool) : Stack bool (requires λ _ → ⊤) (ensures (λ _ _ _ → ⊤)) = x
+
+let test (x y:bool) =
+  let z =
+    if flag
+    then false
+    else let aa = something_effectful x in
+         aa
+  in
+  let z =
+    if flag
+    then false
+    else let aa = something_effectful z in
+         aa
+  in z
+
+let main () = if test true true then 0l else 1l