From e5a6e2f19ae6234c1e58265067cbcbde16e623e1 Mon Sep 17 00:00:00 2001
From: vagrant <vagrant@vagrant.vm>
Date: Mon, 10 Aug 2020 23:18:54 +0000
Subject: [PATCH 01/20] Finished Basic Hello World Pass

Added the skeleton of the AnnotateLoopEnds pass,
which does not modify the code at this point,
but simply prints when it finds a function,
loop, or exit point.
---
 CMakeLists.txt                   |  2 +
 include/smack/AnnotateLoopEnds.h | 24 ++++++++++
 lib/smack/AnnotateLoopEnds.cpp   | 80 ++++++++++++++++++++++++++++++++
 tools/llvm2bpl/llvm2bpl.cpp      |  2 +
 4 files changed, 108 insertions(+)
 create mode 100644 include/smack/AnnotateLoopEnds.h
 create mode 100644 lib/smack/AnnotateLoopEnds.cpp

diff --git a/CMakeLists.txt b/CMakeLists.txt
index ade90912b..0015317cc 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -120,6 +120,7 @@ add_library(smackTranslator STATIC
   include/smack/RewriteBitwiseOps.h
   include/smack/NormalizeLoops.h
   include/smack/RustFixes.h
+  include/smack/AnnotateLoopEnds.h
   include/smack/SplitAggregateValue.h
   include/smack/Prelude.h
   include/smack/SmackWarnings.h
@@ -146,6 +147,7 @@ add_library(smackTranslator STATIC
   lib/smack/RewriteBitwiseOps.cpp
   lib/smack/NormalizeLoops.cpp
   lib/smack/RustFixes.cpp
+  lib/smack/AnnotateLoopEnds.cpp
   lib/smack/SplitAggregateValue.cpp
   lib/smack/Prelude.cpp
   lib/smack/SmackWarnings.cpp
diff --git a/include/smack/AnnotateLoopEnds.h b/include/smack/AnnotateLoopEnds.h
new file mode 100644
index 000000000..7ada4de36
--- /dev/null
+++ b/include/smack/AnnotateLoopEnds.h
@@ -0,0 +1,24 @@
+//
+// This file is distributed under the MIT License. See LICENSE for details.
+//
+#ifndef ANNOTATELOOPENDS_H
+#define ANNOTATELOOPENDS_H
+
+#include "llvm/IR/Instructions.h"
+#include "llvm/IR/Module.h"
+#include "llvm/Pass.h"
+#include <map>
+
+namespace smack {
+
+class AnnotateLoopEnds : public llvm::FunctionPass {
+public:
+  static char ID; // Pass identification, replacement for typeid
+  AnnotateLoopEnds() : llvm::FunctionPass(ID) {}
+  virtual llvm::StringRef getPassName() const override;
+  virtual bool runOnFunction(llvm::Function &F) override;
+  virtual void getAnalysisUsage(llvm::AnalysisUsage &) const override;
+};
+} // namespace smack
+
+#endif // ANNOTATELOOPENDS_H
diff --git a/lib/smack/AnnotateLoopEnds.cpp b/lib/smack/AnnotateLoopEnds.cpp
new file mode 100644
index 000000000..3146af658
--- /dev/null
+++ b/lib/smack/AnnotateLoopEnds.cpp
@@ -0,0 +1,80 @@
+//
+// This file is distributed under the MIT License. See LICENSE for details.
+//
+
+//
+// This pass normalizes loop structures to allow easier generation of Boogie
+// code when a loop edge comes from a branch. Specifically, a forwarding block
+// is added between a branching block and the loop header.
+//
+
+#include "smack/AnnotateLoopEnds.h"
+#include "smack/Naming.h"
+#include "llvm/Analysis/LoopInfo.h"
+#include "llvm/IR/Constants.h"
+#include "llvm/IR/Dominators.h"
+#include "llvm/IR/IRBuilder.h"
+#include "llvm/IR/InstIterator.h"
+#include "llvm/IR/Module.h"
+#include "llvm/IR/ValueSymbolTable.h"
+#include <map>
+#include <set>
+#include <vector>
+
+#include "llvm/Support/raw_ostream.h"
+
+namespace smack {
+
+using namespace llvm;
+
+// Register LoopInfo
+void AnnotateLoopEnds::getAnalysisUsage(AnalysisUsage &AU) const {
+  AU.addRequired<LoopInfoWrapperPass>();
+}
+
+void processExitingBlock(BasicBlock *block) {
+  // print exit block found!!
+
+  errs() << "    Exit block found! \n";
+
+}
+
+void annotateLoopEnd(Loop *loop) {
+  //BasicBlock *headerBlock = loop->getHeader();
+
+  // I imagine that it is very uncommon for a loop to have
+  //   more than 5 exit points.
+  SmallVector<BasicBlock *, 5> exitingBlocks; 
+
+  loop->getExitingBlocks(exitingBlocks);
+  
+  for (BasicBlock *b : exitingBlocks) {
+    processExitingBlock(b);
+  } 
+
+  // Handle subloops
+  //for (Loop *subloop : loop->getSubLoops()) {
+  //  processLoop(subloop);
+  //}
+}
+
+bool AnnotateLoopEnds::runOnFunction(Function &F) {
+  if (F.isIntrinsic() || F.empty()) {
+    return false;
+  }
+  errs() << "Hello " << F.getName() << "\n";
+  LoopInfo &loopInfo = getAnalysis<LoopInfoWrapperPass>().getLoopInfo();
+  for (LoopInfo::iterator LI = loopInfo.begin(), LIEnd = loopInfo.end();
+       LI != LIEnd; ++LI) {
+    errs() << "  Loop Found in " << F.getName() << "\n";
+    annotateLoopEnd(*LI);
+  }
+
+  return true;
+}
+
+// Pass ID variable
+char AnnotateLoopEnds::ID = 0;
+
+StringRef AnnotateLoopEnds::getPassName() const { return "Annotate Loop Ends with assert(false)"; }
+} // namespace smack
diff --git a/tools/llvm2bpl/llvm2bpl.cpp b/tools/llvm2bpl/llvm2bpl.cpp
index 4d018896b..556890b7f 100644
--- a/tools/llvm2bpl/llvm2bpl.cpp
+++ b/tools/llvm2bpl/llvm2bpl.cpp
@@ -36,6 +36,7 @@
 #include "smack/MemorySafetyChecker.h"
 #include "smack/Naming.h"
 #include "smack/NormalizeLoops.h"
+#include "smack/AnnotateLoopEnds.h"
 #include "smack/RemoveDeadDefs.h"
 #include "smack/RewriteBitwiseOps.h"
 #include "smack/RustFixes.h"
@@ -196,6 +197,7 @@ int main(int argc, char **argv) {
 
   // pass_manager.add(new llvm::StructRet());
   pass_manager.add(new smack::NormalizeLoops());
+  pass_manager.add(new smack::AnnotateLoopEnds());
   pass_manager.add(new llvm::SimplifyEV());
   pass_manager.add(new llvm::SimplifyIV());
   pass_manager.add(new smack::ExtractContracts());

From 9cc59b308d05214a62accd33158d59b1fdefc85f Mon Sep 17 00:00:00 2001
From: Jack J Garzella <jjgarzella@gmail.com>
Date: Tue, 11 Aug 2020 20:58:11 +0000
Subject: [PATCH 02/20] Working first version of loop exit pass

Added code to AnnotateLoopEnds which inserts
a boogie 'assert false' at any exit of a loop.

The assertions are inserted at the beginning
of the "loop exit" basic block, that is the
immediate node outside of the loop.
In order to prevent a random failure, the pass
now requires the LoopSimplify pass to run first,
which guarentees that each loop exit block is
dominated only by the loop.
---
 include/smack/AnnotateLoopEnds.h |  6 ++--
 lib/smack/AnnotateLoopEnds.cpp   | 50 ++++++++++++++++++++++----------
 share/smack/lib/smack.c          |  4 +++
 3 files changed, 41 insertions(+), 19 deletions(-)

diff --git a/include/smack/AnnotateLoopEnds.h b/include/smack/AnnotateLoopEnds.h
index 7ada4de36..6b8911195 100644
--- a/include/smack/AnnotateLoopEnds.h
+++ b/include/smack/AnnotateLoopEnds.h
@@ -11,12 +11,12 @@
 
 namespace smack {
 
-class AnnotateLoopEnds : public llvm::FunctionPass {
+class AnnotateLoopEnds : public llvm::ModulePass {
 public:
   static char ID; // Pass identification, replacement for typeid
-  AnnotateLoopEnds() : llvm::FunctionPass(ID) {}
+  AnnotateLoopEnds() : llvm::ModulePass(ID) {}
   virtual llvm::StringRef getPassName() const override;
-  virtual bool runOnFunction(llvm::Function &F) override;
+  virtual bool runOnModule(llvm::Module &m) override;
   virtual void getAnalysisUsage(llvm::AnalysisUsage &) const override;
 };
 } // namespace smack
diff --git a/lib/smack/AnnotateLoopEnds.cpp b/lib/smack/AnnotateLoopEnds.cpp
index 3146af658..1e16d1394 100644
--- a/lib/smack/AnnotateLoopEnds.cpp
+++ b/lib/smack/AnnotateLoopEnds.cpp
@@ -11,6 +11,7 @@
 #include "smack/AnnotateLoopEnds.h"
 #include "smack/Naming.h"
 #include "llvm/Analysis/LoopInfo.h"
+#include "llvm/Transforms/Utils.h"
 #include "llvm/IR/Constants.h"
 #include "llvm/IR/Dominators.h"
 #include "llvm/IR/IRBuilder.h"
@@ -29,27 +30,34 @@ using namespace llvm;
 
 // Register LoopInfo
 void AnnotateLoopEnds::getAnalysisUsage(AnalysisUsage &AU) const {
+  AU.addRequiredID(LoopSimplifyID);
   AU.addRequired<LoopInfoWrapperPass>();
 }
 
-void processExitingBlock(BasicBlock *block) {
+void insertLoopEndAssertion(Function *le, Instruction *insertBefore) {
+  CallInst::Create(le, "", insertBefore);
+}
+
+void processExitBlock(BasicBlock *block, Function *le) {
   // print exit block found!!
 
   errs() << "    Exit block found! \n";
 
+  Instruction& front = block->front();
+  insertLoopEndAssertion(le,&front);
 }
 
-void annotateLoopEnd(Loop *loop) {
+void annotateLoopEnd(Loop *loop, Function *le) {
   //BasicBlock *headerBlock = loop->getHeader();
 
   // I imagine that it is very uncommon for a loop to have
   //   more than 5 exit points.
-  SmallVector<BasicBlock *, 5> exitingBlocks; 
+  SmallVector<BasicBlock *, 5> exitBlocks; 
 
-  loop->getExitingBlocks(exitingBlocks);
+  loop->getExitBlocks(exitBlocks);
   
-  for (BasicBlock *b : exitingBlocks) {
-    processExitingBlock(b);
+  for (BasicBlock *b : exitBlocks) {
+    processExitBlock(b,le);
   } 
 
   // Handle subloops
@@ -58,16 +66,26 @@ void annotateLoopEnd(Loop *loop) {
   //}
 }
 
-bool AnnotateLoopEnds::runOnFunction(Function &F) {
-  if (F.isIntrinsic() || F.empty()) {
-    return false;
-  }
-  errs() << "Hello " << F.getName() << "\n";
-  LoopInfo &loopInfo = getAnalysis<LoopInfoWrapperPass>().getLoopInfo();
-  for (LoopInfo::iterator LI = loopInfo.begin(), LIEnd = loopInfo.end();
-       LI != LIEnd; ++LI) {
-    errs() << "  Loop Found in " << F.getName() << "\n";
-    annotateLoopEnd(*LI);
+bool AnnotateLoopEnds::runOnModule(Module &m) {
+
+  Function *le = m.getFunction("__SMACK_loop_end");
+  assert(le != NULL && "Function __SMACK_loop_end shoudl be present.");
+
+  errs() << "Module Start\n";
+  for (auto F = m.begin(), FEnd = m.end(); F != FEnd; ++F) {
+    if (F->isIntrinsic() || F->empty()) {
+      continue;
+    }
+
+    errs() << "Hello " << F->getName() << "\n";
+
+    LoopInfo &loopInfo = getAnalysis<LoopInfoWrapperPass>(*F).getLoopInfo();
+    for (LoopInfo::iterator LI = loopInfo.begin(), LIEnd = loopInfo.end();
+         LI != LIEnd; ++LI) {
+
+      errs() << "  Loop Found in " << F->getName() << "\n";
+      annotateLoopEnd(*LI, le);
+    }
   }
 
   return true;
diff --git a/share/smack/lib/smack.c b/share/smack/lib/smack.c
index 5666122c9..e5b9d64a4 100644
--- a/share/smack/lib/smack.c
+++ b/share/smack/lib/smack.c
@@ -1409,6 +1409,10 @@ void __SMACK_check_overflow(int flag) {
   __SMACK_code("assert {:overflow} @ == $0;", flag);
 }
 
+void __SMACK_loop_end(void) {
+  __SMACK_code("assert {:loopexit} false;");
+}
+
 char __VERIFIER_nondet_char(void) {
   char x = __SMACK_nondet_char();
   __VERIFIER_assume(x >= SCHAR_MIN && x <= SCHAR_MAX);

From 9dd9f1549a5c9f0492825c456a389783130a81bd Mon Sep 17 00:00:00 2001
From: Jack J Garzella <jjgarzella@gmail.com>
Date: Tue, 11 Aug 2020 21:34:31 +0000
Subject: [PATCH 03/20] Refactor AnnotateLoopEnds and remove extra prints

Rename AnnotateLoopEnds to AnnotateLoopExits

Remove some extrateous pringing in
AnnotateLoopExits, and put the remaining
print statements into the smack debug printing
macro.
---
 CMakeLists.txt                                |  4 +--
 ...AnnotateLoopEnds.h => AnnotateLoopExits.h} | 10 +++----
 ...tateLoopEnds.cpp => AnnotateLoopExits.cpp} | 28 ++++++++-----------
 tools/llvm2bpl/llvm2bpl.cpp                   |  4 +--
 4 files changed, 21 insertions(+), 25 deletions(-)
 rename include/smack/{AnnotateLoopEnds.h => AnnotateLoopExits.h} (72%)
 rename lib/smack/{AnnotateLoopEnds.cpp => AnnotateLoopExits.cpp} (75%)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 0015317cc..e0a522ce1 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -120,7 +120,7 @@ add_library(smackTranslator STATIC
   include/smack/RewriteBitwiseOps.h
   include/smack/NormalizeLoops.h
   include/smack/RustFixes.h
-  include/smack/AnnotateLoopEnds.h
+  include/smack/AnnotateLoopExits.h
   include/smack/SplitAggregateValue.h
   include/smack/Prelude.h
   include/smack/SmackWarnings.h
@@ -147,7 +147,7 @@ add_library(smackTranslator STATIC
   lib/smack/RewriteBitwiseOps.cpp
   lib/smack/NormalizeLoops.cpp
   lib/smack/RustFixes.cpp
-  lib/smack/AnnotateLoopEnds.cpp
+  lib/smack/AnnotateLoopExits.cpp
   lib/smack/SplitAggregateValue.cpp
   lib/smack/Prelude.cpp
   lib/smack/SmackWarnings.cpp
diff --git a/include/smack/AnnotateLoopEnds.h b/include/smack/AnnotateLoopExits.h
similarity index 72%
rename from include/smack/AnnotateLoopEnds.h
rename to include/smack/AnnotateLoopExits.h
index 6b8911195..df0f003b3 100644
--- a/include/smack/AnnotateLoopEnds.h
+++ b/include/smack/AnnotateLoopExits.h
@@ -1,8 +1,8 @@
 //
 // This file is distributed under the MIT License. See LICENSE for details.
 //
-#ifndef ANNOTATELOOPENDS_H
-#define ANNOTATELOOPENDS_H
+#ifndef ANNOTATELOOPEXITS_H
+#define ANNOTATELOOPEXITS_H
 
 #include "llvm/IR/Instructions.h"
 #include "llvm/IR/Module.h"
@@ -11,14 +11,14 @@
 
 namespace smack {
 
-class AnnotateLoopEnds : public llvm::ModulePass {
+class AnnotateLoopExits : public llvm::ModulePass {
 public:
   static char ID; // Pass identification, replacement for typeid
-  AnnotateLoopEnds() : llvm::ModulePass(ID) {}
+  AnnotateLoopExits() : llvm::ModulePass(ID) {}
   virtual llvm::StringRef getPassName() const override;
   virtual bool runOnModule(llvm::Module &m) override;
   virtual void getAnalysisUsage(llvm::AnalysisUsage &) const override;
 };
 } // namespace smack
 
-#endif // ANNOTATELOOPENDS_H
+#endif // ANNOTATELOOPEXITS_H
diff --git a/lib/smack/AnnotateLoopEnds.cpp b/lib/smack/AnnotateLoopExits.cpp
similarity index 75%
rename from lib/smack/AnnotateLoopEnds.cpp
rename to lib/smack/AnnotateLoopExits.cpp
index 1e16d1394..f5abe119f 100644
--- a/lib/smack/AnnotateLoopEnds.cpp
+++ b/lib/smack/AnnotateLoopExits.cpp
@@ -8,8 +8,10 @@
 // is added between a branching block and the loop header.
 //
 
-#include "smack/AnnotateLoopEnds.h"
+#define DEBUG_TYPE "smack-loop-unroll"
+#include "smack/AnnotateLoopExits.h"
 #include "smack/Naming.h"
+#include "smack/Debug.h"
 #include "llvm/Analysis/LoopInfo.h"
 #include "llvm/Transforms/Utils.h"
 #include "llvm/IR/Constants.h"
@@ -29,11 +31,12 @@ namespace smack {
 using namespace llvm;
 
 // Register LoopInfo
-void AnnotateLoopEnds::getAnalysisUsage(AnalysisUsage &AU) const {
+void AnnotateLoopExits::getAnalysisUsage(AnalysisUsage &AU) const {
   AU.addRequiredID(LoopSimplifyID);
   AU.addRequired<LoopInfoWrapperPass>();
 }
 
+// This method is for clarity and self-documentingness
 void insertLoopEndAssertion(Function *le, Instruction *insertBefore) {
   CallInst::Create(le, "", insertBefore);
 }
@@ -41,7 +44,7 @@ void insertLoopEndAssertion(Function *le, Instruction *insertBefore) {
 void processExitBlock(BasicBlock *block, Function *le) {
   // print exit block found!!
 
-  errs() << "    Exit block found! \n";
+  SDEBUG(errs() << "Processing an Exit Block\n");
 
   Instruction& front = block->front();
   insertLoopEndAssertion(le,&front);
@@ -51,7 +54,8 @@ void annotateLoopEnd(Loop *loop, Function *le) {
   //BasicBlock *headerBlock = loop->getHeader();
 
   // I imagine that it is very uncommon for a loop to have
-  //   more than 5 exit points.
+  //   more than 5 exit points. This is a complete guess
+  //   and we could probably have a better heuristic
   SmallVector<BasicBlock *, 5> exitBlocks; 
 
   loop->getExitBlocks(exitBlocks);
@@ -59,31 +63,23 @@ void annotateLoopEnd(Loop *loop, Function *le) {
   for (BasicBlock *b : exitBlocks) {
     processExitBlock(b,le);
   } 
-
-  // Handle subloops
-  //for (Loop *subloop : loop->getSubLoops()) {
-  //  processLoop(subloop);
-  //}
 }
 
-bool AnnotateLoopEnds::runOnModule(Module &m) {
+bool AnnotateLoopExits::runOnModule(Module &m) {
 
   Function *le = m.getFunction("__SMACK_loop_end");
   assert(le != NULL && "Function __SMACK_loop_end shoudl be present.");
 
-  errs() << "Module Start\n";
   for (auto F = m.begin(), FEnd = m.end(); F != FEnd; ++F) {
     if (F->isIntrinsic() || F->empty()) {
       continue;
     }
 
-    errs() << "Hello " << F->getName() << "\n";
-
     LoopInfo &loopInfo = getAnalysis<LoopInfoWrapperPass>(*F).getLoopInfo();
     for (LoopInfo::iterator LI = loopInfo.begin(), LIEnd = loopInfo.end();
          LI != LIEnd; ++LI) {
 
-      errs() << "  Loop Found in " << F->getName() << "\n";
+      SDEBUG(errs() << "Processing Loop in " << F->getName() << "\n");
       annotateLoopEnd(*LI, le);
     }
   }
@@ -92,7 +88,7 @@ bool AnnotateLoopEnds::runOnModule(Module &m) {
 }
 
 // Pass ID variable
-char AnnotateLoopEnds::ID = 0;
+char AnnotateLoopExits::ID = 0;
 
-StringRef AnnotateLoopEnds::getPassName() const { return "Annotate Loop Ends with assert(false)"; }
+StringRef AnnotateLoopExits::getPassName() const { return "Annotate Loop Ends with assert(false)"; }
 } // namespace smack
diff --git a/tools/llvm2bpl/llvm2bpl.cpp b/tools/llvm2bpl/llvm2bpl.cpp
index 556890b7f..03ac9bffe 100644
--- a/tools/llvm2bpl/llvm2bpl.cpp
+++ b/tools/llvm2bpl/llvm2bpl.cpp
@@ -36,7 +36,7 @@
 #include "smack/MemorySafetyChecker.h"
 #include "smack/Naming.h"
 #include "smack/NormalizeLoops.h"
-#include "smack/AnnotateLoopEnds.h"
+#include "smack/AnnotateLoopExits.h"
 #include "smack/RemoveDeadDefs.h"
 #include "smack/RewriteBitwiseOps.h"
 #include "smack/RustFixes.h"
@@ -197,7 +197,7 @@ int main(int argc, char **argv) {
 
   // pass_manager.add(new llvm::StructRet());
   pass_manager.add(new smack::NormalizeLoops());
-  pass_manager.add(new smack::AnnotateLoopEnds());
+  pass_manager.add(new smack::AnnotateLoopExits());
   pass_manager.add(new llvm::SimplifyEV());
   pass_manager.add(new llvm::SimplifyIV());
   pass_manager.add(new smack::ExtractContracts());

From 2916c61a6b7ad932aa8d58ddc46712912edf3aeb Mon Sep 17 00:00:00 2001
From: Jack J Garzella <jjgarzella@gmail.com>
Date: Thu, 13 Aug 2020 17:07:21 +0000
Subject: [PATCH 04/20] Tests, formattingl, and CLI

Some logistics around the AnnotateLoopExits pass.

* added a command line option to llvm2bpl and only
  invoke the pass when this option is set
* added a corresponding option in top.py
* added eight benchmarks, each with passing/failing
  variants. These benchmarks are interesting in that
  the code for passing/failing versions is identical,
  the only difference is the change in unroll bound.
* ran clang-format on the cpp files and fixed a few
  formatting/whitespace errors
---
 include/smack/SmackOptions.h      |  1 +
 lib/smack/AnnotateLoopExits.cpp   | 18 ++++++++++--------
 lib/smack/SmackOptions.cpp        |  3 +++
 share/smack/top.py                |  8 ++++++++
 test/c/unroll/break2.c            | 14 ++++++++++++++
 test/c/unroll/break2_fail.c       | 14 ++++++++++++++
 test/c/unroll/config.yml          |  2 ++
 test/c/unroll/for_nested.c        | 14 ++++++++++++++
 test/c/unroll/for_nested_fail.c   | 14 ++++++++++++++
 test/c/unroll/for_unroll.c        | 12 ++++++++++++
 test/c/unroll/for_unroll_fail.c   | 12 ++++++++++++
 test/c/unroll/goto_exit.c         | 28 ++++++++++++++++++++++++++++
 test/c/unroll/goto_exit_fail.c    | 28 ++++++++++++++++++++++++++++
 test/c/unroll/two_exits.c         | 20 ++++++++++++++++++++
 test/c/unroll/two_exits_fail.c    | 20 ++++++++++++++++++++
 test/c/unroll/two_loops.c         | 16 ++++++++++++++++
 test/c/unroll/two_loops2.c        | 16 ++++++++++++++++
 test/c/unroll/two_loops2_fail.c   | 16 ++++++++++++++++
 test/c/unroll/two_loops_fail.c    | 16 ++++++++++++++++
 test/c/unroll/while_nested.c      | 19 +++++++++++++++++++
 test/c/unroll/while_nested_fail.c | 19 +++++++++++++++++++
 tools/llvm2bpl/llvm2bpl.cpp       |  6 ++++--
 22 files changed, 306 insertions(+), 10 deletions(-)
 create mode 100644 test/c/unroll/break2.c
 create mode 100644 test/c/unroll/break2_fail.c
 create mode 100644 test/c/unroll/config.yml
 create mode 100644 test/c/unroll/for_nested.c
 create mode 100644 test/c/unroll/for_nested_fail.c
 create mode 100644 test/c/unroll/for_unroll.c
 create mode 100644 test/c/unroll/for_unroll_fail.c
 create mode 100644 test/c/unroll/goto_exit.c
 create mode 100644 test/c/unroll/goto_exit_fail.c
 create mode 100644 test/c/unroll/two_exits.c
 create mode 100644 test/c/unroll/two_exits_fail.c
 create mode 100644 test/c/unroll/two_loops.c
 create mode 100644 test/c/unroll/two_loops2.c
 create mode 100644 test/c/unroll/two_loops2_fail.c
 create mode 100644 test/c/unroll/two_loops_fail.c
 create mode 100644 test/c/unroll/while_nested.c
 create mode 100644 test/c/unroll/while_nested_fail.c

diff --git a/include/smack/SmackOptions.h b/include/smack/SmackOptions.h
index 9ca18131c..29293360c 100644
--- a/include/smack/SmackOptions.h
+++ b/include/smack/SmackOptions.h
@@ -32,6 +32,7 @@ class SmackOptions {
   static const llvm::cl::opt<bool> FloatEnabled;
   static const llvm::cl::opt<bool> MemorySafety;
   static const llvm::cl::opt<bool> IntegerOverflow;
+  static const llvm::cl::opt<bool> FailOnLoopExit;
   static const llvm::cl::opt<LLVMAssumeType> LLVMAssumes;
   static const llvm::cl::opt<bool> RustPanics;
   static const llvm::cl::opt<bool> AddTiming;
diff --git a/lib/smack/AnnotateLoopExits.cpp b/lib/smack/AnnotateLoopExits.cpp
index f5abe119f..6b7ce75f7 100644
--- a/lib/smack/AnnotateLoopExits.cpp
+++ b/lib/smack/AnnotateLoopExits.cpp
@@ -46,23 +46,22 @@ void processExitBlock(BasicBlock *block, Function *le) {
 
   SDEBUG(errs() << "Processing an Exit Block\n");
 
-  Instruction& front = block->front();
-  insertLoopEndAssertion(le,&front);
+  Instruction &front = block->front();
+  insertLoopEndAssertion(le, &front);
 }
 
 void annotateLoopEnd(Loop *loop, Function *le) {
-  //BasicBlock *headerBlock = loop->getHeader();
 
   // I imagine that it is very uncommon for a loop to have
   //   more than 5 exit points. This is a complete guess
   //   and we could probably have a better heuristic
-  SmallVector<BasicBlock *, 5> exitBlocks; 
+  SmallVector<BasicBlock *, 5> exitBlocks;
 
   loop->getExitBlocks(exitBlocks);
-  
+
   for (BasicBlock *b : exitBlocks) {
-    processExitBlock(b,le);
-  } 
+    processExitBlock(b, le);
+  }
 }
 
 bool AnnotateLoopExits::runOnModule(Module &m) {
@@ -90,5 +89,8 @@ bool AnnotateLoopExits::runOnModule(Module &m) {
 // Pass ID variable
 char AnnotateLoopExits::ID = 0;
 
-StringRef AnnotateLoopExits::getPassName() const { return "Annotate Loop Ends with assert(false)"; }
+StringRef AnnotateLoopExits::getPassName() const {
+  return "Annotate Loop Ends with assert(false)";
+}
+
 } // namespace smack
diff --git a/lib/smack/SmackOptions.cpp b/lib/smack/SmackOptions.cpp
index 8ee361e07..ecca038cd 100644
--- a/lib/smack/SmackOptions.cpp
+++ b/lib/smack/SmackOptions.cpp
@@ -77,6 +77,9 @@ const llvm::cl::opt<bool>
 const llvm::cl::opt<bool> SmackOptions::IntegerOverflow(
     "integer-overflow", llvm::cl::desc("Enable integer overflow checks"));
 
+const llvm::cl::opt<bool> SmackOptions::FailOnLoopExit("fail-on-loop-exit",
+    llvm::cl::desc("Add assert(false) to the end of each loop"));
+
 const llvm::cl::opt<LLVMAssumeType> SmackOptions::LLVMAssumes(
     "llvm-assumes",
     llvm::cl::desc(
diff --git a/share/smack/top.py b/share/smack/top.py
index fe64058db..90c03d6a1 100755
--- a/share/smack/top.py
+++ b/share/smack/top.py
@@ -518,6 +518,12 @@ def arguments():
         default=False,
         help='enable support for string')
 
+    translate_group.add_argument(
+        '--fail-on-loop-exit',
+        action='store_true',
+        default=False,
+        help='Add assert false to the end of each loop (useful for deciding how much unroll to use)')
+
     verifier_group = parser.add_argument_group('verifier options')
 
     verifier_group.add_argument(
@@ -746,6 +752,8 @@ def llvm_to_bpl(args):
         cmd += ['-integer-overflow']
     if VProperty.RUST_PANICS in args.check:
         cmd += ['-rust-panics']
+    if args.fail_on_loop_exit:
+        cmd += ['-fail-on-loop-exit']
     if args.llvm_assumes:
         cmd += ['-llvm-assumes=' + args.llvm_assumes]
     if args.float:
diff --git a/test/c/unroll/break2.c b/test/c/unroll/break2.c
new file mode 100644
index 000000000..04ba01e82
--- /dev/null
+++ b/test/c/unroll/break2.c
@@ -0,0 +1,14 @@
+#include "smack.h"
+
+// @expect verified
+// @flag --unroll=4
+
+int main(void) {
+  int a = 1;
+  while (a < 10) {
+    if (a == 5) break;
+    a++;
+  }
+
+  return a;
+}
diff --git a/test/c/unroll/break2_fail.c b/test/c/unroll/break2_fail.c
new file mode 100644
index 000000000..7dd0dcf66
--- /dev/null
+++ b/test/c/unroll/break2_fail.c
@@ -0,0 +1,14 @@
+#include "smack.h"
+
+// @expect error
+// @flag --unroll=5
+
+int main(void) {
+  int a = 1;
+  while (a < 10) {
+    if (a == 5) break;
+    a++;
+  }
+
+  return a;
+}
diff --git a/test/c/unroll/config.yml b/test/c/unroll/config.yml
new file mode 100644
index 000000000..d707344f5
--- /dev/null
+++ b/test/c/unroll/config.yml
@@ -0,0 +1,2 @@
+skip: false
+flags: [--fail-on-loop-exit]
diff --git a/test/c/unroll/for_nested.c b/test/c/unroll/for_nested.c
new file mode 100644
index 000000000..4d5ff522d
--- /dev/null
+++ b/test/c/unroll/for_nested.c
@@ -0,0 +1,14 @@
+#include "smack.h"
+
+// @expect verified
+// @flag --unroll=5
+
+int main(void) {
+  int a;
+  int b;
+  int c = 0;
+  for (a = 0; a < 5; a++)
+    for (b = 0; b < 5; b++)
+      c++;
+  return c;
+}
diff --git a/test/c/unroll/for_nested_fail.c b/test/c/unroll/for_nested_fail.c
new file mode 100644
index 000000000..92a658dec
--- /dev/null
+++ b/test/c/unroll/for_nested_fail.c
@@ -0,0 +1,14 @@
+#include "smack.h"
+
+// @expect error
+// @flag --unroll=6
+
+int main(void) {
+  int a;
+  int b;
+  int c = 0;
+  for (a = 0; a < 5; a++)
+    for (b = 0; b < 5; b++)
+      c++;
+  return c;
+}
diff --git a/test/c/unroll/for_unroll.c b/test/c/unroll/for_unroll.c
new file mode 100644
index 000000000..cfa763c35
--- /dev/null
+++ b/test/c/unroll/for_unroll.c
@@ -0,0 +1,12 @@
+#include "smack.h"
+
+// @expect verified
+// @flag --unroll=10
+
+int main(void) {
+  int a;
+  int b = 0;
+  for (a = 0; a < 10; a++)
+    b++;
+  return b;
+}
diff --git a/test/c/unroll/for_unroll_fail.c b/test/c/unroll/for_unroll_fail.c
new file mode 100644
index 000000000..536a716b0
--- /dev/null
+++ b/test/c/unroll/for_unroll_fail.c
@@ -0,0 +1,12 @@
+#include "smack.h"
+
+// @expect error
+// @flag --unroll=11
+
+int main(void) {
+  int a;
+  int b = 0;
+  for (a = 0; a < 10; a++)
+    b++;
+  return b;
+}
diff --git a/test/c/unroll/goto_exit.c b/test/c/unroll/goto_exit.c
new file mode 100644
index 000000000..d0d76f302
--- /dev/null
+++ b/test/c/unroll/goto_exit.c
@@ -0,0 +1,28 @@
+#include "smack.h"
+
+// @expect verified
+// @flag --unroll=6
+
+int func(int a) {
+  int ans = 0;
+
+  if (a < 5) {
+    goto exit;
+  }
+
+  for (int i = 0; i < a; i++)
+    ans++;
+
+exit:
+  ans++;
+  return ans;
+}
+
+int main(void) {
+  int i = func(2);
+  int j = func(6);
+
+  return i + j;
+}
+
+
diff --git a/test/c/unroll/goto_exit_fail.c b/test/c/unroll/goto_exit_fail.c
new file mode 100644
index 000000000..c25f155e5
--- /dev/null
+++ b/test/c/unroll/goto_exit_fail.c
@@ -0,0 +1,28 @@
+#include "smack.h"
+
+// @expect error
+// @flag --unroll=7
+
+int func(int a) {
+  int ans = 0;
+
+  if (a < 5) {
+    goto exit;
+  }
+
+  for (int i = 0; i < a; i++)
+    ans++;
+
+exit:
+  ans++;
+  return ans;
+}
+
+int main(void) {
+  int i = func(2);
+  int j = func(6);
+
+  return i + j;
+}
+
+
diff --git a/test/c/unroll/two_exits.c b/test/c/unroll/two_exits.c
new file mode 100644
index 000000000..b102080ed
--- /dev/null
+++ b/test/c/unroll/two_exits.c
@@ -0,0 +1,20 @@
+#include "smack.h"
+
+// @expect verified
+// @flag --unroll=5
+
+int func(int p) {
+  int a = 0;
+  while (a < 10) {
+    if (a == p) break;
+    a++;
+  }
+  return a;
+}
+
+int main(void) {
+  int i = func(5);
+  int j = func(15);
+
+  return i + j;
+}
diff --git a/test/c/unroll/two_exits_fail.c b/test/c/unroll/two_exits_fail.c
new file mode 100644
index 000000000..2f687256d
--- /dev/null
+++ b/test/c/unroll/two_exits_fail.c
@@ -0,0 +1,20 @@
+#include "smack.h"
+
+// @expect error
+// @flag --unroll=6
+
+int func(int p) {
+  int a = 0;
+  while (a < 10) {
+    if (a == p) break;
+    a++;
+  }
+  return a;
+}
+
+int main(void) {
+  int i = func(5);
+  int j = func(15);
+
+  return i + j;
+}
diff --git a/test/c/unroll/two_loops.c b/test/c/unroll/two_loops.c
new file mode 100644
index 000000000..61d9853bf
--- /dev/null
+++ b/test/c/unroll/two_loops.c
@@ -0,0 +1,16 @@
+#include "smack.h"
+
+// @expect verified
+// @flag --unroll=5
+
+int main(void) {
+  int c = 0;
+
+  for (int a = 0; a < 5; a++)
+    c++;
+
+  for (int a = 0; a < 10; a++)
+    c++;
+
+  return c;
+}
diff --git a/test/c/unroll/two_loops2.c b/test/c/unroll/two_loops2.c
new file mode 100644
index 000000000..03ddaeb16
--- /dev/null
+++ b/test/c/unroll/two_loops2.c
@@ -0,0 +1,16 @@
+#include "smack.h"
+
+// @expect verified
+// @flag --unroll=10
+
+int main(void) {
+  int c = 0;
+
+  for (int a = 0; a < 10; a++)
+    c++;
+
+  for (int a = 0; a < 5; a++)
+    c++;
+
+  return c;
+}
diff --git a/test/c/unroll/two_loops2_fail.c b/test/c/unroll/two_loops2_fail.c
new file mode 100644
index 000000000..733d3e570
--- /dev/null
+++ b/test/c/unroll/two_loops2_fail.c
@@ -0,0 +1,16 @@
+#include "smack.h"
+
+// @expect error
+// @flag --unroll=11
+
+int main(void) {
+  int c = 0;
+
+  for (int a = 0; a < 10; a++)
+    c++;
+
+  for (int a = 0; a < 5; a++)
+    c++;
+
+  return c;
+}
diff --git a/test/c/unroll/two_loops_fail.c b/test/c/unroll/two_loops_fail.c
new file mode 100644
index 000000000..39e264407
--- /dev/null
+++ b/test/c/unroll/two_loops_fail.c
@@ -0,0 +1,16 @@
+#include "smack.h"
+
+// @expect error
+// @flag --unroll=6
+
+int main(void) {
+  int c = 0;
+
+  for (int a = 0; a < 5; a++)
+    c++;
+
+  for (int a = 0; a < 10; a++)
+    c++;
+
+  return c;
+}
diff --git a/test/c/unroll/while_nested.c b/test/c/unroll/while_nested.c
new file mode 100644
index 000000000..46ff4943c
--- /dev/null
+++ b/test/c/unroll/while_nested.c
@@ -0,0 +1,19 @@
+#include "smack.h"
+
+// @expect verified
+// @flag --unroll=8
+
+int main(void) {
+  int a = 1;
+  int c = 0;
+  while (a < 9) {
+    int b = 1;
+    while (b < a) {
+      if (a % b == 0) // b divides a
+        c++;
+      b++;
+    }
+    a++;
+  }
+  return c;
+}
diff --git a/test/c/unroll/while_nested_fail.c b/test/c/unroll/while_nested_fail.c
new file mode 100644
index 000000000..6cf9b3b2b
--- /dev/null
+++ b/test/c/unroll/while_nested_fail.c
@@ -0,0 +1,19 @@
+#include "smack.h"
+
+// @expect error
+// @flag --unroll=9
+
+int main(void) {
+  int a = 1;
+  int c = 0;
+  while (a < 9) {
+    int b = 1;
+    while (b < a) {
+      if (a % b == 0) // b divides a
+        c++;
+      b++;
+    }
+    a++;
+  }
+  return c;
+}
diff --git a/tools/llvm2bpl/llvm2bpl.cpp b/tools/llvm2bpl/llvm2bpl.cpp
index 03ac9bffe..0502cfcde 100644
--- a/tools/llvm2bpl/llvm2bpl.cpp
+++ b/tools/llvm2bpl/llvm2bpl.cpp
@@ -28,6 +28,7 @@
 #include "seadsa/support/Debug.h"
 #include "seadsa/support/RemovePtrToInt.hh"
 #include "smack/AddTiming.h"
+#include "smack/AnnotateLoopExits.h"
 #include "smack/BplFilePrinter.h"
 #include "smack/CodifyStaticInits.h"
 #include "smack/ExtractContracts.h"
@@ -36,7 +37,6 @@
 #include "smack/MemorySafetyChecker.h"
 #include "smack/Naming.h"
 #include "smack/NormalizeLoops.h"
-#include "smack/AnnotateLoopExits.h"
 #include "smack/RemoveDeadDefs.h"
 #include "smack/RewriteBitwiseOps.h"
 #include "smack/RustFixes.h"
@@ -197,7 +197,9 @@ int main(int argc, char **argv) {
 
   // pass_manager.add(new llvm::StructRet());
   pass_manager.add(new smack::NormalizeLoops());
-  pass_manager.add(new smack::AnnotateLoopExits());
+  if (smack::SmackOptions::FailOnLoopExit) {
+    pass_manager.add(new smack::AnnotateLoopExits());
+  }
   pass_manager.add(new llvm::SimplifyEV());
   pass_manager.add(new llvm::SimplifyIV());
   pass_manager.add(new smack::ExtractContracts());

From 31db208e928ed8c3dfb6c0846c305051b45c6729 Mon Sep 17 00:00:00 2001
From: Jack J Garzella <jjgarzella@gmail.com>
Date: Wed, 26 Aug 2020 13:33:40 +0000
Subject: [PATCH 05/20] Some code cleanup

Removed some copypasta and leftovers from an
old name for AnnotateLoopExits.

Added a naming constant for __SMACK_LOOP_EXIT

Some general cleanup
---
 include/smack/Naming.h          |  1 +
 lib/smack/AnnotateLoopExits.cpp | 27 +++++++++++----------------
 lib/smack/Naming.cpp            |  1 +
 share/smack/lib/smack.c         |  2 +-
 4 files changed, 14 insertions(+), 17 deletions(-)

diff --git a/include/smack/Naming.h b/include/smack/Naming.h
index b0f584050..a617042e5 100644
--- a/include/smack/Naming.h
+++ b/include/smack/Naming.h
@@ -54,6 +54,7 @@ class Naming {
   static const std::string RETURN_VALUE_PROC;
   static const std::string INITIALIZE_PROC;
   static const std::string STATIC_INIT_PROC;
+  static const std::string LOOP_EXIT;
 
   static const std::string MEMORY;
   static const std::string ALLOC;
diff --git a/lib/smack/AnnotateLoopExits.cpp b/lib/smack/AnnotateLoopExits.cpp
index 6b7ce75f7..d4c4eb240 100644
--- a/lib/smack/AnnotateLoopExits.cpp
+++ b/lib/smack/AnnotateLoopExits.cpp
@@ -3,9 +3,9 @@
 //
 
 //
-// This pass normalizes loop structures to allow easier generation of Boogie
-// code when a loop edge comes from a branch. Specifically, a forwarding block
-// is added between a branching block and the loop header.
+// This pass adds an annotation to the exit of any loop, with the purpose
+// of debugging instances where the unroll bound does not unroll enough
+// to reach the loop exit. 
 //
 
 #define DEBUG_TYPE "smack-loop-unroll"
@@ -37,25 +37,21 @@ void AnnotateLoopExits::getAnalysisUsage(AnalysisUsage &AU) const {
 }
 
 // This method is for clarity and self-documentingness
-void insertLoopEndAssertion(Function *le, Instruction *insertBefore) {
+void insertLoopExitAssertion(Function *le, Instruction *insertBefore) {
   CallInst::Create(le, "", insertBefore);
 }
 
 void processExitBlock(BasicBlock *block, Function *le) {
-  // print exit block found!!
 
   SDEBUG(errs() << "Processing an Exit Block\n");
 
   Instruction &front = block->front();
-  insertLoopEndAssertion(le, &front);
+  insertLoopExitAssertion(le, &front);
 }
 
-void annotateLoopEnd(Loop *loop, Function *le) {
+void annotateLoopExit(Loop *loop, Function *le) {
 
-  // I imagine that it is very uncommon for a loop to have
-  //   more than 5 exit points. This is a complete guess
-  //   and we could probably have a better heuristic
-  SmallVector<BasicBlock *, 5> exitBlocks;
+  SmallVector<BasicBlock *, 0> exitBlocks;
 
   loop->getExitBlocks(exitBlocks);
 
@@ -65,9 +61,8 @@ void annotateLoopEnd(Loop *loop, Function *le) {
 }
 
 bool AnnotateLoopExits::runOnModule(Module &m) {
-
-  Function *le = m.getFunction("__SMACK_loop_end");
-  assert(le != NULL && "Function __SMACK_loop_end shoudl be present.");
+  Function *le = m.getFunction(Naming::LOOP_EXIT);
+  assert(le != NULL && "Function __SMACK_loop_exit should be present.");
 
   for (auto F = m.begin(), FEnd = m.end(); F != FEnd; ++F) {
     if (F->isIntrinsic() || F->empty()) {
@@ -79,7 +74,7 @@ bool AnnotateLoopExits::runOnModule(Module &m) {
          LI != LIEnd; ++LI) {
 
       SDEBUG(errs() << "Processing Loop in " << F->getName() << "\n");
-      annotateLoopEnd(*LI, le);
+      annotateLoopExit(*LI, le);
     }
   }
 
@@ -90,7 +85,7 @@ bool AnnotateLoopExits::runOnModule(Module &m) {
 char AnnotateLoopExits::ID = 0;
 
 StringRef AnnotateLoopExits::getPassName() const {
-  return "Annotate Loop Ends with assert(false)";
+  return "Annotate Loop Exits with assert(false)";
 }
 
 } // namespace smack
diff --git a/lib/smack/Naming.cpp b/lib/smack/Naming.cpp
index 9d8bb5f1c..ad019c3dc 100644
--- a/lib/smack/Naming.cpp
+++ b/lib/smack/Naming.cpp
@@ -38,6 +38,7 @@ const std::string Naming::VALUE_PROC = "__SMACK_value";
 const std::string Naming::RETURN_VALUE_PROC = "__SMACK_return_value";
 const std::string Naming::INITIALIZE_PROC = "$initialize";
 const std::string Naming::STATIC_INIT_PROC = "__SMACK_static_init";
+const std::string Naming::LOOP_EXIT = "__SMACK_loop_exit";
 
 const std::string Naming::MEMORY = "$M";
 const std::string Naming::ALLOC = "$alloc";
diff --git a/share/smack/lib/smack.c b/share/smack/lib/smack.c
index e5b9d64a4..d32dbb6cf 100644
--- a/share/smack/lib/smack.c
+++ b/share/smack/lib/smack.c
@@ -1409,7 +1409,7 @@ void __SMACK_check_overflow(int flag) {
   __SMACK_code("assert {:overflow} @ == $0;", flag);
 }
 
-void __SMACK_loop_end(void) {
+void __SMACK_loop_exit(void) {
   __SMACK_code("assert {:loopexit} false;");
 }
 

From d9c115ee98af8ed7b8590c79c0fc74c47be37ee9 Mon Sep 17 00:00:00 2001
From: Shaobo <polarishehn@gmail.com>
Date: Wed, 15 Sep 2021 19:54:15 -0700
Subject: [PATCH 06/20] Better error traces

This commit changes the error trace generation flow. Originally, we parse the
textual error trace and converts it into a more readable format. This commit
first converts the texual error trace into JSON and further pretty-print the
error trace. This enables us to have a canonical representation of the error
trace.

Pretty-printing includes removal of duplicate lines as well as Boogie assertion
failures that should be opaque to the users.

This commit also fixes #617
---
 share/smack/errtrace.py     | 218 +++++++++++++++---------------------
 share/smack/svcomp/utils.py |   4 +-
 share/smack/top.py          |   4 +-
 3 files changed, 93 insertions(+), 133 deletions(-)

diff --git a/share/smack/errtrace.py b/share/smack/errtrace.py
index 72771ecda..dabf4b710 100644
--- a/share/smack/errtrace.py
+++ b/share/smack/errtrace.py
@@ -3,6 +3,7 @@
 import shutil
 import subprocess
 import json
+from .frontend import llvm_exact_bin
 
 
 def reformat_assignment(line):
@@ -49,15 +50,16 @@ def demangle_with(func, tool):
                 stdout=subprocess.PIPE,
                 stderr=subprocess.PIPE)
             out, _ = p.communicate(input=func.encode())
-            return out.decode()
+            return out.decode().strip()
         return func
-    return functools.reduce(demangle_with, ['cxxfilt', 'rustfilt'], func)
+    return functools.reduce(demangle_with,
+                            [llvm_exact_bin('llvm-cxxfilt'), 'rustfilt'],
+                            func)
 
 
 def transform(info):
     '''Transform an error trace line'''
 
-    info = info.strip()
     if info.startswith('CALL') or info.startswith('RETURN from'):
         tokens = info.split()
         tokens[-1] = demangle(tokens[-1])
@@ -71,158 +73,116 @@ def transform(info):
         return info
 
 
-def corral_error_step(step):
-    '''Produce an error trace step based on a line of Corral error trace'''
-
-    m = re.match(r'([^\s]*)\s+Trace:\s+(Thread=\d+)\s+\((.*)[\)|;]', step)
-    if m:
-        path = m.group(1)
-        tid = m.group(2)
-        info = ','.join(map(transform,
-                            [x for x in m.group(3).split(',') if not
-                                re.search(
-                                    (r'((CALL|RETURN from)\s+(\$|__SMACK))|'
-                                     r'Done|ASSERTION'), x)]))
-        return '{0}\t{1}  {2}'.format(path, tid, info)
-    else:
-        return step
-
-
-def error_step(step):
-    '''Produce an error trace step based on a line of verifier output'''
-
-    FILENAME = r'[\w#$~%.\/-]*'
-    step = re.match(r"(\s*)(%s)\((\d+),\d+\): (.*)" % FILENAME, step)
-    if step:
-        if re.match('.*[.]bpl$', step.group(2)):
-            line_no = int(step.group(3))
-            message = step.group(4)
-            if re.match(r'.*\$bb\d+.*', message):
-                message = ""
-            with open(step.group(2)) as f:
-                for line in f.read().splitlines(True)[line_no:line_no + 10]:
-                    src = re.match(
-                        r".*{:sourceloc \"(%s)\", (\d+), (\d+)}" %
-                        FILENAME, line)
-                    if src:
-                        return "%s%s(%s,%s): %s" % (step.group(1), src.group(
-                            1), src.group(2), src.group(3), message)
-        else:
-            return corral_error_step(step.group(0))
-    else:
-        return None
-
-
-def error_trace(verifier_output, args):
+def error_trace(verifier_output, verifier):
     '''Generate string error trace.'''
+    from .top import VResult
+
+    traces = json_output(VResult.ERROR, verifier_output, verifier)['traces']
+    output = '\n'.join(
+        map(
+            lambda trace: '{0}({1},{2}): {3}'.format(
+                trace['file'],
+                trace['line'],
+                trace['column'],
+                trace['description']), traces))
+    return output
 
-    trace = ""
-    for line in verifier_output.splitlines(True):
-        step = error_step(line)
-        if step:
-            m = re.match('(.*): [Ee]rror [A-Z0-9]+: (.*)', step)
-            if m:
-                trace += "%s: %s\nExecution trace:\n" % (
-                    m.group(1), m.group(2))
-            else:
-                trace += ('' if step[0] == ' ' else '    ') + step + "\n"
 
-    return trace
+def smackdOutput(result, output, verifier):
+    return json.dumps(json_output(result, output, verifier))
 
 
-def smackdOutput(result, corralOutput):
+def json_output(result, output, verifier):
     '''Convert error traces into JSON format'''
 
     from .top import VResult
 
+    def merger(traces, trace):
+        if len(traces) == 0:
+            return [trace]
+        last_trace = traces[-1]
+        if (last_trace['file'] == trace['file']
+            and last_trace['line'] == trace['line']
+                and last_trace['column'] == trace['column']):
+            if len(trace['description']) != 0:
+                if len(last_trace['description']) == 0:
+                    last_trace['description'] = trace['description']
+                else:
+                    last_trace['description'] += (', ' + trace['description'])
+            return traces
+        else:
+            return traces + [trace]
+
     if not (result is VResult.VERIFIED or result in VResult.ERROR):
         return
 
     FILENAME = r'[\w#$~%.\/-]+'
-    traceP = re.compile(
-        ('('
-         + FILENAME
-         + r')\((\d+),(\d+)\): Trace: Thread=(\d+)\s+\((.*(;\n)?.*)\)'))
-    # test1.i(223,16): Trace: Thread=1  (ASSERTION FAILS assert false;
-    errorP = re.compile(
-        ('('
-         + FILENAME
-         + r')\((\d+),(\d+)\): Trace: Thread=\d+\s+\(ASSERTION FAILS'))
+    failsAt = None
 
     if result is VResult.VERIFIED:
         json_data = {
-            'verifier': 'corral',
+            'verifier': verifier,
             'passed?': True
         }
-    else:
+    elif verifier == 'boogie':
+        traces = []
+        traceP = re.compile(r"(\s*)(%s)\((\d+),\d+\):" % FILENAME)
+        steps = re.findall(traceP, output)
+        for step in steps:
+            if re.match('.*[.]bpl$', step[1]):
+                line_no = int(step[2])
+                with open(step[1]) as f:
+                    for ln in f.read().splitlines(True)[line_no:line_no + 10]:
+                        src = re.match(
+                            r".*{:sourceloc \"(%s)\", (\d+), (\d+)}" %
+                            FILENAME, ln)
+                        if src:
+                            traces.append(
+                                {'file': src.group(1),
+                                 'line': src.group(2),
+                                 'column': src.group(3),
+                                 'description': ''})
+                            break
+    elif verifier == 'corral':
         traces = []
-        raw_data = re.findall(traceP, corralOutput)
-        for t in raw_data:
-            file_name = t[0]
-            line_num = t[1]
-            col_num = t[2]
-            thread_id = t[3]
-            description = t[4]
+        traceP = re.compile(
+            ('('
+             + FILENAME
+             + r')\((\d+),(\d+)\): Trace: Thread=(\d+)\s+\((.*(;\n)?.*)\)'))
+        raw_data = re.findall(traceP, output)
+        for step in raw_data:
+            file_name = step[0]
+            line_num = step[1]
+            col_num = step[2]
+            thread_id = step[3]
+            description = step[4]
+            if 'ASSERTION FAILS' in description:
+                description = re.sub('ASSERTION FAILS.*;\n', '', description)
+                failsAt = {
+                    'file': file_name,
+                    'line': line_num,
+                    'column': col_num,
+                    'description': ''}
+
             for token in description.split(','):
+                token = token.strip()
+                if re.search(
+                  (r'((CALL|RETURN from)\s+(\$|__SMACK))|'
+                   r'Done|ASSERTION'), token) is not None:
+                    continue
+                token = transform(token)
                 traces.append(
                     {'threadid': thread_id,
                      'file': file_name,
                      'line': line_num,
                      'column': col_num,
                      'description': token,
-                     'assumption': transform(token) if '=' in token else ''})
-
-        r"""filename = ''
-        lineno = 0
-        colno = 0
-        threadid = 0
-        desc = ''
-        for traceLine in corralOutput.splitlines(True):
-            traceMatch = traceP.match(traceLine)
-            if traceMatch:
-                filename = str(traceMatch.group(1))
-                lineno = int(traceMatch.group(2))
-                colno = int(traceMatch.group(3))
-                threadid = int(traceMatch.group(4))
-                desc = str(traceMatch.group(6))
-                for e in desc.split(','):
-                    e = e.strip()
-                    assm = re.sub(
-                        r'=(\s*\d+)bv\d+',
-                        r'=\1',
-                        e) if '=' in e else ''
-                    trace = {'threadid': threadid,
-                             'file': filename,
-                             'line': lineno,
-                             'column': colno,
-                             'description': e,
-                             'assumption': assm}
-                    traces.append(trace)
-            else:
-                errorMatch = errorP.match(traceLine)
-                if errorMatch:
-                    filename = str(errorMatch.group(1))
-                    lineno = int(errorMatch.group(2))
-                    colno = int(errorMatch.group(3))
-                    desc = str(errorMatch.group(4))"""
-        errorMatch = errorP.search(corralOutput)
-        assert errorMatch, 'Failed to obtain assertion failure info!'
-        filename = str(errorMatch.group(1))
-        lineno = int(errorMatch.group(2))
-        colno = int(errorMatch.group(3))
-
-        failsAt = {
-            'file': filename,
-            'line': lineno,
-            'column': colno,
-            'description': result.description()}
-
-        json_data = {
-            'verifier': 'corral',
+                     'assumption': token if '=' in token else ''})
+    json_data = {
+            'verifier': verifier,
             'passed?': False,
             'failsAt': failsAt,
             'threadCount': 1,
-            'traces': traces
-        }
-    json_string = json.dumps(json_data)
-    return json_string
+            'traces': functools.reduce(merger, traces, [])
+    }
+    return json_data
diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index 02dfef512..0db4a50c9 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -110,7 +110,7 @@ def verify_bpl_svcomp(args):
     heurTrace += "Found a bug during normal inlining.\n"
 
     if not args.quiet:
-      error = smack.top.error_trace(verifier_output, args)
+      error = smack.top.error_trace(verifier_output, 'corral')
       print(error)
 
   elif result is VResult.TIMEOUT: #normal inlining
@@ -170,7 +170,7 @@ def write_error_file(args, status, verifier_output):
     if args.language == 'svcomp':
       error = smackJsonToXmlGraph(smackdOutput(status, verifier_output), args, hasBug, status)
     elif hasBug:
-      error = smack.top.error_trace(verifier_output, args)
+      error = smack.top.error_trace(verifier_output, 'corral')
     if error is not None:
       with open(args.error_file, 'w') as f:
         f.write(error.decode('utf-8'))
diff --git a/share/smack/top.py b/share/smack/top.py
index fe64058db..fcf47e205 100755
--- a/share/smack/top.py
+++ b/share/smack/top.py
@@ -948,10 +948,10 @@ def verify_bpl(args):
     result = verification_result(verifier_output, args.verifier)
 
     if args.smackd:
-        print(smackdOutput(result, verifier_output))
+        print(smackdOutput(result, verifier_output, args.verifier))
     else:
         if result in VResult.ERROR:
-            error = error_trace(verifier_output, args)
+            error = error_trace(verifier_output, args.verifier)
 
             if args.error_file:
                 with open(args.error_file, 'w') as f:

From 51919d225c3b81b88fd15aa9fd7c5c0fe9adce77 Mon Sep 17 00:00:00 2001
From: JJ Garzella <jjgarzella@gmail.com>
Date: Thu, 23 Sep 2021 15:42:00 -0700
Subject: [PATCH 07/20] Format code

Whitespace corrections and other formatting
as per clang-format-11
---
 lib/smack/AnnotateLoopExits.cpp | 6 +++---
 lib/smack/SmackOptions.cpp      | 3 ++-
 share/smack/lib/smack.c         | 4 +---
 test/c/unroll/break2.c          | 3 ++-
 test/c/unroll/break2_fail.c     | 3 ++-
 test/c/unroll/goto_exit.c       | 2 --
 test/c/unroll/goto_exit_fail.c  | 2 --
 test/c/unroll/two_exits.c       | 3 ++-
 test/c/unroll/two_exits_fail.c  | 3 ++-
 9 files changed, 14 insertions(+), 15 deletions(-)

diff --git a/lib/smack/AnnotateLoopExits.cpp b/lib/smack/AnnotateLoopExits.cpp
index d4c4eb240..83a64b8d3 100644
--- a/lib/smack/AnnotateLoopExits.cpp
+++ b/lib/smack/AnnotateLoopExits.cpp
@@ -5,21 +5,21 @@
 //
 // This pass adds an annotation to the exit of any loop, with the purpose
 // of debugging instances where the unroll bound does not unroll enough
-// to reach the loop exit. 
+// to reach the loop exit.
 //
 
 #define DEBUG_TYPE "smack-loop-unroll"
 #include "smack/AnnotateLoopExits.h"
-#include "smack/Naming.h"
 #include "smack/Debug.h"
+#include "smack/Naming.h"
 #include "llvm/Analysis/LoopInfo.h"
-#include "llvm/Transforms/Utils.h"
 #include "llvm/IR/Constants.h"
 #include "llvm/IR/Dominators.h"
 #include "llvm/IR/IRBuilder.h"
 #include "llvm/IR/InstIterator.h"
 #include "llvm/IR/Module.h"
 #include "llvm/IR/ValueSymbolTable.h"
+#include "llvm/Transforms/Utils.h"
 #include <map>
 #include <set>
 #include <vector>
diff --git a/lib/smack/SmackOptions.cpp b/lib/smack/SmackOptions.cpp
index ecca038cd..1ce8fdc2f 100644
--- a/lib/smack/SmackOptions.cpp
+++ b/lib/smack/SmackOptions.cpp
@@ -77,7 +77,8 @@ const llvm::cl::opt<bool>
 const llvm::cl::opt<bool> SmackOptions::IntegerOverflow(
     "integer-overflow", llvm::cl::desc("Enable integer overflow checks"));
 
-const llvm::cl::opt<bool> SmackOptions::FailOnLoopExit("fail-on-loop-exit",
+const llvm::cl::opt<bool> SmackOptions::FailOnLoopExit(
+    "fail-on-loop-exit",
     llvm::cl::desc("Add assert(false) to the end of each loop"));
 
 const llvm::cl::opt<LLVMAssumeType> SmackOptions::LLVMAssumes(
diff --git a/share/smack/lib/smack.c b/share/smack/lib/smack.c
index d32dbb6cf..218fa0503 100644
--- a/share/smack/lib/smack.c
+++ b/share/smack/lib/smack.c
@@ -1409,9 +1409,7 @@ void __SMACK_check_overflow(int flag) {
   __SMACK_code("assert {:overflow} @ == $0;", flag);
 }
 
-void __SMACK_loop_exit(void) {
-  __SMACK_code("assert {:loopexit} false;");
-}
+void __SMACK_loop_exit(void) { __SMACK_code("assert {:loopexit} false;"); }
 
 char __VERIFIER_nondet_char(void) {
   char x = __SMACK_nondet_char();
diff --git a/test/c/unroll/break2.c b/test/c/unroll/break2.c
index 04ba01e82..a20d41dfc 100644
--- a/test/c/unroll/break2.c
+++ b/test/c/unroll/break2.c
@@ -6,7 +6,8 @@
 int main(void) {
   int a = 1;
   while (a < 10) {
-    if (a == 5) break;
+    if (a == 5)
+      break;
     a++;
   }
 
diff --git a/test/c/unroll/break2_fail.c b/test/c/unroll/break2_fail.c
index 7dd0dcf66..a2213e38f 100644
--- a/test/c/unroll/break2_fail.c
+++ b/test/c/unroll/break2_fail.c
@@ -6,7 +6,8 @@
 int main(void) {
   int a = 1;
   while (a < 10) {
-    if (a == 5) break;
+    if (a == 5)
+      break;
     a++;
   }
 
diff --git a/test/c/unroll/goto_exit.c b/test/c/unroll/goto_exit.c
index d0d76f302..290e288ec 100644
--- a/test/c/unroll/goto_exit.c
+++ b/test/c/unroll/goto_exit.c
@@ -24,5 +24,3 @@ int main(void) {
 
   return i + j;
 }
-
-
diff --git a/test/c/unroll/goto_exit_fail.c b/test/c/unroll/goto_exit_fail.c
index c25f155e5..b888b14b5 100644
--- a/test/c/unroll/goto_exit_fail.c
+++ b/test/c/unroll/goto_exit_fail.c
@@ -24,5 +24,3 @@ int main(void) {
 
   return i + j;
 }
-
-
diff --git a/test/c/unroll/two_exits.c b/test/c/unroll/two_exits.c
index b102080ed..4bbf842ea 100644
--- a/test/c/unroll/two_exits.c
+++ b/test/c/unroll/two_exits.c
@@ -6,7 +6,8 @@
 int func(int p) {
   int a = 0;
   while (a < 10) {
-    if (a == p) break;
+    if (a == p)
+      break;
     a++;
   }
   return a;
diff --git a/test/c/unroll/two_exits_fail.c b/test/c/unroll/two_exits_fail.c
index 2f687256d..c35a9f9b8 100644
--- a/test/c/unroll/two_exits_fail.c
+++ b/test/c/unroll/two_exits_fail.c
@@ -6,7 +6,8 @@
 int func(int p) {
   int a = 0;
   while (a < 10) {
-    if (a == p) break;
+    if (a == p)
+      break;
     a++;
   }
   return a;

From 57be28b8e6467b9886c722258a0cabb439631fb3 Mon Sep 17 00:00:00 2001
From: JJ Garzella <jjgarzella@gmail.com>
Date: Thu, 23 Sep 2021 15:59:02 -0700
Subject: [PATCH 08/20] Fix Python formatting error

Fixes the formatting in top.py, as per flake8.

This commit should be squashed into the previous
one eventually.
---
 share/smack/top.py | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/share/smack/top.py b/share/smack/top.py
index 90c03d6a1..f3d8af6e4 100755
--- a/share/smack/top.py
+++ b/share/smack/top.py
@@ -522,7 +522,8 @@ def arguments():
         '--fail-on-loop-exit',
         action='store_true',
         default=False,
-        help='Add assert false to the end of each loop (useful for deciding how much unroll to use)')
+        help='''Add assert false to the end of each loop
+                (useful for deciding how much unroll to use)''')
 
     verifier_group = parser.add_argument_group('verifier options')
 

From b867ee44b6a5f1dfe86ad1e1961742fb1154c305 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Thu, 7 Oct 2021 22:24:12 -0600
Subject: [PATCH 09/20] Cleans up JSON output generation

We deprecated smackd output since it has not been used for years.
Renamed it as json output. Also, fixed a bug related to json
output generation.

Closes #759
---
 share/smack/errtrace.py              |  6 +++--
 share/smack/svcomp/toSVCOMPformat.py |  2 +-
 share/smack/svcomp/utils.py          |  4 +--
 share/smack/top.py                   | 40 +++++++++++++++-------------
 4 files changed, 28 insertions(+), 24 deletions(-)

diff --git a/share/smack/errtrace.py b/share/smack/errtrace.py
index dabf4b710..f4ef9ad67 100644
--- a/share/smack/errtrace.py
+++ b/share/smack/errtrace.py
@@ -88,7 +88,7 @@ def error_trace(verifier_output, verifier):
     return output
 
 
-def smackdOutput(result, output, verifier):
+def json_output_str(result, output, verifier):
     return json.dumps(json_output(result, output, verifier))
 
 
@@ -124,7 +124,9 @@ def merger(traces, trace):
             'verifier': verifier,
             'passed?': True
         }
-    elif verifier == 'boogie':
+        return json_data
+
+    if verifier == 'boogie':
         traces = []
         traceP = re.compile(r"(\s*)(%s)\((\d+),\d+\):" % FILENAME)
         steps = re.findall(traceP, output)
diff --git a/share/smack/svcomp/toSVCOMPformat.py b/share/smack/svcomp/toSVCOMPformat.py
index 346ccbef5..4f3809b72 100644
--- a/share/smack/svcomp/toSVCOMPformat.py
+++ b/share/smack/svcomp/toSVCOMPformat.py
@@ -139,7 +139,7 @@ def isSMACKInitFunc(funcName):
   return funcName == '$initialize' or funcName == '__SMACK_static_init' or funcName == '__SMACK_init_func_memory_model'
 
 def smackJsonToXmlGraph(strJsonOutput, args, hasBug, status):
-    """Converts output from SMACK (in the smackd json format) to a graphml
+    """Converts output from SMACK (in the json format) to a graphml
        format that conforms to the SVCOMP witness file format"""
     # Build tree & start node
     tree = buildEmptyXmlGraph(args, hasBug)
diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index 0db4a50c9..cf2851747 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -158,7 +158,7 @@ def verify_bpl_svcomp(args):
 def write_error_file(args, status, verifier_output):
   from smack.top import VProperty
   from smack.top import VResult
-  from smack.errtrace import smackdOutput
+  from smack.errtrace import json_output_str
   #return
   if status is VResult.UNKNOWN:
     return
@@ -168,7 +168,7 @@ def write_error_file(args, status, verifier_output):
   if args.error_file:
     error = None
     if args.language == 'svcomp':
-      error = smackJsonToXmlGraph(smackdOutput(status, verifier_output), args, hasBug, status)
+      error = smackJsonToXmlGraph(json_output_str(status, verifier_output), args, hasBug, status)
     elif hasBug:
       error = smack.top.error_trace(verifier_output, 'corral')
     if error is not None:
diff --git a/share/smack/top.py b/share/smack/top.py
index fcf47e205..5723f4596 100755
--- a/share/smack/top.py
+++ b/share/smack/top.py
@@ -12,7 +12,7 @@
     llvm_exact_bin
 from .replay import replay_error_trace
 from .frontend import link_bc_files, frontends, languages, extra_libs
-from .errtrace import error_trace, smackdOutput
+from .errtrace import error_trace, json_output_str
 
 VERSION = '2.7.1'
 
@@ -329,6 +329,9 @@ def arguments():
     parser.add_argument('-w', '--error-file', metavar='FILE', default=None,
                         type=str, help='save error trace/witness to FILE')
 
+    parser.add_argument('--json-file', metavar='FILE', default=None,
+                        type=str, help='generate JSON output to FILE')
+
     frontend_group = parser.add_argument_group('front-end options')
 
     frontend_group.add_argument('-x', '--language', metavar='LANG',
@@ -578,9 +581,6 @@ def arguments():
         type=int,
         help='maximum reported assertion violations [default: %(default)s]')
 
-    verifier_group.add_argument('--smackd', action="store_true", default=False,
-                                help='generate JSON-format output for SMACKd')
-
     verifier_group.add_argument(
         '--svcomp-property',
         metavar='FILE',
@@ -947,23 +947,24 @@ def verify_bpl(args):
     verifier_output = transform_out(args, verifier_output)
     result = verification_result(verifier_output, args.verifier)
 
-    if args.smackd:
-        print(smackdOutput(result, verifier_output, args.verifier))
-    else:
-        if result in VResult.ERROR:
-            error = error_trace(verifier_output, args.verifier)
+    if args.json_file:
+        with open(args.json_file, 'w') as f:
+            f.write(json_output_str(result, verifier_output, args.verifier))
 
-            if args.error_file:
-                with open(args.error_file, 'w') as f:
-                    f.write(error)
+    if result in VResult.ERROR:
+        error = error_trace(verifier_output, args.verifier)
 
-            if not args.quiet:
-                print(error)
+        if args.error_file:
+            with open(args.error_file, 'w') as f:
+                f.write(error)
+
+        if not args.quiet:
+            print(error)
 
-            if args.replay:
-                replay_error_trace(verifier_output, args)
-        print(result.message(args))
-        sys.exit(result.return_code())
+        if args.replay:
+            replay_error_trace(verifier_output, args)
+    print(result.message(args))
+    return result.return_code()
 
 
 def clean_up_upon_sigterm(main):
@@ -991,7 +992,8 @@ def main():
             if not args.quiet:
                 print("SMACK generated %s" % args.bpl_file)
         else:
-            verify_bpl(args)
+            return_code = verify_bpl(args)
+            sys.exit(return_code)
 
     except KeyboardInterrupt:
         sys.exit("SMACK aborted by keyboard interrupt.")

From be2d6c5faf9ddd1aaadfba38e3ec10de85d914b6 Mon Sep 17 00:00:00 2001
From: Shaobo <polarishehn@gmail.com>
Date: Sat, 9 Oct 2021 09:32:44 -0700
Subject: [PATCH 10/20] Upgrade SMACK to support LLVM 12

Upgraded SMACK to support LLVM 12. Fixed a bunch of warnings that appeared.
Using clang by default to build SMACK.
Removed demangling from error trace generation. We plan to add it back.
---
 bin/build.sh                           |  4 +-
 bin/versions                           |  4 +-
 docs/installation.md                   |  8 +--
 include/smack/BoogieAst.h              | 68 +++++++++++------------
 include/smack/BplFilePrinter.h         |  8 +--
 include/smack/BplPrinter.h             |  4 +-
 include/smack/CodifyStaticInits.h      |  4 +-
 include/smack/DSAWrapper.h             |  4 +-
 include/smack/ExtractContracts.h       |  4 +-
 include/smack/IntegerOverflowChecker.h |  4 +-
 include/smack/MemorySafetyChecker.h    |  2 +-
 include/smack/Prelude.h                | 46 ++++++++--------
 include/smack/Regions.h                |  4 +-
 include/smack/RemoveDeadDefs.h         |  2 +-
 include/smack/RewriteBitwiseOps.h      |  4 +-
 include/smack/RustFixes.h              |  4 +-
 include/smack/SimplifyLibCalls.h       |  4 +-
 include/smack/SmackModuleGenerator.h   |  4 +-
 include/smack/SplitAggregateValue.h    |  2 +-
 include/smack/VectorOperations.h       |  4 +-
 include/smack/VerifierCodeMetadata.h   |  4 +-
 include/utils/Devirt.h                 |  4 +-
 include/utils/MergeGEP.h               |  2 +-
 include/utils/SimplifyExtractValue.h   |  2 +-
 include/utils/SimplifyInsertValue.h    |  2 +-
 lib/smack/AddTiming.cpp                |  3 +-
 lib/smack/RewriteBitwiseOps.cpp        |  3 +-
 lib/smack/SmackInstGenerator.cpp       | 14 ++---
 lib/smack/SmackRep.cpp                 |  2 +-
 lib/smack/VectorOperations.cpp         | 34 ++++++------
 lib/utils/Devirt.cpp                   | 12 +----
 sea-dsa                                |  2 +-
 share/smack/errtrace.py                | 38 +++----------
 share/smack/svcomp/utils.py            |  2 +-
 test/c/failing/floppy_false.i.cil.c    | 66 +++++++++++++----------
 test/c/failing/floppy_true.i.cil.c     | 66 +++++++++++++----------
 test/c/ntdrivers/kbfiltr_false.i.cil.c | 24 ++++-----
 test/c/ntdrivers/parport_false.i.cil.c | 75 ++++++++++++++++----------
 test/c/ntdrivers/parport_true.i.cil.c  | 75 ++++++++++++++++----------
 tools/externalizer/ExternalizePass.h   |  4 +-
 40 files changed, 327 insertions(+), 295 deletions(-)

diff --git a/bin/build.sh b/bin/build.sh
index a48d6b37c..bfc441fb1 100755
--- a/bin/build.sh
+++ b/bin/build.sh
@@ -489,7 +489,9 @@ if [ ${BUILD_SMACK} -eq 1 ] ; then
 
   mkdir -p ${SMACK_DIR}/build
   cd ${SMACK_DIR}/build
-  cmake ${CMAKE_INSTALL_PREFIX} -DCMAKE_BUILD_TYPE=Debug .. -G Ninja
+  cmake -DCMAKE_CXX_COMPILER=clang++-${LLVM_SHORT_VERSION} \
+        -DCMAKE_C_COMPILER=clang-${LLVM_SHORT_VERSION} ${CMAKE_INSTALL_PREFIX} \
+        -DCMAKE_BUILD_TYPE=Debug .. -G Ninja
   ninja
 
   if [ -n "${CMAKE_INSTALL_PREFIX}" ] ; then
diff --git a/bin/versions b/bin/versions
index 940c6ab4d..e7a5d4319 100644
--- a/bin/versions
+++ b/bin/versions
@@ -5,6 +5,6 @@ BOOGIE_VERSION="2.9.1"
 CORRAL_VERSION="1.1.8"
 SYMBOOGLIX_COMMIT="ccb2e7f2b3"
 LOCKPWN_COMMIT="12ba58f1ec"
-LLVM_SHORT_VERSION="11"
-LLVM_FULL_VERSION="11.1.0"
+LLVM_SHORT_VERSION="12"
+LLVM_FULL_VERSION="12.0.1"
 RUST_VERSION="nightly-2021-03-01"
diff --git a/docs/installation.md b/docs/installation.md
index a160e50d2..ae6ee2502 100644
--- a/docs/installation.md
+++ b/docs/installation.md
@@ -74,8 +74,8 @@ to Docker's official documentation.
 
 SMACK depends on the following projects:
 
-* [LLVM][] version [11.1.0][LLVM-11.1.0]
-* [Clang][] version [11.1.0][Clang-11.1.0]
+* [LLVM][] version [12.0.1][LLVM-12.0.1]
+* [Clang][] version [12.0.1][Clang-12.0.1]
 * [Boost][] version 1.55 or greater
 * [Python][] version 3.6.8 or greater
 * [Ninja][] version 1.5.1 or greater
@@ -189,9 +189,9 @@ shell in the `test` directory by executing
 [CMake]: http://www.cmake.org
 [Python]: http://www.python.org
 [LLVM]: http://llvm.org
-[LLVM-11.1.0]: http://llvm.org/releases/download.html#11.1.0
+[LLVM-12.0.1]: http://llvm.org/releases/download.html#12.0.1
 [Clang]: http://clang.llvm.org
-[Clang-11.1.0]: http://llvm.org/releases/download.html#11.1.0
+[Clang-12.0.1]: http://llvm.org/releases/download.html#12.0.1
 [Boogie]: https://github.com/boogie-org/boogie
 [Corral]: https://github.com/boogie-org/corral
 [Z3]: https://github.com/Z3Prover/z3/
diff --git a/include/smack/BoogieAst.h b/include/smack/BoogieAst.h
index ffddfeac0..06e77157c 100644
--- a/include/smack/BoogieAst.h
+++ b/include/smack/BoogieAst.h
@@ -85,7 +85,7 @@ class BinExpr : public Expr {
 public:
   BinExpr(const Binary b, const Expr *l, const Expr *r)
       : op(b), lhs(l), rhs(r) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
 };
 
 class FunExpr : public Expr {
@@ -94,7 +94,7 @@ class FunExpr : public Expr {
 
 public:
   FunExpr(std::string f, std::list<const Expr *> xs) : fun(f), args(xs) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
 };
 
 class BoolLit : public Expr {
@@ -102,7 +102,7 @@ class BoolLit : public Expr {
 
 public:
   BoolLit(bool b) : val(b) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
 };
 
 class RModeLit : public Expr {
@@ -110,7 +110,7 @@ class RModeLit : public Expr {
 
 public:
   RModeLit(RModeKind v) : val(v) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
 };
 
 class IntLit : public Expr {
@@ -128,7 +128,7 @@ class IntLit : public Expr {
     s << v;
     val = s.str();
   }
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
 };
 
 class BvLit : public Expr {
@@ -142,7 +142,7 @@ class BvLit : public Expr {
     s << v;
     val = s.str();
   }
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
 };
 
 class FPLit : public Expr {
@@ -158,7 +158,7 @@ class FPLit : public Expr {
       : neg(n), sig(s), expo(e), sigSize(ss), expSize(es) {}
   FPLit(std::string v, unsigned ss, unsigned es)
       : specialValue(v), sigSize(ss), expSize(es) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
 };
 
 class StringLit : public Expr {
@@ -166,7 +166,7 @@ class StringLit : public Expr {
 
 public:
   StringLit(std::string v) : val(v) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
 };
 
 class NegExpr : public Expr {
@@ -174,7 +174,7 @@ class NegExpr : public Expr {
 
 public:
   NegExpr(const Expr *e) : expr(e) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
 };
 
 class NotExpr : public Expr {
@@ -182,7 +182,7 @@ class NotExpr : public Expr {
 
 public:
   NotExpr(const Expr *e) : expr(e) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
 };
 
 class QuantExpr : public Expr {
@@ -197,7 +197,7 @@ class QuantExpr : public Expr {
 public:
   QuantExpr(Quantifier q, std::list<Binding> vs, const Expr *e)
       : quant(q), vars(vs), expr(e) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
 };
 
 class SelExpr : public Expr {
@@ -208,7 +208,7 @@ class SelExpr : public Expr {
   SelExpr(const Expr *a, std::list<const Expr *> i) : base(a), idxs(i) {}
   SelExpr(const Expr *a, const Expr *i)
       : base(a), idxs(std::list<const Expr *>(1, i)) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
 };
 
 class UpdExpr : public Expr {
@@ -221,7 +221,7 @@ class UpdExpr : public Expr {
       : base(a), idxs(i), val(v) {}
   UpdExpr(const Expr *a, const Expr *i, const Expr *v)
       : base(a), idxs(std::list<const Expr *>(1, i)), val(v) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
 };
 
 class VarExpr : public Expr {
@@ -230,7 +230,7 @@ class VarExpr : public Expr {
 public:
   VarExpr(std::string v) : var(v) {}
   std::string name() const { return var; }
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
 };
 
 class IfThenElseExpr : public Expr {
@@ -241,7 +241,7 @@ class IfThenElseExpr : public Expr {
 public:
   IfThenElseExpr(const Expr *c, const Expr *t, const Expr *e)
       : cond(c), trueValue(t), falseValue(e) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
 };
 
 class BvExtract : public Expr {
@@ -252,7 +252,7 @@ class BvExtract : public Expr {
 public:
   BvExtract(const Expr *var, const Expr *upper, const Expr *lower)
       : var(var), upper(upper), lower(lower) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
 };
 
 class BvConcat : public Expr {
@@ -261,7 +261,7 @@ class BvConcat : public Expr {
 
 public:
   BvConcat(const Expr *left, const Expr *right) : left(left), right(right) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
 };
 
 class Attr {
@@ -343,7 +343,7 @@ class AssertStmt : public Stmt {
 public:
   AssertStmt(const Expr *e, std::list<const Attr *> ax)
       : Stmt(ASSERT), expr(e), attrs(ax) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
   static bool classof(const Stmt *S) { return S->getKind() == ASSERT; }
 };
 
@@ -354,7 +354,7 @@ class AssignStmt : public Stmt {
 public:
   AssignStmt(std::list<const Expr *> lhs, std::list<const Expr *> rhs)
       : Stmt(ASSIGN), lhs(lhs), rhs(rhs) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
   static bool classof(const Stmt *S) { return S->getKind() == ASSIGN; }
 };
 
@@ -372,7 +372,7 @@ class AssumeStmt : public Stmt {
     }
     return false;
   }
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
   static bool classof(const Stmt *S) { return S->getKind() == ASSUME; }
 };
 
@@ -387,7 +387,7 @@ class CallStmt : public Stmt {
            std::list<const Expr *> args, std::list<std::string> rets)
       : Stmt(CALL), proc(p), attrs(attrs), params(args), returns(rets) {}
 
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
   static bool classof(const Stmt *S) { return S->getKind() == CALL; }
 };
 
@@ -396,7 +396,7 @@ class Comment : public Stmt {
 
 public:
   Comment(std::string s) : Stmt(COMMENT), str(s) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
   static bool classof(const Stmt *S) { return S->getKind() == COMMENT; }
 };
 
@@ -405,7 +405,7 @@ class GotoStmt : public Stmt {
 
 public:
   GotoStmt(std::list<std::string> ts) : Stmt(GOTO), targets(ts) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
   static bool classof(const Stmt *S) { return S->getKind() == GOTO; }
 };
 
@@ -414,7 +414,7 @@ class HavocStmt : public Stmt {
 
 public:
   HavocStmt(std::list<std::string> vs) : Stmt(HAVOC), vars(vs) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
   static bool classof(const Stmt *S) { return S->getKind() == HAVOC; }
 };
 
@@ -423,7 +423,7 @@ class ReturnStmt : public Stmt {
 
 public:
   ReturnStmt(const Expr *e = nullptr) : Stmt(RETURN), expr(e) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
   static bool classof(const Stmt *S) { return S->getKind() == RETURN; }
 };
 
@@ -432,7 +432,7 @@ class CodeStmt : public Stmt {
 
 public:
   CodeStmt(std::string s) : Stmt(CODE), code(s) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
   static bool classof(const Stmt *S) { return S->getKind() == CODE; }
 };
 
@@ -494,7 +494,7 @@ class TypeDecl : public Decl {
 public:
   TypeDecl(std::string n, std::string t, std::list<const Attr *> ax)
       : Decl(TYPE, n, ax), alias(t) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
   static bool classof(const Decl *D) { return D->getKind() == TYPE; }
 };
 
@@ -504,7 +504,7 @@ class AxiomDecl : public Decl {
 
 public:
   AxiomDecl(std::string n, const Expr *e) : Decl(AXIOM, n, {}), expr(e) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
   static bool classof(const Decl *D) { return D->getKind() == AXIOM; }
 };
 
@@ -515,7 +515,7 @@ class ConstDecl : public Decl {
 public:
   ConstDecl(std::string n, std::string t, std::list<const Attr *> ax, bool u)
       : Decl(CONSTANT, n, ax), type(t), unique(u) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
   static bool classof(const Decl *D) { return D->getKind() == CONSTANT; }
 };
 
@@ -528,7 +528,7 @@ class FuncDecl : public Decl {
   FuncDecl(std::string n, std::list<const Attr *> ax, std::list<Binding> ps,
            std::string t, const Expr *b)
       : Decl(FUNCTION, n, ax), params(ps), type(t), body(b) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
   static bool classof(const Decl *D) { return D->getKind() == FUNCTION; }
 };
 
@@ -537,7 +537,7 @@ class VarDecl : public Decl {
 
 public:
   VarDecl(std::string n, std::string t) : Decl(VARIABLE, n, {}), type(t) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
   static bool classof(const Decl *D) { return D->getKind() == VARIABLE; }
 };
 
@@ -595,7 +595,7 @@ class CodeContainer {
 class CodeExpr : public Expr, public CodeContainer {
 public:
   CodeExpr(DeclarationList ds, BlockList bs) : CodeContainer(ds, bs) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
 };
 
 class ProcDecl : public Decl, public CodeContainer {
@@ -630,7 +630,7 @@ class ProcDecl : public Decl, public CodeContainer {
   spec_iterator ensures_end() { return ensures.end(); }
   SpecificationList &getEnsures() { return ensures; }
 
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
   static bool classof(const Decl *D) { return D->getKind() == PROCEDURE; }
 };
 
@@ -639,7 +639,7 @@ class CodeDecl : public Decl {
 
 public:
   CodeDecl(std::string name, std::string s) : Decl(CODE, name, {}), code(s) {}
-  void print(std::ostream &os) const;
+  void print(std::ostream &os) const override;
   static bool classof(const Decl *D) { return D->getKind() == CODE; }
 };
 
diff --git a/include/smack/BplFilePrinter.h b/include/smack/BplFilePrinter.h
index eb339c5ae..54bcb177e 100644
--- a/include/smack/BplFilePrinter.h
+++ b/include/smack/BplFilePrinter.h
@@ -17,11 +17,13 @@ class BplFilePrinter : public llvm::ModulePass {
 
   BplFilePrinter(llvm::raw_ostream &out) : llvm::ModulePass(ID), out(out) {}
 
-  virtual bool runOnModule(llvm::Module &m);
+  virtual bool runOnModule(llvm::Module &m) override;
 
-  virtual llvm::StringRef getPassName() const { return "Boogie file printing"; }
+  virtual llvm::StringRef getPassName() const override {
+    return "Boogie file printing";
+  }
 
-  virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const;
+  virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const override;
 };
 } // namespace smack
 
diff --git a/include/smack/BplPrinter.h b/include/smack/BplPrinter.h
index 0c3f39c8e..97f4ae7dd 100644
--- a/include/smack/BplPrinter.h
+++ b/include/smack/BplPrinter.h
@@ -14,8 +14,8 @@ class BplPrinter : public llvm::ModulePass {
   static char ID; // Pass identification, replacement for typeid
 
   BplPrinter() : llvm::ModulePass(ID) {}
-  virtual bool runOnModule(llvm::Module &m);
-  virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const;
+  virtual bool runOnModule(llvm::Module &m) override;
+  virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const override;
 };
 } // namespace smack
 
diff --git a/include/smack/CodifyStaticInits.h b/include/smack/CodifyStaticInits.h
index 4ac92ae5e..e5d9c6cc7 100644
--- a/include/smack/CodifyStaticInits.h
+++ b/include/smack/CodifyStaticInits.h
@@ -17,8 +17,8 @@ class CodifyStaticInits : public llvm::ModulePass {
   static char ID;
 
   CodifyStaticInits() : llvm::ModulePass(ID) {}
-  virtual bool runOnModule(llvm::Module &M);
-  virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const;
+  virtual bool runOnModule(llvm::Module &M) override;
+  virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const override;
 };
 
 llvm::Pass *createCodifyStaticInitsPass();
diff --git a/include/smack/DSAWrapper.h b/include/smack/DSAWrapper.h
index 63f434d86..fa3a392de 100644
--- a/include/smack/DSAWrapper.h
+++ b/include/smack/DSAWrapper.h
@@ -38,8 +38,8 @@ class DSAWrapper : public llvm::ModulePass {
   static char ID;
   DSAWrapper() : ModulePass(ID) {}
 
-  virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const;
-  virtual bool runOnModule(llvm::Module &M);
+  virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const override;
+  virtual bool runOnModule(llvm::Module &M) override;
 
   bool isStaticInitd(const seadsa::Node *n);
   bool isMemOpd(const seadsa::Node *n);
diff --git a/include/smack/ExtractContracts.h b/include/smack/ExtractContracts.h
index bbd385826..47df37203 100644
--- a/include/smack/ExtractContracts.h
+++ b/include/smack/ExtractContracts.h
@@ -13,7 +13,7 @@ class ExtractContracts : public ModulePass {
 public:
   static char ID;
   ExtractContracts() : ModulePass(ID) {}
-  virtual bool runOnModule(Module &M);
-  virtual void getAnalysisUsage(AnalysisUsage &AU) const;
+  virtual bool runOnModule(Module &M) override;
+  virtual void getAnalysisUsage(AnalysisUsage &AU) const override;
 };
 } // namespace smack
diff --git a/include/smack/IntegerOverflowChecker.h b/include/smack/IntegerOverflowChecker.h
index a21f63d34..991d9b33a 100644
--- a/include/smack/IntegerOverflowChecker.h
+++ b/include/smack/IntegerOverflowChecker.h
@@ -15,8 +15,8 @@ class IntegerOverflowChecker : public llvm::ModulePass {
 public:
   static char ID; // Pass identification, replacement for typeid
   IntegerOverflowChecker() : llvm::ModulePass(ID) {}
-  virtual llvm::StringRef getPassName() const;
-  virtual bool runOnModule(llvm::Module &m);
+  virtual llvm::StringRef getPassName() const override;
+  virtual bool runOnModule(llvm::Module &m) override;
 
 private:
   static const std::map<std::string, llvm::Instruction::BinaryOps>
diff --git a/include/smack/MemorySafetyChecker.h b/include/smack/MemorySafetyChecker.h
index e0f042a41..c0bd2b3a8 100644
--- a/include/smack/MemorySafetyChecker.h
+++ b/include/smack/MemorySafetyChecker.h
@@ -25,7 +25,7 @@ class MemorySafetyChecker : public llvm::FunctionPass,
 public:
   static char ID; // Pass identification, replacement for typeid
   MemorySafetyChecker() : llvm::FunctionPass(ID) {}
-  virtual bool runOnFunction(llvm::Function &F);
+  virtual bool runOnFunction(llvm::Function &F) override;
 
   void visitReturnInst(llvm::ReturnInst &I);
   void visitLoadInst(llvm::LoadInst &I);
diff --git a/include/smack/Prelude.h b/include/smack/Prelude.h
index 7c8daf677..9de2d888a 100644
--- a/include/smack/Prelude.h
+++ b/include/smack/Prelude.h
@@ -70,7 +70,7 @@ struct FpOp {
 // builtin functions templated by a function type. A function
 // of such type, when applied, returns an attribute
 template <typename ATTRT> struct BuiltinOp : public Op {
-  typedef const Attr *(*attrT)();
+  typedef const Attr *(*attrT)(...);
   attrT func;
   BuiltinOp(ATTRT func) : Op(Builtin), func((attrT)func) {}
   static bool classof(const Op *op) { return op->getOpType() == Builtin; }
@@ -79,7 +79,7 @@ template <typename ATTRT> struct BuiltinOp : public Op {
 // inlined functions templated by a function type. A function
 // of such type, when applied, returns an expression as the function body
 template <typename EXPRT> struct InlinedOp : public Op {
-  typedef const Expr *(*exprT)();
+  typedef const Expr *(*exprT)(...);
   exprT func;
   InlinedOp(EXPRT func) : Op(Inlined), func((exprT)func) {}
   static bool classof(const Op *op) { return op->getOpType() == Inlined; }
@@ -122,26 +122,26 @@ struct IntOpGen : public TypeGen {
 
   static const std::vector<unsigned> INTEGER_SIZES;
 
-  void generateArithOps(std::stringstream &s) const;
-  void generatePreds(std::stringstream &s) const;
-  void generateMemOps(std::stringstream &s) const;
-  void generateConvOps(std::stringstream &s) const;
-  void generateExtractValueFuncs(std::stringstream &s) const;
+  void generateArithOps(std::stringstream &s) const override;
+  void generatePreds(std::stringstream &s) const override;
+  void generateMemOps(std::stringstream &s) const override;
+  void generateConvOps(std::stringstream &s) const override;
+  void generateExtractValueFuncs(std::stringstream &s) const override;
   void generateBvIntConvs(std::stringstream &s) const;
-  void generate(std::stringstream &s) const;
+  void generate(std::stringstream &s) const override;
 };
 
 // generator class for pointers
 struct PtrOpGen : public TypeGen {
   PtrOpGen(Prelude &prelude) : TypeGen(prelude) {}
 
-  void generateArithOps(std::stringstream &s) const;
-  void generatePreds(std::stringstream &s) const;
-  void generateMemOps(std::stringstream &s) const;
-  void generateConvOps(std::stringstream &s) const;
-  void generateExtractValueFuncs(std::stringstream &s) const;
+  void generateArithOps(std::stringstream &s) const override;
+  void generatePreds(std::stringstream &s) const override;
+  void generateMemOps(std::stringstream &s) const override;
+  void generateConvOps(std::stringstream &s) const override;
+  void generateExtractValueFuncs(std::stringstream &s) const override;
   void generatePtrNumConvs(std::stringstream &s) const;
-  void generate(std::stringstream &s) const;
+  void generate(std::stringstream &s) const override;
 };
 
 // generator class for floats
@@ -155,25 +155,25 @@ struct FpOpGen : public TypeGen {
   static const std::map<unsigned, std::pair<unsigned, unsigned>> FP_LAYOUT;
   static const std::vector<unsigned> FP_BIT_WIDTHS;
 
-  void generateArithOps(std::stringstream &s) const;
-  void generatePreds(std::stringstream &s) const;
-  void generateMemOps(std::stringstream &s) const;
-  void generateConvOps(std::stringstream &s) const;
-  void generateExtractValueFuncs(std::stringstream &s) const;
+  void generateArithOps(std::stringstream &s) const override;
+  void generatePreds(std::stringstream &s) const override;
+  void generateMemOps(std::stringstream &s) const override;
+  void generateConvOps(std::stringstream &s) const override;
+  void generateExtractValueFuncs(std::stringstream &s) const override;
   void generateFpIntConv(std::stringstream &s) const;
-  void generate(std::stringstream &s) const;
+  void generate(std::stringstream &s) const override;
 };
 
 struct TypeDeclGen : public Gen {
   TypeDeclGen(Prelude &prelude) : Gen(prelude) {}
-  void generate(std::stringstream &s) const;
+  void generate(std::stringstream &s) const override;
 };
 
 struct ConstDeclGen : public Gen {
   ConstDeclGen(Prelude &prelude) : Gen(prelude) {}
   void generatePtrConstant(unsigned val, std::stringstream &s) const;
   void generateIntConstant(unsigned val, std::stringstream &s) const;
-  void generate(std::stringstream &s) const;
+  void generate(std::stringstream &s) const override;
 };
 
 struct MemDeclGen : public Gen {
@@ -181,7 +181,7 @@ struct MemDeclGen : public Gen {
   void generateMemoryMaps(std::stringstream &s) const;
   void generateAddrBoundsAndPred(std::stringstream &s) const;
   void generateGlobalAllocations(std::stringstream &s) const;
-  void generate(std::stringstream &s) const;
+  void generate(std::stringstream &s) const override;
 };
 
 class Prelude {
diff --git a/include/smack/Regions.h b/include/smack/Regions.h
index 8e783050e..a0bb5e82b 100644
--- a/include/smack/Regions.h
+++ b/include/smack/Regions.h
@@ -68,8 +68,8 @@ class Regions : public ModulePass, public InstVisitor<Regions> {
 public:
   static char ID;
   Regions() : ModulePass(ID) {}
-  virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const;
-  virtual bool runOnModule(llvm::Module &M);
+  virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const override;
+  virtual bool runOnModule(llvm::Module &M) override;
 
   unsigned size() const;
   unsigned idx(const llvm::Value *v);
diff --git a/include/smack/RemoveDeadDefs.h b/include/smack/RemoveDeadDefs.h
index 708832f10..a9a088de3 100644
--- a/include/smack/RemoveDeadDefs.h
+++ b/include/smack/RemoveDeadDefs.h
@@ -16,6 +16,6 @@ class RemoveDeadDefs : public llvm::ModulePass {
 public:
   static char ID;
   RemoveDeadDefs() : llvm::ModulePass(ID) {}
-  virtual bool runOnModule(llvm::Module &M);
+  virtual bool runOnModule(llvm::Module &M) override;
 };
 } // namespace smack
diff --git a/include/smack/RewriteBitwiseOps.h b/include/smack/RewriteBitwiseOps.h
index da009d209..74006028c 100644
--- a/include/smack/RewriteBitwiseOps.h
+++ b/include/smack/RewriteBitwiseOps.h
@@ -13,8 +13,8 @@ class RewriteBitwiseOps : public llvm::ModulePass {
 public:
   static char ID; // Pass identification, replacement for typeid
   RewriteBitwiseOps() : llvm::ModulePass(ID) {}
-  virtual llvm::StringRef getPassName() const;
-  virtual bool runOnModule(llvm::Module &m);
+  virtual llvm::StringRef getPassName() const override;
+  virtual bool runOnModule(llvm::Module &m) override;
 };
 } // namespace smack
 
diff --git a/include/smack/RustFixes.h b/include/smack/RustFixes.h
index ca3c624fb..28d2e2790 100644
--- a/include/smack/RustFixes.h
+++ b/include/smack/RustFixes.h
@@ -13,8 +13,8 @@ class RustFixes : public llvm::FunctionPass {
 public:
   static char ID; // Pass identification, replacement for typeid
   RustFixes() : llvm::FunctionPass(ID) {}
-  virtual llvm::StringRef getPassName() const;
-  virtual bool runOnFunction(llvm::Function &F);
+  virtual llvm::StringRef getPassName() const override;
+  virtual bool runOnFunction(llvm::Function &F) override;
 };
 } // namespace smack
 
diff --git a/include/smack/SimplifyLibCalls.h b/include/smack/SimplifyLibCalls.h
index 139d3b242..a16514e65 100644
--- a/include/smack/SimplifyLibCalls.h
+++ b/include/smack/SimplifyLibCalls.h
@@ -21,8 +21,8 @@ class SimplifyLibCalls : public FunctionPass,
 public:
   static char ID;
   SimplifyLibCalls() : FunctionPass(ID) {}
-  virtual void getAnalysisUsage(AnalysisUsage &AU) const;
-  virtual bool runOnFunction(Function &F);
+  virtual void getAnalysisUsage(AnalysisUsage &AU) const override;
+  virtual bool runOnFunction(Function &F) override;
   void visitCallInst(CallInst &);
 };
 } // namespace smack
diff --git a/include/smack/SmackModuleGenerator.h b/include/smack/SmackModuleGenerator.h
index dcfb4df07..79fd3684d 100644
--- a/include/smack/SmackModuleGenerator.h
+++ b/include/smack/SmackModuleGenerator.h
@@ -18,8 +18,8 @@ class SmackModuleGenerator : public llvm::ModulePass {
   static char ID; // Pass identification, replacement for typeid
 
   SmackModuleGenerator();
-  virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const;
-  virtual bool runOnModule(llvm::Module &m);
+  virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const override;
+  virtual bool runOnModule(llvm::Module &m) override;
   void generateProgram(llvm::Module &m);
   Program *getProgram() { return program; }
 };
diff --git a/include/smack/SplitAggregateValue.h b/include/smack/SplitAggregateValue.h
index 94991a9b2..062b5c08b 100644
--- a/include/smack/SplitAggregateValue.h
+++ b/include/smack/SplitAggregateValue.h
@@ -20,7 +20,7 @@ class SplitAggregateValue : public llvm::FunctionPass {
   typedef std::pair<IndexT, llvm::Constant *> InfoT;
   static char ID;
   SplitAggregateValue() : llvm::FunctionPass(ID) {}
-  virtual bool runOnFunction(llvm::Function &F);
+  virtual bool runOnFunction(llvm::Function &F) override;
 
 private:
   llvm::Value *splitAggregateLoad(llvm::Type *T, llvm::Value *P,
diff --git a/include/smack/VectorOperations.h b/include/smack/VectorOperations.h
index b277e5f8e..ea6ce07a4 100644
--- a/include/smack/VectorOperations.h
+++ b/include/smack/VectorOperations.h
@@ -23,8 +23,8 @@ class VectorOperations {
 
   FuncDecl *cast(unsigned OpCode, Type *SrcTy, Type *DstTy);
   Decl *inverseAxiom(unsigned OpCode, Type *SrcTy, Type *DstTy);
-  FuncDecl *binary(unsigned OpCode, VectorType *T);
-  FuncDecl *cmp(CmpInst::Predicate P, VectorType *T);
+  FuncDecl *binary(unsigned OpCode, FixedVectorType *T);
+  FuncDecl *cmp(CmpInst::Predicate P, FixedVectorType *T);
 
 public:
   VectorOperations(SmackRep *rep) : rep(rep) {}
diff --git a/include/smack/VerifierCodeMetadata.h b/include/smack/VerifierCodeMetadata.h
index dd91a56fe..9c14fa9b8 100644
--- a/include/smack/VerifierCodeMetadata.h
+++ b/include/smack/VerifierCodeMetadata.h
@@ -20,8 +20,8 @@ class VerifierCodeMetadata : public ModulePass,
 public:
   static char ID;
   VerifierCodeMetadata() : ModulePass(ID) {}
-  virtual bool runOnModule(Module &M);
-  virtual void getAnalysisUsage(AnalysisUsage &AU) const;
+  virtual bool runOnModule(Module &M) override;
+  virtual void getAnalysisUsage(AnalysisUsage &AU) const override;
   void visitCallInst(CallInst &);
   void visitInstruction(Instruction &);
   static bool isMarked(const Instruction &I);
diff --git a/include/utils/Devirt.h b/include/utils/Devirt.h
index 06fc69d53..23e64eea6 100644
--- a/include/utils/Devirt.h
+++ b/include/utils/Devirt.h
@@ -62,9 +62,9 @@ namespace llvm {
       static char ID;
       Devirtualize() : ModulePass(ID) {}
 
-      virtual bool runOnModule(Module & M);
+      virtual bool runOnModule(Module & M) override;
 
-      virtual void getAnalysisUsage(AnalysisUsage &AU) const {
+      virtual void getAnalysisUsage(AnalysisUsage &AU) const override{
         AU.addRequired<seadsa::CompleteCallGraph>();
       }
 
diff --git a/include/utils/MergeGEP.h b/include/utils/MergeGEP.h
index 012346d5c..0f2c3eec1 100644
--- a/include/utils/MergeGEP.h
+++ b/include/utils/MergeGEP.h
@@ -24,7 +24,7 @@ namespace llvm {
   public:
     static char ID;
     MergeArrayGEP() : ModulePass(ID) {}
-    virtual bool runOnModule(Module& M);
+    virtual bool runOnModule(Module& M) override;
   };
 }
 
diff --git a/include/utils/SimplifyExtractValue.h b/include/utils/SimplifyExtractValue.h
index ca211daa7..60f3103db 100644
--- a/include/utils/SimplifyExtractValue.h
+++ b/include/utils/SimplifyExtractValue.h
@@ -25,7 +25,7 @@ namespace llvm {
   public:
     static char ID;
     SimplifyEV() : ModulePass(ID) {}
-    virtual bool runOnModule(Module& M);
+    virtual bool runOnModule(Module& M) override;
   };
 }
 
diff --git a/include/utils/SimplifyInsertValue.h b/include/utils/SimplifyInsertValue.h
index 210a2dc68..0e60bce46 100644
--- a/include/utils/SimplifyInsertValue.h
+++ b/include/utils/SimplifyInsertValue.h
@@ -24,7 +24,7 @@ namespace llvm {
   public:
     static char ID;
     SimplifyIV() : ModulePass(ID) {}
-    virtual bool runOnModule(Module& M);
+    virtual bool runOnModule(Module& M) override;
   };
 }
 
diff --git a/lib/smack/AddTiming.cpp b/lib/smack/AddTiming.cpp
index b165e7634..e678a398c 100644
--- a/lib/smack/AddTiming.cpp
+++ b/lib/smack/AddTiming.cpp
@@ -213,7 +213,8 @@ unsigned AddTiming::getInstructionCost(const Instruction *I) const {
   case Instruction::BitCast:
   case Instruction::AddrSpaceCast: {
     Type *SrcTy = I->getOperand(0)->getType();
-    return TTI->getCastInstrCost(I->getOpcode(), I->getType(), SrcTy);
+    return TTI->getCastInstrCost(I->getOpcode(), I->getType(), SrcTy,
+                                 TTI->getCastContextHint(I));
   }
   case Instruction::ExtractElement: {
     return NO_TIMING_INFO;
diff --git a/lib/smack/RewriteBitwiseOps.cpp b/lib/smack/RewriteBitwiseOps.cpp
index 5c25d2922..3487c0f14 100644
--- a/lib/smack/RewriteBitwiseOps.cpp
+++ b/lib/smack/RewriteBitwiseOps.cpp
@@ -66,7 +66,8 @@ bool RewriteBitwiseOps::runOnModule(Module &m) {
             // Shifting left by a constant amount is equivalent to dividing by
             // 2^amount
             op = Instruction::Mul;
-          }
+          } else
+            llvm_unreachable("Unexpected shift operation!");
 
           auto lhs = bi->getOperand(0);
           unsigned bitWidth = getOpBitWidth(lhs);
diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp
index 28b7887ec..86a7a498a 100644
--- a/lib/smack/SmackInstGenerator.cpp
+++ b/lib/smack/SmackInstGenerator.cpp
@@ -348,7 +348,7 @@ void SmackInstGenerator::visitBinaryOperator(llvm::BinaryOperator &I) {
         {&SmackOptions::FloatEnabled}, currBlock, &I);
 
   const Expr *E;
-  if (isa<VectorType>(I.getType())) {
+  if (isa<FixedVectorType>(I.getType())) {
     auto X = I.getOperand(0);
     auto Y = I.getOperand(1);
     auto D = VectorOperations(rep).binary(&I);
@@ -364,8 +364,8 @@ void SmackInstGenerator::visitBinaryOperator(llvm::BinaryOperator &I) {
 /******************************************************************************/
 
 void SmackInstGenerator::visitUnaryOperator(llvm::UnaryOperator &I) {
-  assert(I.getOpcode() == Instruction::FNeg && !isa<VectorType>(I.getType()) &&
-         "Unsupported unary operation!");
+  assert(I.getOpcode() == Instruction::FNeg &&
+         !isa<FixedVectorType>(I.getType()) && "Unsupported unary operation!");
   processInstruction(I);
   SmackWarnings::warnOverApproximate(
       std::string("floating-point operation ") + I.getOpcodeName(),
@@ -485,7 +485,7 @@ void SmackInstGenerator::visitLoadInst(llvm::LoadInst &li) {
   // assert (!li.getType()->isAggregateType() && "Unexpected load value.");
 
   const Expr *E;
-  if (isa<VectorType>(T->getElementType())) {
+  if (isa<FixedVectorType>(T->getElementType())) {
     auto D = VectorOperations(rep).load(P);
     E = Expr::fn(D->getName(), {Expr::id(rep->memPath(P)), rep->expr(P)});
   } else {
@@ -509,7 +509,7 @@ void SmackInstGenerator::visitStoreInst(llvm::StoreInst &si) {
   const llvm::Value *V = si.getValueOperand()->stripPointerCastsAndAliases();
   assert(!V->getType()->isAggregateType() && "Unexpected store value.");
 
-  if (isa<VectorType>(V->getType())) {
+  if (isa<FixedVectorType>(V->getType())) {
     auto D = VectorOperations(rep).store(P);
     auto M = Expr::id(rep->memPath(P));
     auto E = Expr::fn(D->getName(), {M, rep->expr(P), rep->expr(V)});
@@ -583,7 +583,7 @@ void SmackInstGenerator::visitGetElementPtrInst(llvm::GetElementPtrInst &I) {
 void SmackInstGenerator::visitCastInst(llvm::CastInst &I) {
   processInstruction(I);
   const Expr *E;
-  if (isa<VectorType>(I.getType())) {
+  if (isa<FixedVectorType>(I.getType())) {
     auto X = I.getOperand(0);
     auto D = VectorOperations(rep).cast(&I);
     E = Expr::fn(D->getName(), rep->expr(X));
@@ -607,7 +607,7 @@ void SmackInstGenerator::visitCastInst(llvm::CastInst &I) {
 void SmackInstGenerator::visitCmpInst(llvm::CmpInst &I) {
   processInstruction(I);
   const Expr *E;
-  if (isa<VectorType>(I.getType())) {
+  if (isa<FixedVectorType>(I.getType())) {
     auto X = I.getOperand(0);
     auto Y = I.getOperand(1);
     auto D = VectorOperations(rep).cmp(&I);
diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp
index 4ab04a129..357a5dc36 100644
--- a/lib/smack/SmackRep.cpp
+++ b/lib/smack/SmackRep.cpp
@@ -236,7 +236,7 @@ std::string SmackRep::type(const llvm::Type *t) {
   else if (t->isPointerTy())
     return Naming::PTR_TYPE;
 
-  else if (auto VT = dyn_cast<VectorType>(t))
+  else if (auto VT = dyn_cast<FixedVectorType>(t))
     return vectorType(VT->getNumElements(), VT->getElementType());
 
   else
diff --git a/lib/smack/VectorOperations.cpp b/lib/smack/VectorOperations.cpp
index 96d090aad..c9ee78e5b 100644
--- a/lib/smack/VectorOperations.cpp
+++ b/lib/smack/VectorOperations.cpp
@@ -27,7 +27,7 @@ std::string VectorOperations::selector(Type *T, unsigned idx) {
 }
 
 std::list<Decl *> VectorOperations::type(Type *T) {
-  auto VT = dyn_cast<VectorType>(T);
+  auto VT = dyn_cast<FixedVectorType>(T);
   assert(VT && "expected vector type");
   std::list<Decl *> decls;
 
@@ -61,8 +61,8 @@ const Expr *VectorOperations::constant(const ConstantAggregateZero *C) {
 }
 
 FuncDecl *VectorOperations::cast(unsigned OpCode, Type *SrcTy, Type *DstTy) {
-  auto SrcVecTy = dyn_cast<VectorType>(SrcTy);
-  auto DstVecTy = dyn_cast<VectorType>(DstTy);
+  auto SrcVecTy = dyn_cast<FixedVectorType>(SrcTy);
+  auto DstVecTy = dyn_cast<FixedVectorType>(DstTy);
   assert((SrcVecTy || DstVecTy) && "Expected a vector type");
 
   auto FnName =
@@ -91,7 +91,7 @@ Decl *VectorOperations::inverseAxiom(unsigned OpCode, Type *SrcTy,
       Fn + "inverse");
 }
 
-FuncDecl *VectorOperations::binary(unsigned OpCode, VectorType *T) {
+FuncDecl *VectorOperations::binary(unsigned OpCode, FixedVectorType *T) {
   auto FnName = rep->opName(Naming::INSTRUCTION_TABLE.at(OpCode), {T});
   auto FnBase =
       rep->opName(Naming::INSTRUCTION_TABLE.at(OpCode), {T->getElementType()});
@@ -105,7 +105,7 @@ FuncDecl *VectorOperations::binary(unsigned OpCode, VectorType *T) {
                         rep->type(T), Expr::fn(constructor(T), Args));
 }
 
-FuncDecl *VectorOperations::cmp(CmpInst::Predicate P, VectorType *T) {
+FuncDecl *VectorOperations::cmp(CmpInst::Predicate P, FixedVectorType *T) {
   auto FnName = rep->opName(Naming::CMPINST_TABLE.at(P), {T});
   auto FnBase = rep->opName(Naming::CMPINST_TABLE.at(P), {T->getElementType()});
   std::list<const Expr *> Args;
@@ -116,8 +116,8 @@ FuncDecl *VectorOperations::cmp(CmpInst::Predicate P, VectorType *T) {
   }
   return Decl::function(
       FnName, {{"v1", rep->type(T)}, {"v2", rep->type(T)}},
-      rep->type(VectorType::get(IntegerType::get(T->getContext(), 1),
-                                T->getNumElements())),
+      rep->type(FixedVectorType::get(IntegerType::get(T->getContext(), 1),
+                                     T->getNumElements())),
       Expr::fn(constructor(T), Args));
 }
 
@@ -127,9 +127,9 @@ FuncDecl *VectorOperations::cast(CastInst *I) {
   auto G = cast(I->getOpcode(), I->getDestTy(), I->getSrcTy());
   auto A = inverseAxiom(I->getOpcode(), I->getSrcTy(), I->getDestTy());
   auto B = inverseAxiom(I->getOpcode(), I->getDestTy(), I->getSrcTy());
-  if (isa<VectorType>(I->getSrcTy()))
+  if (isa<FixedVectorType>(I->getSrcTy()))
     type(I->getSrcTy());
-  if (isa<VectorType>(I->getDestTy()))
+  if (isa<FixedVectorType>(I->getDestTy()))
     type(I->getDestTy());
   rep->addAuxiliaryDeclaration(F);
   rep->addAuxiliaryDeclaration(G);
@@ -140,7 +140,7 @@ FuncDecl *VectorOperations::cast(CastInst *I) {
 
 FuncDecl *VectorOperations::binary(BinaryOperator *I) {
   SDEBUG(errs() << "simd-binary: " << *I << "\n");
-  auto T = dyn_cast<VectorType>(I->getType());
+  auto T = dyn_cast<FixedVectorType>(I->getType());
   assert(T && T == I->getOperand(0)->getType() &&
          "expected equal vector types");
   auto F = binary(I->getOpcode(), T);
@@ -151,20 +151,20 @@ FuncDecl *VectorOperations::binary(BinaryOperator *I) {
 
 FuncDecl *VectorOperations::cmp(CmpInst *I) {
   SDEBUG(errs() << "simd-binary: " << *I << "\n");
-  auto T = dyn_cast<VectorType>(I->getOperand(0)->getType());
+  auto T = dyn_cast<FixedVectorType>(I->getOperand(0)->getType());
   assert(T && "expected vector type");
   auto F = cmp(I->getPredicate(), T);
   type(T);
-  type(VectorType::get(IntegerType::get(T->getContext(), 1),
-                       T->getNumElements()));
+  type(FixedVectorType::get(IntegerType::get(T->getContext(), 1),
+                            T->getNumElements()));
   rep->addAuxiliaryDeclaration(F);
   return F;
 }
 
 FuncDecl *VectorOperations::shuffle(Type *T, Type *U, std::vector<int> mask) {
-  auto VT = dyn_cast<VectorType>(T);
+  auto VT = dyn_cast<FixedVectorType>(T);
   assert(VT && "expected vector type");
-  assert(isa<VectorType>(U) && "expected vector type");
+  assert(isa<FixedVectorType>(U) && "expected vector type");
   type(T);
   type(U);
 
@@ -195,7 +195,7 @@ FuncDecl *VectorOperations::shuffle(Type *T, Type *U, std::vector<int> mask) {
 }
 
 FuncDecl *VectorOperations::insert(Type *T, Type *IT) {
-  auto VT = dyn_cast<VectorType>(T);
+  auto VT = dyn_cast<FixedVectorType>(T);
   assert(VT && "expected vector type");
   type(T);
 
@@ -236,7 +236,7 @@ FuncDecl *VectorOperations::insert(Type *T, Type *IT) {
 }
 
 FuncDecl *VectorOperations::extract(Type *T, Type *IT) {
-  auto VT = dyn_cast<VectorType>(T);
+  auto VT = dyn_cast<FixedVectorType>(T);
   assert(VT && "expected vector type");
   type(T);
 
diff --git a/lib/utils/Devirt.cpp b/lib/utils/Devirt.cpp
index 90b3e407e..359f0794d 100644
--- a/lib/utils/Devirt.cpp
+++ b/lib/utils/Devirt.cpp
@@ -79,16 +79,8 @@ castTo (Value * V, Type * Ty, std::string Name, Value * InsertPt) {
 }
 
 static inline bool isZExtOrBitCastable(Value* V, Type* T) {
-  if (!CastInst::isCastable(V->getType(), T))
-    return false;
-
-  switch(CastInst::getCastOpcode(V, false, T, false)) {
-    case Instruction::ZExt:
-    case Instruction::BitCast:
-      return true;
-    default:
-      return false;
-  }
+  return CastInst::castIsValid(Instruction::ZExt, V->getType(), T) ||
+         CastInst::castIsValid(Instruction::BitCast, V->getType(), T);
 }
 
 static inline bool match(CallBase *CS, const Function &F) {
diff --git a/sea-dsa b/sea-dsa
index e967981b4..934b99861 160000
--- a/sea-dsa
+++ b/sea-dsa
@@ -1 +1 @@
-Subproject commit e967981b4600afeb5f0bc557fb1301ffa90da689
+Subproject commit 934b99861602df3e5a29b0f86819a03e2da676d0
diff --git a/share/smack/errtrace.py b/share/smack/errtrace.py
index f4ef9ad67..c4a1e1a21 100644
--- a/share/smack/errtrace.py
+++ b/share/smack/errtrace.py
@@ -1,9 +1,6 @@
 import re
 import functools
-import shutil
-import subprocess
 import json
-from .frontend import llvm_exact_bin
 
 
 def reformat_assignment(line):
@@ -39,36 +36,14 @@ def repl(m):
         line.strip())
 
 
-def demangle(func):
-    '''Demangle C++/Rust function names'''
-
-    def demangle_with(func, tool):
-        if shutil.which(tool):
-            p = subprocess.Popen(
-                tool,
-                stdin=subprocess.PIPE,
-                stdout=subprocess.PIPE,
-                stderr=subprocess.PIPE)
-            out, _ = p.communicate(input=func.encode())
-            return out.decode().strip()
-        return func
-    return functools.reduce(demangle_with,
-                            [llvm_exact_bin('llvm-cxxfilt'), 'rustfilt'],
-                            func)
-
-
 def transform(info):
     '''Transform an error trace line'''
 
-    if info.startswith('CALL') or info.startswith('RETURN from'):
-        tokens = info.split()
-        tokens[-1] = demangle(tokens[-1])
-        return ' '.join(tokens)
-    elif '=' in info:
+    if '=' in info:
         tokens = info.split('=')
         lhs = tokens[0].strip()
         rhs = tokens[1].strip()
-        return demangle(lhs) + ' = ' + reformat_assignment(rhs)
+        return lhs + ' = ' + reformat_assignment(rhs)
     else:
         return info
 
@@ -88,11 +63,11 @@ def error_trace(verifier_output, verifier):
     return output
 
 
-def json_output_str(result, output, verifier):
-    return json.dumps(json_output(result, output, verifier))
+def json_output_str(result, output, verifier, prettify=True):
+    return json.dumps(json_output(result, output, verifier, prettify))
 
 
-def json_output(result, output, verifier):
+def json_output(result, output, verifier, prettify=True):
     '''Convert error traces into JSON format'''
 
     from .top import VResult
@@ -185,6 +160,7 @@ def merger(traces, trace):
             'passed?': False,
             'failsAt': failsAt,
             'threadCount': 1,
-            'traces': functools.reduce(merger, traces, [])
+            'traces': (functools.reduce(merger, traces, []) if prettify
+                       else traces)
     }
     return json_data
diff --git a/share/smack/svcomp/utils.py b/share/smack/svcomp/utils.py
index cf2851747..188a4ae43 100644
--- a/share/smack/svcomp/utils.py
+++ b/share/smack/svcomp/utils.py
@@ -168,7 +168,7 @@ def write_error_file(args, status, verifier_output):
   if args.error_file:
     error = None
     if args.language == 'svcomp':
-      error = smackJsonToXmlGraph(json_output_str(status, verifier_output), args, hasBug, status)
+      error = smackJsonToXmlGraph(json_output_str(status, verifier_output, 'corral', False), args, hasBug, status)
     elif hasBug:
       error = smack.top.error_trace(verifier_output, 'corral')
     if error is not None:
diff --git a/test/c/failing/floppy_false.i.cil.c b/test/c/failing/floppy_false.i.cil.c
index 4638eda45..705e74efd 100644
--- a/test/c/failing/floppy_false.i.cil.c
+++ b/test/c/failing/floppy_false.i.cil.c
@@ -2291,7 +2291,8 @@ NTSTATUS FloppyAddDevice(PDRIVER_OBJECT DriverObject,
           disketteExtension->TargetObject =
               IoAttachDeviceToDeviceStack(deviceObject, PhysicalDeviceObject);
         }
-        {} {
+        {}
+        {
           /*       KeInitializeSemaphore(& disketteExtension->RequestSemaphore,
            * 0L, 2147483647); */ /* INLINED */
           disketteExtension->PowerDownMutex.Count = 1;
@@ -2614,9 +2615,11 @@ NTSTATUS FlQueueIrpToThread(PIRP Irp, PDISKETTE_EXTENSION DisketteExtension) {
     } else {
     }
     {
-        /*   ExReleaseFastMutex(& DisketteExtension->PowerDownMutex); */ /* INLINED
-                                                                          */
-    } {} {
+      /*   ExReleaseFastMutex(& DisketteExtension->PowerDownMutex); */ /* INLINED
+                                                                        */
+    }
+    {}
+    {
       /*   ExAcquireFastMutex(& DisketteExtension->ThreadReferenceMutex); */ /* INLINED */
       DisketteExtension->ThreadReferenceCount += 1L;
     }
@@ -2847,9 +2850,9 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                                     disketteExtension->DeviceName.Length;
                                 if (irpSp->Parameters.DeviceIoControl
                                         .OutputBufferLength <
-                                    (ULONG)(
-                                        sizeof(USHORT) +
-                                        (unsigned int)mountName->NameLength)) {
+                                    (ULONG)(sizeof(USHORT) +
+                                            (unsigned int)
+                                                mountName->NameLength)) {
                                   ntStatus = -2147483643L;
                                   Irp->IoStatus.Information =
                                       sizeof(MOUNTDEV_NAME);
@@ -3004,13 +3007,12 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                                 }
                                 ntStatus = 0L;
                                 if (outputBufferLength <
-                                    (ULONG)(
-                                        sizeof(DISK_GEOMETRY) *
-                                        (unsigned int)(((int)
-                                                            highestDriveMediaType -
-                                                        (int)
-                                                            lowestDriveMediaType) +
-                                                       1))) {
+                                    (ULONG)(sizeof(DISK_GEOMETRY) *
+                                            (unsigned int)(((int)
+                                                                highestDriveMediaType -
+                                                            (int)
+                                                                lowestDriveMediaType) +
+                                                           1))) {
                                   {}
                                   ntStatus = -2147483643L;
                                   highestDriveMediaType =
@@ -3219,7 +3221,8 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                                     goto switch_16_break;
                                   } else {
                                   }
-                                  {} {
+                                  {}
+                                  {
                                     ntStatus = FlQueueIrpToThread(
                                         Irp, disketteExtension);
                                   }
@@ -4169,7 +4172,9 @@ void FlFinishOperation(PIRP Irp, PDISKETTE_EXTENSION DisketteExtension) {
     _L___0 : /* CIL Label */
     {}
     }
-    {} {} { IofCompleteRequest(Irp, 1); }
+    {}
+    {}
+    { IofCompleteRequest(Irp, 1); }
     return;
   }
 }
@@ -4687,8 +4692,9 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) {
                         _L : /* CIL Label */
                         {}
                           DisketteExtension->DriveMediaType =
-                              (DRIVE_MEDIA_TYPE)(
-                                  (int)DisketteExtension->DriveMediaType - 1);
+                              (DRIVE_MEDIA_TYPE)((int)DisketteExtension
+                                                     ->DriveMediaType -
+                                                 1);
                           DisketteExtension->DriveMediaConstants =
                               *(DriveMediaConstants +
                                 DisketteExtension->DriveMediaType);
@@ -4769,7 +4775,8 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) {
                                 .__annonCompField16.CurrentStackLocation -= 1;
                             ntStatus = FlReadWrite(DisketteExtension, irp, 1);
                           }
-                          {} {
+                          {}
+                          {
                             /*                     MmUnlockPages(irp->MdlAddress);
                              */ /* INLINED */
                             /*                     IoFreeMdl(irp->MdlAddress);
@@ -4781,8 +4788,9 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) {
                           if (!(ntStatus >= 0L)) {
                             {}
                             DisketteExtension->DriveMediaType =
-                                (DRIVE_MEDIA_TYPE)(
-                                    (int)DisketteExtension->DriveMediaType - 1);
+                                (DRIVE_MEDIA_TYPE)((int)DisketteExtension
+                                                       ->DriveMediaType -
+                                                   1);
                             DisketteExtension->DriveMediaConstants =
                                 *(DriveMediaConstants +
                                   DisketteExtension->DriveMediaType);
@@ -5051,11 +5059,10 @@ void FloppyThread(PVOID Context) {
               }
             } else {
             }
-            {
-                /*         ExReleaseFastMutex(PagingMutex); */ /* INLINED */
-            } {} {
-              PsTerminateSystemThread(0L);
+            { /*         ExReleaseFastMutex(PagingMutex); */ /* INLINED */
             }
+            {}
+            { PsTerminateSystemThread(0L); }
           } else {
           }
           {
@@ -5110,8 +5117,10 @@ void FloppyThread(PVOID Context) {
             } else {
             }
             {
-                /*       ExReleaseFastMutex(& disketteExtension->PowerDownMutex); */ /* INLINED */
-            } {}
+              /*       ExReleaseFastMutex(& disketteExtension->PowerDownMutex);
+               */ /* INLINED */
+            }
+            {}
             irpSp = irp->Tail.Overlay.__annonCompField17.__annonCompField16
                         .CurrentStackLocation;
             {}
@@ -5657,7 +5666,8 @@ void FlConsolidateMediaTypeWithBootSector(PDISKETTE_EXTENSION DisketteExtension,
       }
     } else {
     }
-    {} {}
+    {}
+    {}
     if ((int)bpbMediaType == (int)DisketteExtension->MediaType) {
       changeToBpbMedia = 0;
       {}
diff --git a/test/c/failing/floppy_true.i.cil.c b/test/c/failing/floppy_true.i.cil.c
index ab4a35db4..15c4a7c77 100644
--- a/test/c/failing/floppy_true.i.cil.c
+++ b/test/c/failing/floppy_true.i.cil.c
@@ -2291,7 +2291,8 @@ NTSTATUS FloppyAddDevice(PDRIVER_OBJECT DriverObject,
           disketteExtension->TargetObject =
               IoAttachDeviceToDeviceStack(deviceObject, PhysicalDeviceObject);
         }
-        {} {
+        {}
+        {
           /*       KeInitializeSemaphore(& disketteExtension->RequestSemaphore,
            * 0L, 2147483647); */ /* INLINED */
           disketteExtension->PowerDownMutex.Count = 1;
@@ -2614,9 +2615,11 @@ NTSTATUS FlQueueIrpToThread(PIRP Irp, PDISKETTE_EXTENSION DisketteExtension) {
     } else {
     }
     {
-        /*   ExReleaseFastMutex(& DisketteExtension->PowerDownMutex); */ /* INLINED
-                                                                          */
-    } {} {
+      /*   ExReleaseFastMutex(& DisketteExtension->PowerDownMutex); */ /* INLINED
+                                                                        */
+    }
+    {}
+    {
       /*   ExAcquireFastMutex(& DisketteExtension->ThreadReferenceMutex); */ /* INLINED */
       DisketteExtension->ThreadReferenceCount += 1L;
     }
@@ -2847,9 +2850,9 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                                     disketteExtension->DeviceName.Length;
                                 if (irpSp->Parameters.DeviceIoControl
                                         .OutputBufferLength <
-                                    (ULONG)(
-                                        sizeof(USHORT) +
-                                        (unsigned int)mountName->NameLength)) {
+                                    (ULONG)(sizeof(USHORT) +
+                                            (unsigned int)
+                                                mountName->NameLength)) {
                                   ntStatus = -2147483643L;
                                   Irp->IoStatus.Information =
                                       sizeof(MOUNTDEV_NAME);
@@ -3004,13 +3007,12 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                                 }
                                 ntStatus = 0L;
                                 if (outputBufferLength <
-                                    (ULONG)(
-                                        sizeof(DISK_GEOMETRY) *
-                                        (unsigned int)(((int)
-                                                            highestDriveMediaType -
-                                                        (int)
-                                                            lowestDriveMediaType) +
-                                                       1))) {
+                                    (ULONG)(sizeof(DISK_GEOMETRY) *
+                                            (unsigned int)(((int)
+                                                                highestDriveMediaType -
+                                                            (int)
+                                                                lowestDriveMediaType) +
+                                                           1))) {
                                   {}
                                   ntStatus = -2147483643L;
                                   highestDriveMediaType =
@@ -3219,7 +3221,8 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                                     goto switch_16_break;
                                   } else {
                                   }
-                                  {} {
+                                  {}
+                                  {
                                     ntStatus = FlQueueIrpToThread(
                                         Irp, disketteExtension);
                                   }
@@ -4169,7 +4172,9 @@ void FlFinishOperation(PIRP Irp, PDISKETTE_EXTENSION DisketteExtension) {
     _L___0 : /* CIL Label */
     {}
     }
-    {} {} { IofCompleteRequest(Irp, 1); }
+    {}
+    {}
+    { IofCompleteRequest(Irp, 1); }
     return;
   }
 }
@@ -4687,8 +4692,9 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) {
                         _L : /* CIL Label */
                         {}
                           DisketteExtension->DriveMediaType =
-                              (DRIVE_MEDIA_TYPE)(
-                                  (int)DisketteExtension->DriveMediaType - 1);
+                              (DRIVE_MEDIA_TYPE)((int)DisketteExtension
+                                                     ->DriveMediaType -
+                                                 1);
                           DisketteExtension->DriveMediaConstants =
                               *(DriveMediaConstants +
                                 DisketteExtension->DriveMediaType);
@@ -4769,7 +4775,8 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) {
                                 .__annonCompField16.CurrentStackLocation -= 1;
                             ntStatus = FlReadWrite(DisketteExtension, irp, 1);
                           }
-                          {} {
+                          {}
+                          {
                             /*                     MmUnlockPages(irp->MdlAddress);
                              */ /* INLINED */
                             /*                     IoFreeMdl(irp->MdlAddress);
@@ -4781,8 +4788,9 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) {
                           if (!(ntStatus >= 0L)) {
                             {}
                             DisketteExtension->DriveMediaType =
-                                (DRIVE_MEDIA_TYPE)(
-                                    (int)DisketteExtension->DriveMediaType - 1);
+                                (DRIVE_MEDIA_TYPE)((int)DisketteExtension
+                                                       ->DriveMediaType -
+                                                   1);
                             DisketteExtension->DriveMediaConstants =
                                 *(DriveMediaConstants +
                                   DisketteExtension->DriveMediaType);
@@ -5051,11 +5059,10 @@ void FloppyThread(PVOID Context) {
               }
             } else {
             }
-            {
-                /*         ExReleaseFastMutex(PagingMutex); */ /* INLINED */
-            } {} {
-              PsTerminateSystemThread(0L);
+            { /*         ExReleaseFastMutex(PagingMutex); */ /* INLINED */
             }
+            {}
+            { PsTerminateSystemThread(0L); }
           } else {
           }
           {
@@ -5110,8 +5117,10 @@ void FloppyThread(PVOID Context) {
             } else {
             }
             {
-                /*       ExReleaseFastMutex(& disketteExtension->PowerDownMutex); */ /* INLINED */
-            } {}
+              /*       ExReleaseFastMutex(& disketteExtension->PowerDownMutex);
+               */ /* INLINED */
+            }
+            {}
             irpSp = irp->Tail.Overlay.__annonCompField17.__annonCompField16
                         .CurrentStackLocation;
             {}
@@ -5657,7 +5666,8 @@ void FlConsolidateMediaTypeWithBootSector(PDISKETTE_EXTENSION DisketteExtension,
       }
     } else {
     }
-    {} {}
+    {}
+    {}
     if ((int)bpbMediaType == (int)DisketteExtension->MediaType) {
       changeToBpbMedia = 0;
       {}
diff --git a/test/c/ntdrivers/kbfiltr_false.i.cil.c b/test/c/ntdrivers/kbfiltr_false.i.cil.c
index 8f5dce352..a82976feb 100644
--- a/test/c/ntdrivers/kbfiltr_false.i.cil.c
+++ b/test/c/ntdrivers/kbfiltr_false.i.cil.c
@@ -2136,10 +2136,10 @@ NTSTATUS KbFilter_PnP(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                                                     { errorFn(); }
                                                   }
                                                   {
-                                                    Irp->CurrentLocation = (CHAR)(
-                                                        (int)Irp
-                                                            ->CurrentLocation +
-                                                        1);
+                                                    Irp->CurrentLocation =
+                                                        (CHAR)((int)Irp
+                                                                   ->CurrentLocation +
+                                                               1);
                                                     Irp->Tail.Overlay
                                                         .__annonCompField17
                                                         .__annonCompField16
@@ -2158,10 +2158,10 @@ NTSTATUS KbFilter_PnP(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                                                     { errorFn(); }
                                                   }
                                                   {
-                                                    Irp->CurrentLocation = (CHAR)(
-                                                        (int)Irp
-                                                            ->CurrentLocation +
-                                                        1);
+                                                    Irp->CurrentLocation =
+                                                        (CHAR)((int)Irp
+                                                                   ->CurrentLocation +
+                                                               1);
                                                     Irp->Tail.Overlay
                                                         .__annonCompField17
                                                         .__annonCompField16
@@ -2203,10 +2203,10 @@ NTSTATUS KbFilter_PnP(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                                                     { errorFn(); }
                                                   }
                                                   {
-                                                    Irp->CurrentLocation = (CHAR)(
-                                                        (int)Irp
-                                                            ->CurrentLocation +
-                                                        1);
+                                                    Irp->CurrentLocation =
+                                                        (CHAR)((int)Irp
+                                                                   ->CurrentLocation +
+                                                               1);
                                                     Irp->Tail.Overlay
                                                         .__annonCompField17
                                                         .__annonCompField16
diff --git a/test/c/ntdrivers/parport_false.i.cil.c b/test/c/ntdrivers/parport_false.i.cil.c
index 619b84168..2e063859f 100644
--- a/test/c/ntdrivers/parport_false.i.cil.c
+++ b/test/c/ntdrivers/parport_false.i.cil.c
@@ -2523,7 +2523,8 @@ void PptDebugDumpResourceRequirementsList(
         } else {
           goto while_12_break;
         }
-        {} {
+        {}
+        {
           PptDebugDumpResourceList(curList);
           curList = (struct _IO_RESOURCE_LIST *)(curList->Descriptors +
                                                  curList->Count);
@@ -2932,9 +2933,10 @@ PptRemovePptRemovalRelation(PDEVICE_EXTENSION Extension,
       }
     }
     {
-        /*   ExAcquireFastMutex(& Extension->ExtensionFastMutex); */ /* INLINED
-                                                                      */
-    } {
+      /*   ExAcquireFastMutex(& Extension->ExtensionFastMutex); */ /* INLINED
+                                                                    */
+    }
+    {
       while (1) {
       while_27_continue: /* CIL Label */;
         if (!done) {
@@ -3818,7 +3820,8 @@ BOOLEAN PptIsNecR98Machine(void) {
       }
       return (0);
     }
-    {} { /*   ExFreePool(identifierString.Buffer); */ /* INLINED */
+    {}
+    { /*   ExFreePool(identifierString.Buffer); */ /* INLINED */
     }
     return (0);
   }
@@ -3875,7 +3878,8 @@ NTSTATUS PptDispatchCreate(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
       InterlockedIncrement(&extension->OpenCloseRefCount);
       /*   ExReleaseFastMutex(& extension->OpenCloseMutex); */ /* INLINED */
     }
-    {} {
+    {}
+    {
       PptReleaseRemoveLock(&extension->RemoveLock, Irp);
       Irp->IoStatus.__annonCompField4.Status = status;
       myStatus = status;
@@ -3922,9 +3926,10 @@ NTSTATUS PptDispatchClose(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
       } else {
       }
       {
-          /*     ExReleaseFastMutex(& extension->OpenCloseMutex); */ /* INLINED
-                                                                      */
-      } {}
+        /*     ExReleaseFastMutex(& extension->OpenCloseMutex); */ /* INLINED
+                                                                    */
+      }
+      {}
     } else {
       {
           /*     ExReleaseFastMutex(& extension->OpenCloseMutex); */ /* INLINED
@@ -4925,7 +4930,8 @@ NTSTATUS PptDetectPortType(PDEVICE_EXTENSION Extension) {
       Status = RtlQueryRegistryValues(1, ParportPath.Buffer, RegTable,
                                       (void *)0, (void *)0);
     }
-    {} {}
+    {}
+    {}
     if (Status >= 0L) {
       if (IdentifierHex == 0UL) {
 
@@ -4953,7 +4959,8 @@ NTSTATUS PptDetectPortType(PDEVICE_EXTENSION Extension) {
     } else {
       Status = 3221225473UL;
     }
-    {} { Status = PptDetectPortCapabilities(Extension); }
+    {}
+    { Status = PptDetectPortCapabilities(Extension); }
     {}
     Status = 0L;
     {}
@@ -4989,7 +4996,8 @@ NTSTATUS PptDetectPortCapabilities(PDEVICE_EXTENSION Extension) {
     {}
       Extension->CheckedForGenericEpp = 1;
     }
-    {} { PptDetectBytePort(Extension); }
+    {}
+    { PptDetectBytePort(Extension); }
     if (Extension->PnpInfo.HardwareCapabilities & 11UL) {
       {}
       return (0L);
@@ -5021,7 +5029,8 @@ void PptDetectEcpPort(PDEVICE_EXTENSION Extension) {
       ecr = READ_PORT_UCHAR(wPortECR);
       ecrLast = ecr;
     }
-    {} {
+    {}
+    {
       dcr = (unsigned char)14;
       WRITE_PORT_UCHAR(wPortDCR, dcr);
       ecr = READ_PORT_UCHAR(wPortECR);
@@ -5165,7 +5174,8 @@ void PptDetectEppPort(PDEVICE_EXTENSION Extension) {
       dcr = READ_PORT_UCHAR(Controller + 2);
       Extension->PnpInfo.HardwareCapabilities |= 2UL;
     }
-    {} {
+    {}
+    {
       PptEcrSetMode(Extension, 148);
       WRITE_PORT_UCHAR(Controller + 2, Reverse);
       KeStallExecutionProcessor(5);
@@ -5989,7 +5999,8 @@ PDEVICE_RELATIONS PptPnpBuildRemovalRelations(PDEVICE_EXTENSION Extension) {
       }
     while_185_break: /* CIL Label */;
     }
-    {} {
+    {}
+    {
       tmp = ExAllocatePoolWithTag(1,
                                   (ULONG)sizeof(DEVICE_RELATIONS) +
                                       (count - 1UL) *
@@ -6848,7 +6859,9 @@ NTSTATUS PptPnpFilterResourceRequirements(PDEVICE_OBJECT DeviceObject,
       pResourceRequirementsIn =
           (struct _IO_RESOURCE_REQUIREMENTS_LIST *)Irp->IoStatus.Information;
     }
-    {} {} { PptDebugDumpResourceRequirementsList(pResourceRequirementsIn); }
+    {}
+    {}
+    { PptDebugDumpResourceRequirementsList(pResourceRequirementsIn); }
     if (filterResourceMethod == 1) {
       goto switch_229_1;
     } else {
@@ -6876,9 +6889,8 @@ NTSTATUS PptPnpFilterResourceRequirements(PDEVICE_OBJECT DeviceObject,
                       pResourceRequirementsIn);
                 }
               }
-              {} {
-                PptDebugDumpResourceRequirementsList(pResourceRequirementsIn);
-              }
+              {}
+              { PptDebugDumpResourceRequirementsList(pResourceRequirementsIn); }
               goto switch_229_break;
             switch_229_0: /* CIL Label */;
               {} {
@@ -6889,7 +6901,8 @@ NTSTATUS PptPnpFilterResourceRequirements(PDEVICE_OBJECT DeviceObject,
                 {} {
                   PptPnpFilterRemoveIrqResourceLists(pResourceRequirementsIn);
                 }
-                {} {
+                {}
+                {
                   PptDebugDumpResourceRequirementsList(pResourceRequirementsIn);
                 }
               } else {
@@ -7006,7 +7019,9 @@ void PptPnpFilterRemoveIrqResourceLists(
         } else {
           goto while_249_break;
         }
-        {} {} { tmp___0 = PptPnpListContainsIrqResourceDescriptor(curList); }
+        {}
+        {}
+        { tmp___0 = PptPnpListContainsIrqResourceDescriptor(curList); }
         if (tmp___0) {
           {}
           nextList = (struct _IO_RESOURCE_LIST *)(curList->Descriptors +
@@ -7081,7 +7096,8 @@ void PptPnpFilterNukeIrqResourceDescriptorsFromAllLists(
         } else {
           goto while_257_break;
         }
-        {} {
+        {}
+        {
           PptPnpFilterNukeIrqResourceDescriptors(curList);
           curList = (struct _IO_RESOURCE_LIST *)(curList->Descriptors +
                                                  curList->Count);
@@ -8042,9 +8058,9 @@ void PptRegInitDriverSettings(PUNICODE_STRING RegistryPath___0) {
       PptBreakOn = defaultBreakOn;
     } else {
     }
-    {
-        /*   ExFreePool(path); */ /* INLINED */
-    } {}
+    { /*   ExFreePool(path); */ /* INLINED */
+    }
+    {}
     return;
   }
 }
@@ -8915,7 +8931,8 @@ PDEVICE_OBJECT PptBuildDeviceObject(PDRIVER_OBJECT DriverObject,
       goto targetExit;
     } else {
     }
-    {} { status = PptGetPortNumberFromLptName(portName, &portNumber); }
+    {}
+    { status = PptGetPortNumberFromLptName(portName, &portNumber); }
     if (!(status >= 0L)) {
       {} { /*     ExFreePool(portName); */ /* INLINED */
       }
@@ -8930,7 +8947,8 @@ PDEVICE_OBJECT PptBuildDeviceObject(PDRIVER_OBJECT DriverObject,
       goto targetExit;
     } else {
     }
-    {} {
+    {}
+    {
       status = IoCreateDevice(DriverObject, sizeof(DEVICE_EXTENSION),
                               &uniNameString, 22, 256, 0, &deviceObject);
     }
@@ -8951,7 +8969,8 @@ PDEVICE_OBJECT PptBuildDeviceObject(PDRIVER_OBJECT DriverObject,
             goto targetExit;
           } else {
           }
-          {} {
+          {}
+          {
             status = IoCreateDevice(DriverObject, sizeof(DEVICE_EXTENSION),
                                     &uniNameString, 22, 256, 0, &deviceObject);
           }
diff --git a/test/c/ntdrivers/parport_true.i.cil.c b/test/c/ntdrivers/parport_true.i.cil.c
index 4ef6ca1f3..a393ae368 100644
--- a/test/c/ntdrivers/parport_true.i.cil.c
+++ b/test/c/ntdrivers/parport_true.i.cil.c
@@ -2523,7 +2523,8 @@ void PptDebugDumpResourceRequirementsList(
         } else {
           goto while_12_break;
         }
-        {} {
+        {}
+        {
           PptDebugDumpResourceList(curList);
           curList = (struct _IO_RESOURCE_LIST *)(curList->Descriptors +
                                                  curList->Count);
@@ -2932,9 +2933,10 @@ PptRemovePptRemovalRelation(PDEVICE_EXTENSION Extension,
       }
     }
     {
-        /*   ExAcquireFastMutex(& Extension->ExtensionFastMutex); */ /* INLINED
-                                                                      */
-    } {
+      /*   ExAcquireFastMutex(& Extension->ExtensionFastMutex); */ /* INLINED
+                                                                    */
+    }
+    {
       while (1) {
       while_27_continue: /* CIL Label */;
         if (!done) {
@@ -3818,7 +3820,8 @@ BOOLEAN PptIsNecR98Machine(void) {
       }
       return (0);
     }
-    {} { /*   ExFreePool(identifierString.Buffer); */ /* INLINED */
+    {}
+    { /*   ExFreePool(identifierString.Buffer); */ /* INLINED */
     }
     return (0);
   }
@@ -3875,7 +3878,8 @@ NTSTATUS PptDispatchCreate(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
       InterlockedIncrement(&extension->OpenCloseRefCount);
       /*   ExReleaseFastMutex(& extension->OpenCloseMutex); */ /* INLINED */
     }
-    {} {
+    {}
+    {
       PptReleaseRemoveLock(&extension->RemoveLock, Irp);
       Irp->IoStatus.__annonCompField4.Status = status;
       myStatus = status;
@@ -3922,9 +3926,10 @@ NTSTATUS PptDispatchClose(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
       } else {
       }
       {
-          /*     ExReleaseFastMutex(& extension->OpenCloseMutex); */ /* INLINED
-                                                                      */
-      } {}
+        /*     ExReleaseFastMutex(& extension->OpenCloseMutex); */ /* INLINED
+                                                                    */
+      }
+      {}
     } else {
       {
           /*     ExReleaseFastMutex(& extension->OpenCloseMutex); */ /* INLINED
@@ -4925,7 +4930,8 @@ NTSTATUS PptDetectPortType(PDEVICE_EXTENSION Extension) {
       Status = RtlQueryRegistryValues(1, ParportPath.Buffer, RegTable,
                                       (void *)0, (void *)0);
     }
-    {} {}
+    {}
+    {}
     if (Status >= 0L) {
       if (IdentifierHex == 0UL) {
 
@@ -4953,7 +4959,8 @@ NTSTATUS PptDetectPortType(PDEVICE_EXTENSION Extension) {
     } else {
       Status = 3221225473UL;
     }
-    {} { Status = PptDetectPortCapabilities(Extension); }
+    {}
+    { Status = PptDetectPortCapabilities(Extension); }
     {}
     Status = 0L;
     {}
@@ -4989,7 +4996,8 @@ NTSTATUS PptDetectPortCapabilities(PDEVICE_EXTENSION Extension) {
     {}
       Extension->CheckedForGenericEpp = 1;
     }
-    {} { PptDetectBytePort(Extension); }
+    {}
+    { PptDetectBytePort(Extension); }
     if (Extension->PnpInfo.HardwareCapabilities & 11UL) {
       {}
       return (0L);
@@ -5021,7 +5029,8 @@ void PptDetectEcpPort(PDEVICE_EXTENSION Extension) {
       ecr = READ_PORT_UCHAR(wPortECR);
       ecrLast = ecr;
     }
-    {} {
+    {}
+    {
       dcr = (unsigned char)14;
       WRITE_PORT_UCHAR(wPortDCR, dcr);
       ecr = READ_PORT_UCHAR(wPortECR);
@@ -5165,7 +5174,8 @@ void PptDetectEppPort(PDEVICE_EXTENSION Extension) {
       dcr = READ_PORT_UCHAR(Controller + 2);
       Extension->PnpInfo.HardwareCapabilities |= 2UL;
     }
-    {} {
+    {}
+    {
       PptEcrSetMode(Extension, 148);
       WRITE_PORT_UCHAR(Controller + 2, Reverse);
       KeStallExecutionProcessor(5);
@@ -5989,7 +5999,8 @@ PDEVICE_RELATIONS PptPnpBuildRemovalRelations(PDEVICE_EXTENSION Extension) {
       }
     while_185_break: /* CIL Label */;
     }
-    {} {
+    {}
+    {
       tmp = ExAllocatePoolWithTag(1,
                                   (ULONG)sizeof(DEVICE_RELATIONS) +
                                       (count - 1UL) *
@@ -6848,7 +6859,9 @@ NTSTATUS PptPnpFilterResourceRequirements(PDEVICE_OBJECT DeviceObject,
       pResourceRequirementsIn =
           (struct _IO_RESOURCE_REQUIREMENTS_LIST *)Irp->IoStatus.Information;
     }
-    {} {} { PptDebugDumpResourceRequirementsList(pResourceRequirementsIn); }
+    {}
+    {}
+    { PptDebugDumpResourceRequirementsList(pResourceRequirementsIn); }
     if (filterResourceMethod == 1) {
       goto switch_229_1;
     } else {
@@ -6876,9 +6889,8 @@ NTSTATUS PptPnpFilterResourceRequirements(PDEVICE_OBJECT DeviceObject,
                       pResourceRequirementsIn);
                 }
               }
-              {} {
-                PptDebugDumpResourceRequirementsList(pResourceRequirementsIn);
-              }
+              {}
+              { PptDebugDumpResourceRequirementsList(pResourceRequirementsIn); }
               goto switch_229_break;
             switch_229_0: /* CIL Label */;
               {} {
@@ -6889,7 +6901,8 @@ NTSTATUS PptPnpFilterResourceRequirements(PDEVICE_OBJECT DeviceObject,
                 {} {
                   PptPnpFilterRemoveIrqResourceLists(pResourceRequirementsIn);
                 }
-                {} {
+                {}
+                {
                   PptDebugDumpResourceRequirementsList(pResourceRequirementsIn);
                 }
               } else {
@@ -7006,7 +7019,9 @@ void PptPnpFilterRemoveIrqResourceLists(
         } else {
           goto while_249_break;
         }
-        {} {} { tmp___0 = PptPnpListContainsIrqResourceDescriptor(curList); }
+        {}
+        {}
+        { tmp___0 = PptPnpListContainsIrqResourceDescriptor(curList); }
         if (tmp___0) {
           {}
           nextList = (struct _IO_RESOURCE_LIST *)(curList->Descriptors +
@@ -7081,7 +7096,8 @@ void PptPnpFilterNukeIrqResourceDescriptorsFromAllLists(
         } else {
           goto while_257_break;
         }
-        {} {
+        {}
+        {
           PptPnpFilterNukeIrqResourceDescriptors(curList);
           curList = (struct _IO_RESOURCE_LIST *)(curList->Descriptors +
                                                  curList->Count);
@@ -8042,9 +8058,9 @@ void PptRegInitDriverSettings(PUNICODE_STRING RegistryPath___0) {
       PptBreakOn = defaultBreakOn;
     } else {
     }
-    {
-        /*   ExFreePool(path); */ /* INLINED */
-    } {}
+    { /*   ExFreePool(path); */ /* INLINED */
+    }
+    {}
     return;
   }
 }
@@ -8915,7 +8931,8 @@ PDEVICE_OBJECT PptBuildDeviceObject(PDRIVER_OBJECT DriverObject,
       goto targetExit;
     } else {
     }
-    {} { status = PptGetPortNumberFromLptName(portName, &portNumber); }
+    {}
+    { status = PptGetPortNumberFromLptName(portName, &portNumber); }
     if (!(status >= 0L)) {
       {} { /*     ExFreePool(portName); */ /* INLINED */
       }
@@ -8930,7 +8947,8 @@ PDEVICE_OBJECT PptBuildDeviceObject(PDRIVER_OBJECT DriverObject,
       goto targetExit;
     } else {
     }
-    {} {
+    {}
+    {
       status = IoCreateDevice(DriverObject, sizeof(DEVICE_EXTENSION),
                               &uniNameString, 22, 256, 0, &deviceObject);
     }
@@ -8951,7 +8969,8 @@ PDEVICE_OBJECT PptBuildDeviceObject(PDRIVER_OBJECT DriverObject,
             goto targetExit;
           } else {
           }
-          {} {
+          {}
+          {
             status = IoCreateDevice(DriverObject, sizeof(DEVICE_EXTENSION),
                                     &uniNameString, 22, 256, 0, &deviceObject);
           }
diff --git a/tools/externalizer/ExternalizePass.h b/tools/externalizer/ExternalizePass.h
index e25a4b3f1..9bd13f2ba 100644
--- a/tools/externalizer/ExternalizePass.h
+++ b/tools/externalizer/ExternalizePass.h
@@ -12,8 +12,8 @@ namespace externalize {
 struct ExternalizePass : public llvm::ModulePass {
   static char ID;
   ExternalizePass() : llvm::ModulePass(ID) {}
-  virtual llvm::StringRef getPassName() const;
-  virtual bool runOnModule(llvm::Module &M);
+  virtual llvm::StringRef getPassName() const override;
+  virtual bool runOnModule(llvm::Module &M) override;
 };
 } // namespace externalize
 #endif // EXTERNALIZEPASS_H

From a3af50095ebe4a4b8c91b843b03edbe19dafd180 Mon Sep 17 00:00:00 2001
From: JJ Garzella <jjgarzella@gmail.com>
Date: Mon, 11 Oct 2021 11:11:50 -0700
Subject: [PATCH 11/20] AnnotateLoopExits from Module to Function Pass

Changes AnnotateLoopExits from a ModulePass
to a FunctionPass.

With the previous ModulePass version, there were
some crashes happening in the regressions,
which seem to be because LoopInfoWrapperPass
doesn't work with ModulePass in the legacy pass
manager:
https://groups.google.com/g/llvm-dev/c/lVc2-0d2cRs/m/uwuOA_pXAgAJ

I've changed the pass to be a FunctionPass,
and now the regressions work.

This also means that the pass now stores
the "__SMACK_loop_exit" function as a
private member.
---
 include/smack/AnnotateLoopExits.h | 11 ++++++++---
 lib/smack/AnnotateLoopExits.cpp   | 31 +++++++++++++++++--------------
 2 files changed, 25 insertions(+), 17 deletions(-)

diff --git a/include/smack/AnnotateLoopExits.h b/include/smack/AnnotateLoopExits.h
index df0f003b3..3d44ef1c9 100644
--- a/include/smack/AnnotateLoopExits.h
+++ b/include/smack/AnnotateLoopExits.h
@@ -4,6 +4,7 @@
 #ifndef ANNOTATELOOPEXITS_H
 #define ANNOTATELOOPEXITS_H
 
+#include "llvm/IR/Function.h"
 #include "llvm/IR/Instructions.h"
 #include "llvm/IR/Module.h"
 #include "llvm/Pass.h"
@@ -11,12 +12,16 @@
 
 namespace smack {
 
-class AnnotateLoopExits : public llvm::ModulePass {
+class AnnotateLoopExits : public llvm::FunctionPass {
+private:
+  llvm::Function *LoopExitFunction;
+
 public:
   static char ID; // Pass identification, replacement for typeid
-  AnnotateLoopExits() : llvm::ModulePass(ID) {}
+  AnnotateLoopExits() : llvm::FunctionPass(ID) {}
+  bool doInitialization(llvm::Module &M);
   virtual llvm::StringRef getPassName() const override;
-  virtual bool runOnModule(llvm::Module &m) override;
+  virtual bool runOnFunction(llvm::Function &F) override;
   virtual void getAnalysisUsage(llvm::AnalysisUsage &) const override;
 };
 } // namespace smack
diff --git a/lib/smack/AnnotateLoopExits.cpp b/lib/smack/AnnotateLoopExits.cpp
index 83a64b8d3..e05423968 100644
--- a/lib/smack/AnnotateLoopExits.cpp
+++ b/lib/smack/AnnotateLoopExits.cpp
@@ -15,6 +15,7 @@
 #include "llvm/Analysis/LoopInfo.h"
 #include "llvm/IR/Constants.h"
 #include "llvm/IR/Dominators.h"
+#include "llvm/IR/Function.h"
 #include "llvm/IR/IRBuilder.h"
 #include "llvm/IR/InstIterator.h"
 #include "llvm/IR/Module.h"
@@ -30,6 +31,13 @@ namespace smack {
 
 using namespace llvm;
 
+bool AnnotateLoopExits::doInitialization(Module &M) {
+  LoopExitFunction = M.getFunction(Naming::LOOP_EXIT);
+  assert(LoopExitFunction != NULL &&
+         "Function __SMACK_loop_exit should be present.");
+  return true;
+}
+
 // Register LoopInfo
 void AnnotateLoopExits::getAnalysisUsage(AnalysisUsage &AU) const {
   AU.addRequiredID(LoopSimplifyID);
@@ -60,22 +68,17 @@ void annotateLoopExit(Loop *loop, Function *le) {
   }
 }
 
-bool AnnotateLoopExits::runOnModule(Module &m) {
-  Function *le = m.getFunction(Naming::LOOP_EXIT);
-  assert(le != NULL && "Function __SMACK_loop_exit should be present.");
-
-  for (auto F = m.begin(), FEnd = m.end(); F != FEnd; ++F) {
-    if (F->isIntrinsic() || F->empty()) {
-      continue;
-    }
+bool AnnotateLoopExits::runOnFunction(Function &F) {
+  if (F.isIntrinsic() || F.empty()) {
+    return false;
+  }
 
-    LoopInfo &loopInfo = getAnalysis<LoopInfoWrapperPass>(*F).getLoopInfo();
-    for (LoopInfo::iterator LI = loopInfo.begin(), LIEnd = loopInfo.end();
-         LI != LIEnd; ++LI) {
+  LoopInfo &loopInfo = getAnalysis<LoopInfoWrapperPass>().getLoopInfo();
+  for (LoopInfo::iterator LI = loopInfo.begin(), LIEnd = loopInfo.end();
+       LI != LIEnd; ++LI) {
 
-      SDEBUG(errs() << "Processing Loop in " << F->getName() << "\n");
-      annotateLoopExit(*LI, le);
-    }
+    SDEBUG(errs() << "Processing Loop in " << F.getName() << "\n");
+    annotateLoopExit(*LI, LoopExitFunction);
   }
 
   return true;

From 60185b64be4eff751681692f1a4e79aae1616414 Mon Sep 17 00:00:00 2001
From: JJ Garzella <jjgarzella@gmail.com>
Date: Mon, 11 Oct 2021 17:42:28 -0700
Subject: [PATCH 12/20] Add __SMACK_loop_exit to inlined_functions

---
 share/smack/top.py | 1 +
 1 file changed, 1 insertion(+)

diff --git a/share/smack/top.py b/share/smack/top.py
index f3d8af6e4..3b83c66bc 100755
--- a/share/smack/top.py
+++ b/share/smack/top.py
@@ -210,6 +210,7 @@ def inlined_procedures():
         '$initialize',
         '__SMACK_static_init',
         '__SMACK_init_func_memory_model',
+        '__SMACK_loop_exit',
         '__SMACK_check_overflow'
     ]
 

From 1f173536703f5b409ce3f73f65ac09da30bc6eda Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Sun, 17 Oct 2021 20:55:08 -0600
Subject: [PATCH 13/20] Added override to fix a compiler warning

---
 include/smack/AnnotateLoopExits.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/include/smack/AnnotateLoopExits.h b/include/smack/AnnotateLoopExits.h
index 3d44ef1c9..7a96b0068 100644
--- a/include/smack/AnnotateLoopExits.h
+++ b/include/smack/AnnotateLoopExits.h
@@ -19,7 +19,7 @@ class AnnotateLoopExits : public llvm::FunctionPass {
 public:
   static char ID; // Pass identification, replacement for typeid
   AnnotateLoopExits() : llvm::FunctionPass(ID) {}
-  bool doInitialization(llvm::Module &M);
+  bool doInitialization(llvm::Module &M) override;
   virtual llvm::StringRef getPassName() const override;
   virtual bool runOnFunction(llvm::Function &F) override;
   virtual void getAnalysisUsage(llvm::AnalysisUsage &) const override;

From 35bfda5f04548df4a08272767cd9c76a05bda47d Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Mon, 18 Oct 2021 21:20:43 -0600
Subject: [PATCH 14/20] Added unroll folder to regressions

Also, we should only use Corral on the regressions in the unroll folder.
The reason is that Boogie's unrolling of nested loops is not intuitive.
For example, nested loops of 5 iterations each need 25 or so unrolls
in Boogie to be fully unrolled.
---
 .github/workflows/smack-ci.yaml | 1 +
 test/c/unroll/config.yml        | 1 +
 2 files changed, 2 insertions(+)

diff --git a/.github/workflows/smack-ci.yaml b/.github/workflows/smack-ci.yaml
index 1ec7301d8..417f887f1 100644
--- a/.github/workflows/smack-ci.yaml
+++ b/.github/workflows/smack-ci.yaml
@@ -24,6 +24,7 @@ jobs:
             "--exhaustive --folder=c/strings",
             "--exhaustive --folder=c/special",
             "--exhaustive --folder=c/targeted-checks",
+            "--exhaustive --folder=c/unroll",
             "--exhaustive --folder=rust/array --languages=rust",
             "--exhaustive --folder=rust/basic --languages=rust",
             "--exhaustive --folder=rust/box --languages=rust",
diff --git a/test/c/unroll/config.yml b/test/c/unroll/config.yml
index d707344f5..b3a12c5ef 100644
--- a/test/c/unroll/config.yml
+++ b/test/c/unroll/config.yml
@@ -1,2 +1,3 @@
 skip: false
+verifiers: [corral]
 flags: [--fail-on-loop-exit]

From ba87bb23286d05e705f2dcdb397cca4f8a78a621 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Mon, 18 Oct 2021 21:34:27 -0600
Subject: [PATCH 15/20] Updated Boogie and Z3

---
 bin/versions | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/bin/versions b/bin/versions
index e7a5d4319..3add2a0ce 100644
--- a/bin/versions
+++ b/bin/versions
@@ -1,7 +1,7 @@
-Z3_VERSION="4.8.10"
+Z3_VERSION="4.8.12"
 CVC4_VERSION="1.8"
 YICES2_VERSION="2.6.2"
-BOOGIE_VERSION="2.9.1"
+BOOGIE_VERSION="2.9.4"
 CORRAL_VERSION="1.1.8"
 SYMBOOGLIX_COMMIT="ccb2e7f2b3"
 LOCKPWN_COMMIT="12ba58f1ec"

From 832dc04d71cf31ca213f944c4c44a2d9bfa347c3 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Mon, 18 Oct 2021 22:46:20 -0600
Subject: [PATCH 16/20] Fixed Z3 download url

---
 bin/build.sh | 19 ++-----------------
 1 file changed, 2 insertions(+), 17 deletions(-)

diff --git a/bin/build.sh b/bin/build.sh
index bfc441fb1..012c8954f 100755
--- a/bin/build.sh
+++ b/bin/build.sh
@@ -60,6 +60,7 @@ source ${SMACK_DIR}/bin/versions
 
 SMACKENV=${ROOT_DIR}/smack.environment
 WGET="wget --no-verbose"
+Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-glibc-2.31.zip"
 
 # Install prefix -- system default is used if left unspecified
 INSTALL_PREFIX=
@@ -190,7 +191,6 @@ puts "Detected distribution: $distro"
 # Set platform-dependent flags
 case "$distro" in
 linux-opensuse*)
-  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-debian-8.10.zip"
   if [ ${INSTALL_LLVM} -eq 1 ] ; then
     DEPENDENCIES+=" llvm-clang llvm-devel"
   fi
@@ -198,22 +198,7 @@ linux-opensuse*)
   DEPENDENCIES+=" ncurses-devel"
   ;;
 
-linux-@(ubuntu|neon)-16*)
-  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-18.04.zip"
-  if [ ${INSTALL_LLVM} -eq 1 ] ; then
-    DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev"
-  fi
-  ;;
-
-linux-@(ubuntu|neon)-18*)
-  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-18.04.zip"
-  if [ ${INSTALL_LLVM} -eq 1 ] ; then
-    DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev"
-  fi
-  ;;
-
-linux-@(ubuntu|neon)-20*)
-  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-18.04.zip"
+linux-@(ubuntu|neon)-@(16|18|20)*)
   if [ ${INSTALL_LLVM} -eq 1 ] ; then
     DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev"
   fi

From b6c6ff34025883fc734727494db1e89e1b4efae8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mark=20S=2E=20Baranowski=20=28Marek=20Stanis=C5=82aw=20Bar?=
 =?UTF-8?q?anowski=29?= <keram88@users.noreply.github.com>
Date: Tue, 19 Oct 2021 17:59:48 -0600
Subject: [PATCH 17/20] Convert calls to Rust's panic functions to a call to a
 marker (#763)

This removes the calls to panic functions called by Rust programs. Removing the calls enables dead code elimination to remove the arguments flowing into the panic function call.
---
 include/smack/Naming.h           |  1 +
 lib/smack/Naming.cpp             |  2 ++
 lib/smack/RustFixes.cpp          | 24 ++++++++++++++++++++++--
 lib/smack/SmackInstGenerator.cpp |  2 +-
 4 files changed, 26 insertions(+), 3 deletions(-)

diff --git a/include/smack/Naming.h b/include/smack/Naming.h
index a617042e5..acfceb2f5 100644
--- a/include/smack/Naming.h
+++ b/include/smack/Naming.h
@@ -98,6 +98,7 @@ class Naming {
   static const std::string RUST_LANG_START_INTERNAL;
   static const std::vector<std::string> RUST_PANICS;
   static const std::string RUST_PANIC_ANNOTATION;
+  static const std::string RUST_PANIC_MARKER;
 
   static const std::string INT_WRAP_SIGNED_FUNCTION;
   static const std::string INT_WRAP_UNSIGNED_FUNCTION;
diff --git a/lib/smack/Naming.cpp b/lib/smack/Naming.cpp
index ad019c3dc..ce762cb64 100644
--- a/lib/smack/Naming.cpp
+++ b/lib/smack/Naming.cpp
@@ -72,6 +72,8 @@ const std::vector<std::string> Naming::RUST_PANICS = {
 
 const std::string Naming::RUST_PANIC_ANNOTATION = "rust_panic";
 
+const std::string Naming::RUST_PANIC_MARKER = "__SMACK_RUST_PANIC_MARKER";
+
 const std::string Naming::BLOCK_LBL = "$bb";
 const std::string Naming::RET_VAR = "$r";
 const std::string Naming::EXN_VAR = "$exn";
diff --git a/lib/smack/RustFixes.cpp b/lib/smack/RustFixes.cpp
index fcfb01566..92ef7b736 100644
--- a/lib/smack/RustFixes.cpp
+++ b/lib/smack/RustFixes.cpp
@@ -27,7 +27,9 @@ bool isRustNameMatch(StringRef search, StringRef name) {
   return hashed_match || exact_match;
 }
 
-bool replaceRustMemoryFunctions(Function &f) {
+bool replaceSpecialRustFunctions(Function &f) {
+  std::vector<Instruction *> to_remove;
+
   bool changed = false;
   static const std::map<StringRef, StringRef> alloc_fns = {
       {"_ZN5alloc5alloc5alloc17h", "__smack_rust_std_alloc"},
@@ -53,9 +55,27 @@ bool replaceRustMemoryFunctions(Function &f) {
             ci->setCalledFunction(replacement);
           }
         }
+
+        if (Naming::isRustPanic(name)) {
+          // Remove the calls rust panic functions
+          changed = true;
+          // Keep track of the panic call
+          Module *m = f->getParent();
+          FunctionCallee marker = m->getOrInsertFunction(
+              Naming::RUST_PANIC_MARKER, Type::getVoidTy(m->getContext()));
+          CallInst *panic_marker = CallInst::Create(marker);
+          panic_marker->setDebugLoc(ci->getDebugLoc());
+          panic_marker->insertBefore(ci);
+          to_remove.push_back(ci);
+        }
       }
     }
   }
+
+  for (auto ci : to_remove) {
+    ci->eraseFromParent();
+  }
+
   return changed;
 }
 
@@ -127,7 +147,7 @@ bool RustFixes::runOnFunction(Function &F) {
     if (name == "main") {
       result |= fixEntry(F);
     }
-    result |= replaceRustMemoryFunctions(F);
+    result |= replaceSpecialRustFunctions(F);
   }
 
   return result;
diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp
index 86a7a498a..fc13f70ac 100644
--- a/lib/smack/SmackInstGenerator.cpp
+++ b/lib/smack/SmackInstGenerator.cpp
@@ -648,7 +648,7 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst &ci) {
 
   StringRef name = f->hasName() ? f->getName() : "";
 
-  if (SmackOptions::RustPanics && Naming::isRustPanic(name) &&
+  if (SmackOptions::RustPanics && name == Naming::RUST_PANIC_MARKER &&
       SmackOptions::shouldCheckFunction(
           ci.getParent()->getParent()->getName())) {
     // Convert Rust's panic functions into assertion violations

From 1f80e6362b65ff02b06479e927a312a6c55bcb51 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Mon, 25 Oct 2021 21:08:10 -0600
Subject: [PATCH 18/20] Updated Boogie

---
 bin/versions | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/bin/versions b/bin/versions
index 3add2a0ce..35146303e 100644
--- a/bin/versions
+++ b/bin/versions
@@ -1,7 +1,7 @@
 Z3_VERSION="4.8.12"
 CVC4_VERSION="1.8"
 YICES2_VERSION="2.6.2"
-BOOGIE_VERSION="2.9.4"
+BOOGIE_VERSION="2.9.6"
 CORRAL_VERSION="1.1.8"
 SYMBOOGLIX_COMMIT="ccb2e7f2b3"
 LOCKPWN_COMMIT="12ba58f1ec"

From 12f23972824f91d27dd96a02af23d45428bbf9ab Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Fri, 29 Oct 2021 13:27:31 -0600
Subject: [PATCH 19/20] Updated SMACK to use main branch instead of master

Closes #765
---
 CONTRIBUTING.md      | 2 +-
 README.md            | 2 +-
 docs/installation.md | 6 +++---
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 5bee11e92..c872336d4 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -8,7 +8,7 @@ items before you start contributing:
   By participating, you are expected to honor this code.
 * We use this [git branching
   model](http://nvie.com/posts/a-successful-git-branching-model/). Please avoid
-  working directly on the `master` branch.
+  working directly on the `main` branch.
 * We follow guidelines for [good git commit
   practice](https://wiki.openstack.org/wiki/GitCommitMessages)
 * We follow the [LLVM Coding
diff --git a/README.md b/README.md
index f3bb22ae8..990ee40bc 100644
--- a/README.md
+++ b/README.md
@@ -1,4 +1,4 @@
-[![master branch ci status](https://github.com/smackers/smack/workflows/SMACK%20CI/badge.svg?branch=master)](https://github.com/smackers/smack/actions)
+[![main branch ci status](https://github.com/smackers/smack/workflows/SMACK%20CI/badge.svg?branch=main)](https://github.com/smackers/smack/actions)
 [![develop branch ci status](https://github.com/smackers/smack/workflows/SMACK%20CI/badge.svg?branch=develop)](https://github.com/smackers/smack/actions)
 
 <img src="docs/smack-logo.png" width=400 alt="SMACK Logo" align="right">
diff --git a/docs/installation.md b/docs/installation.md
index ae6ee2502..a449dbd78 100644
--- a/docs/installation.md
+++ b/docs/installation.md
@@ -51,7 +51,7 @@ the following configurations:
 SMACK's Docker container images can be pulled from Docker Hub directly:
 
 ```shell
-docker pull smackers/smack:stable # built from the master branch
+docker pull smackers/smack:stable # built from the main branch
 docker pull smackers/smack:latest # built from the develop branch
 ```
 
@@ -83,7 +83,7 @@ SMACK depends on the following projects:
 * [Boogie][] or [Corral][] or compatible Boogie-format verifier
 * [sea-dsa][]
 
-See [here](https://github.com/smackers/smack/blob/master/bin/versions) for
+See [here](https://github.com/smackers/smack/blob/main/bin/versions) for
 compatible version numbers of [Boogie][] and [Corral][]. See the appropriate
 installation instructions below for installing these requirements.
 
@@ -198,7 +198,7 @@ shell in the `test` directory by executing
 [Mono]: http://www.mono-project.com/
 [Cygwin]: https://www.cygwin.com
 [.NET]: https://msdn.microsoft.com/en-us/vstudio/aa496123.aspx
-[build.sh]: https://github.com/smackers/smack/blob/master/bin/build.sh
+[build.sh]: https://github.com/smackers/smack/blob/main/bin/build.sh
 [Xcode]: https://developer.apple.com/xcode/
 [Homebrew]: http://brew.sh/
 [Homebrew Cask]: https://formulae.brew.sh/cask/

From 6d30af23950879ca52d27a00023e18e33e4962d4 Mon Sep 17 00:00:00 2001
From: Zvonimir <zvonimir@cs.utah.edu>
Date: Fri, 29 Oct 2021 13:33:03 -0600
Subject: [PATCH 20/20] Bumped version number to 2.8.0

---
 Doxyfile             | 2 +-
 share/smack/reach.py | 2 +-
 share/smack/top.py   | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Doxyfile b/Doxyfile
index f9b99dad3..69b64e676 100644
--- a/Doxyfile
+++ b/Doxyfile
@@ -5,7 +5,7 @@
 #---------------------------------------------------------------------------
 DOXYFILE_ENCODING      = UTF-8
 PROJECT_NAME           = smack
-PROJECT_NUMBER         = 2.7.1
+PROJECT_NUMBER         = 2.8.0
 PROJECT_BRIEF          = "A bounded software verifier."
 PROJECT_LOGO           =
 OUTPUT_DIRECTORY       = docs
diff --git a/share/smack/reach.py b/share/smack/reach.py
index e1cfd0344..82bf00e78 100755
--- a/share/smack/reach.py
+++ b/share/smack/reach.py
@@ -11,7 +11,7 @@
 from smackgen import *
 from smackverify import *
 
-VERSION = '2.7.1'
+VERSION = '2.8.0'
 
 
 def reachParser():
diff --git a/share/smack/top.py b/share/smack/top.py
index bba90ebdf..4a7fd195c 100755
--- a/share/smack/top.py
+++ b/share/smack/top.py
@@ -14,7 +14,7 @@
 from .frontend import link_bc_files, frontends, languages, extra_libs
 from .errtrace import error_trace, json_output_str
 
-VERSION = '2.7.1'
+VERSION = '2.8.0'
 
 
 class VResult(Flag):