From e672e0d456e016d12fce489940d88220ee5e2b9a Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <mt@debian.org>
Date: Fri, 23 Dec 2016 14:47:45 +0100
Subject: [PATCH] Turn "label: goto label;" or "while(cond);" into assume

This pattern occurs in some SV-COMP benchmarks, but may also appear as
busy-wait loops in realistic systems.
---
 src/goto-symex/symex_goto.cpp | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index 17149677965..dd31349024c 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -68,6 +68,27 @@ void goto_symext::symex_goto(statet &state)
 
   if(!forward) // backwards?
   {
+    // is it label: goto label; or while(cond); - popular in SV-COMP
+    if(goto_target==state.source.pc ||
+       (instruction.incoming_edges.size()==1 &&
+        *instruction.incoming_edges.begin()==goto_target))
+    {
+      // generate assume(false) or a suitable negation if this
+      // instruction is a conditional goto
+      exprt negated_cond;
+
+      if(new_guard.is_true())
+        negated_cond=false_exprt();
+      else
+        negated_cond=not_exprt(new_guard);
+
+      symex_assume(state, negated_cond);
+
+      // next instruction
+      state.source.pc++;
+      return;
+    }
+
     unsigned &unwind=
       frame.loop_iterations[goto_programt::loop_id(state.source.pc)].count;
     unwind++;