From 0f5e93e82c58f9babc38252a8e392d4fb4113ac1 Mon Sep 17 00:00:00 2001
From: Qinheping Hu <qinhh@amazon.com>
Date: Wed, 31 May 2023 12:00:36 -0500
Subject: [PATCH] Conver do{}while(0) to non-loop block

---
 .../goto-synthesizer/do_while_loop_0/main.c   |  8 ++++++
 .../do_while_loop_0/test.desc                 | 10 ++++++++
 ...enumerative_loop_contracts_synthesizer.cpp | 25 ++++++++++++++++---
 3 files changed, 40 insertions(+), 3 deletions(-)
 create mode 100644 regression/goto-synthesizer/do_while_loop_0/main.c
 create mode 100644 regression/goto-synthesizer/do_while_loop_0/test.desc

diff --git a/regression/goto-synthesizer/do_while_loop_0/main.c b/regression/goto-synthesizer/do_while_loop_0/main.c
new file mode 100644
index 00000000000..7d6aad05431
--- /dev/null
+++ b/regression/goto-synthesizer/do_while_loop_0/main.c
@@ -0,0 +1,8 @@
+int main()
+{
+  int result = 0;
+  do
+  {
+    result += 1;
+  } while(0 == 1);
+}
diff --git a/regression/goto-synthesizer/do_while_loop_0/test.desc b/regression/goto-synthesizer/do_while_loop_0/test.desc
new file mode 100644
index 00000000000..7ff4163109e
--- /dev/null
+++ b/regression/goto-synthesizer/do_while_loop_0/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Check if synthesizer works for do {} while (0).
diff --git a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp
index e681bb2fed6..12382c90a04 100644
--- a/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp
+++ b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp
@@ -99,15 +99,34 @@ void enumerative_loop_contracts_synthesizert::init_candidates()
       if(loop_head_and_content.second.size() <= 1)
         continue;
 
-      goto_programt::const_targett loop_end =
+      goto_programt::targett loop_end =
         get_loop_end_from_loop_head_and_content_mutable(
           loop_head_and_content.first, loop_head_and_content.second);
 
       loop_idt new_id(function_p.first, loop_end->loop_number);
       loop_cfg_infot cfg_info(function_p.second, loop_head_and_content.second);
 
-      log.debug() << "Initialize candidates for the loop at "
-                  << loop_end->source_location() << messaget::eom;
+      log.progress() << "Initialize candidates for the loop at "
+                     << loop_end->source_location() << messaget::eom;
+
+      // Turn do while loops of form
+      //
+      // do
+      // { loop body }
+      // while (0)
+      //
+      // into non-loop block
+      //
+      // { loop body }
+      // skip
+      //
+      if(
+        loop_end->is_goto() &&
+        simplify_expr(loop_end->condition(), ns) == false_exprt())
+      {
+        loop_end->turn_into_skip();
+        continue;
+      }
 
       // we only synthesize invariants and assigns for unannotated loops
       if(loop_end->condition().find(ID_C_spec_loop_invariant).is_nil())