diff --git a/.github/workflows/smack-ci.yaml b/.github/workflows/smack-ci.yaml
index aa4386ccc..9205d93f9 100644
--- a/.github/workflows/smack-ci.yaml
+++ b/.github/workflows/smack-ci.yaml
@@ -4,15 +4,10 @@ on: [push, pull_request]
 
 jobs:
   check-regressions:
-    env:
-      COMPILER_NAME: clang
-      COMPILER: clang++
-      CXX: clang++
-      CC: clang
     runs-on: ubuntu-20.04
     strategy:
       matrix:
-        travis_env:
+        regtest_env:
           [
             "--exhaustive --folder=c/basic",
             "--exhaustive --folder=c/data",
@@ -37,7 +32,9 @@ jobs:
             "--exhaustive --folder=rust/panic --languages=rust",
             "--exhaustive --folder=rust/recursion --languages=rust",
             "--exhaustive --folder=rust/structures --languages=rust",
-            "--exhaustive --folder=rust/vector --languages=rust"
+            "--exhaustive --folder=rust/vector --languages=rust",
+            "--exhaustive --folder=rust/cargo/** --languages=cargo --threads=1",
+            "--exhaustive --folder=llvm --languages=llvm-ir"
           ]
     steps:
       - uses: actions/checkout@v2
@@ -47,20 +44,58 @@ jobs:
           GITHUB_ACTIONS: true
         run: INSTALL_DEV_DEPENDENCIES=1 INSTALL_RUST=1 ./bin/build.sh
 
-      - run: python3 --version
-      - run: $CXX --version
-      - run: $CC --version
-      - run: clang --version
-      - run: clang++ --version
-      - run: llvm-link --version
-      - run: llvm-config --version
-
       - name: format checking
         run: |
           ./format/run-clang-format.py -r lib/smack include/smack tools share/smack/include share/smack/lib test examples
           flake8 test/regtest.py share/smack/ --extend-exclude share/smack/svcomp/,share/smack/reach.py
-      
+
       - name: compile and test
         env:
-          TRAVIS_ENV: ${{ matrix.travis_env }}
+          REGTEST_ENV: ${{ matrix.regtest_env }}
         run: ./bin/build.sh
+
+  build-and-push-docker:
+    runs-on: ubuntu-20.04
+    needs: check-regressions
+
+    steps:
+      - name: Check Out Repo
+        uses: actions/checkout@v2
+
+      - name: Login to Docker Hub
+        uses: docker/login-action@v1
+        with:
+          username: ${{ secrets.DOCKER_HUB_USERNAME }}
+          password: ${{ secrets.DOCKER_HUB_ACCESS_TOKEN }}
+
+      - name: Set up Docker Buildx
+        id: buildx
+        uses: docker/setup-buildx-action@v1
+
+      # borrowed from:
+      # https://stackoverflow.com/questions/58033366/how-to-get-current-branch-within-github-actions/58035262
+      - name: Extract branch name
+        shell: bash
+        run: echo "##[set-output name=branch;]$(echo ${GITHUB_REF#refs/heads/})"
+        id: extract_branch
+
+      - name: Set tag name
+        shell: bash
+        id: set_tag
+        run: |
+          if [ ${{ steps.extract_branch.outputs.branch }} == 'master' ]; then echo "##[set-output name=docker_tag;]$(echo stable)" && exit 0; fi
+          if [ ${{ steps.extract_branch.outputs.branch }} == 'develop' ]; then echo "##[set-output name=docker_tag;]$(echo latest)" && exit 0; fi
+          echo "##[set-output name=docker_tag;]$(echo none)"
+
+      - name: Build and push
+        if: ${{ steps.set_tag.outputs.docker_tag != 'none' }}
+        id: docker_build
+        uses: docker/build-push-action@v2
+        with:
+          context: ./
+          file: ./Dockerfile
+          push: true
+          tags: smackers/smack:${{ steps.set_tag.outputs.docker_tag }}
+
+      - name: Image digest
+        run: echo ${{ steps.docker_build.outputs.digest }}
diff --git a/CMakeLists.txt b/CMakeLists.txt
index b6959b051..ab522a15a 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -5,14 +5,20 @@
 cmake_minimum_required(VERSION 3.4.3)
 project(smack)
 
-if (NOT WIN32 OR MSYS OR CYGWIN)
+if(NOT WIN32 OR MSYS OR CYGWIN)
 
-  file(STRINGS "bin/versions" LLVM_VERSION_STR REGEX "LLVM_SHORT_VERSION=\"[0-9]+\"")
+  file(STRINGS "bin/versions" LLVM_VERSION_STR
+    REGEX "LLVM_FULL_VERSION=\"[0-9]+\.[0-9]+\.[0-9]+")
+  string(REGEX MATCH "[0-9]+\.[0-9]+" LLVM_EXTENDED_VERSION "${LLVM_VERSION_STR}")
+
+  file(STRINGS "bin/versions" LLVM_VERSION_STR
+    REGEX "LLVM_SHORT_VERSION=\"[0-9]+")
   string(REGEX MATCH "[0-9]+" LLVM_SHORT_VERSION "${LLVM_VERSION_STR}")
 
-  find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-${LLVM_SHORT_VERSION} llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config")
+  find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-${LLVM_SHORT_VERSION}
+    llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config")
 
-  if (LLVM_CONFIG_EXECUTABLE STREQUAL "LLVM_CONFIG_EXECUTABLE-NOTFOUND")
+  if(LLVM_CONFIG_EXECUTABLE STREQUAL "LLVM_CONFIG_EXECUTABLE-NOTFOUND")
     message(FATAL_ERROR "llvm-config could not be found!")
   endif()
 
@@ -22,36 +28,12 @@ if (NOT WIN32 OR MSYS OR CYGWIN)
     OUTPUT_STRIP_TRAILING_WHITESPACE
   )
 
-  # TODO: explain why these are required.
-  string(REPLACE "-DNDEBUG" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
-  string(REPLACE "-Wno-maybe-uninitialized" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
-  string(REPLACE "-fuse-ld=gold" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
-  string(REPLACE "--no-keep-files-mapped" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
-  string(REPLACE "--no-map-whole-files" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
-  string(REPLACE "-Wl," "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
-  string(REPLACE "-gsplit-dwarf" "" LLVM_CXXFLAGS "${LLVM_CXXFLAGS}")
-  string(REGEX REPLACE "-O[0-9]" "" CMAKE_CXX_FLAGS "${LLVM_CXXFLAGS}")
-
-  # TODO: append these one at a time; give rationale.
-  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fno-exceptions -fno-rtti -Wno-undefined-var-template")
-
-  # Apparently avoids a problem with inconsistent visibility settings from LLVM:
-  #
-  # > ld: warning: direct access in function 'llvm::_'
-  # >   from file '/usr/local/opt/llvm@8/lib/_'
-  # >   to global weak symbol 'llvm::_'
-  # >   from file 'libsmackTranslator.a(_.cpp.o)'
-  # >   means the weak symbol cannot be overridden at runtime.
-  # >   This was likely caused by different translation units being compiled
-  # >   with different visibility settings.
-  #
-  # Solution found on Stack Overflow:
-  # https://stackoverflow.com/questions/8685045/xcode-with-boost-linkerid-warning-about-visibility-settings
-  string(APPEND CMAKE_CXX_FLAGS_DEBUG " -fvisibility=hidden")
-
-  # TODO: explain why these are required.
-  string(APPEND CMAKE_CXX_FLAGS_DEBUG " -O0")
-  string(APPEND CMAKE_C_FLAGS_DEBUG " -O0")
+  # SMACK doesn't catch or throw exceptions, so -fno-exceptions is justified.
+  # SMACK doesn't use C++ runtime type identification features, so -fno-rtti
+  # is justified.
+  # Shaobo: enable O3 so SMACK can save some time.
+  set(CMAKE_CXX_FLAGS
+    "${LLVM_CXXFLAGS} -fno-exceptions -fno-rtti -O3")
 
   execute_process(
     COMMAND ${LLVM_CONFIG_EXECUTABLE} --libs
@@ -76,12 +58,12 @@ else()
   set(LLVM_BUILD "" CACHE PATH "LLVM build directory")
   set(LLVM_BUILD_TYPE "" CACHE STRING "LLVM build type")
 
-  if (NOT EXISTS "${LLVM_SRC}/include/llvm")
+  if(NOT EXISTS "${LLVM_SRC}/include/llvm")
     message(FATAL_ERROR "Invalid LLVM source directory: ${LLVM_SRC}")
   endif()
 
   set(LLVM_LIBDIR "${LLVM_BUILD}/lib/${LLVM_BUILD_TYPE}")
-  if (NOT EXISTS "${LLVM_LIBDIR}")
+  if(NOT EXISTS "${LLVM_LIBDIR}")
     message(FATAL_ERROR "Invalid LLVM build directory: ${LLVM_BUILD}")
   endif()
 
@@ -92,7 +74,11 @@ else()
   set(CMAKE_CXX_FLAGS "\"/I${LLVM_SRC}/include\" \"/I${LLVM_BUILD}/include\" -D_SCL_SECURE_NO_WARNINGS -wd4146 -wd4244 -wd4355 -wd4482 -wd4800")
 
   set(LLVM_LDFLAGS "")
-  set(LLVM_LIBS "${LLVM_LIBDIR}/LLVMTransformUtils.lib" "${LLVM_LIBDIR}/LLVMipa.lib" "${LLVM_LIBDIR}/LLVMAnalysis.lib" "${LLVM_LIBDIR}/LLVMTarget.lib" "${LLVM_LIBDIR}/LLVMMC.lib" "${LLVM_LIBDIR}/LLVMObject.lib" "${LLVM_LIBDIR}/LLVMBitReader.lib" "${LLVM_LIBDIR}/LLVMCore.lib" "${LLVM_LIBDIR}/LLVMSupport.lib")
+  set(LLVM_LIBS "${LLVM_LIBDIR}/LLVMTransformUtils.lib"
+    "${LLVM_LIBDIR}/LLVMipa.lib" "${LLVM_LIBDIR}/LLVMAnalysis.lib"
+    "${LLVM_LIBDIR}/LLVMTarget.lib" "${LLVM_LIBDIR}/LLVMMC.lib"
+    "${LLVM_LIBDIR}/LLVMObject.lib" "${LLVM_LIBDIR}/LLVMBitReader.lib"
+    "${LLVM_LIBDIR}/LLVMCore.lib" "${LLVM_LIBDIR}/LLVMSupport.lib")
 
 endif()
 
@@ -170,13 +156,17 @@ add_executable(llvm2bpl
 )
 
 # We need to include Boost header files at least for macOS
-find_package (Boost 1.55)
-if (Boost_FOUND)
-  include_directories (${Boost_INCLUDE_DIRS})
-endif ()
+find_package(Boost 1.55)
+if(Boost_FOUND)
+  include_directories(${Boost_INCLUDE_DIRS})
+endif()
 # We have to import LLVM's cmake definitions to build sea-dsa
 # Borrowed from sea-dsa's CMakeLists.txt
-find_package (LLVM ${LLVM_SHORT_VERSION} CONFIG)
+# Borrowed from https://github.com/banach-space/llvm-tutor/commit/72cb20d058b9b3f51717c7a17607f7a4c7398642
+find_package (LLVM ${LLVM_EXTENDED_VERSION} REQUIRED CONFIG)
+if (NOT ${LLVM_SHORT_VERSION} VERSION_EQUAL "${LLVM_VERSION_MAJOR}")
+  message(FATAL_ERROR "Found LLVM ${LLVM_VERSION_MAJOR}, but need ${LLVM_SHORT_VERSION}")
+endif ()
 list(APPEND CMAKE_MODULE_PATH "${LLVM_CMAKE_DIR}")
 include(AddLLVM)
 include(HandleLLVMOptions)
@@ -188,14 +178,15 @@ set(CMAKE_BUILD_TYPE "Release")
 add_subdirectory(sea-dsa/lib/seadsa)
 set(CMAKE_BUILD_TYPE ${SMACK_BUILD_TYPE})
 
-target_link_libraries(smackTranslator ${LLVM_LIBS} ${LLVM_SYSTEM_LIBS} ${LLVM_LDFLAGS})
+target_link_libraries(smackTranslator ${LLVM_LIBS} ${LLVM_SYSTEM_LIBS}
+  ${LLVM_LDFLAGS})
 target_link_libraries(llvm2bpl smackTranslator utils SeaDsaAnalysis)
 
-INSTALL(TARGETS llvm2bpl
+install(TARGETS llvm2bpl
   RUNTIME DESTINATION bin
 )
 
-INSTALL(FILES
+install(FILES
   ${CMAKE_CURRENT_SOURCE_DIR}/bin/smack
   ${CMAKE_CURRENT_SOURCE_DIR}/bin/smack-doctor
   ${CMAKE_CURRENT_SOURCE_DIR}/bin/smack-svcomp-wrapper.sh
@@ -204,30 +195,31 @@ INSTALL(FILES
   DESTINATION bin
 )
 
-INSTALL(DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/share/smack
+install(DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/share/smack
   DESTINATION share
   USE_SOURCE_PERMISSIONS
-  FILES_MATCHING PATTERN "*.py" PATTERN "*.h" PATTERN "*.c" PATTERN "Makefile" PATTERN "*.rs" PATTERN "*.f90" PATTERN "*.di" PATTERN "*.toml"
+  FILES_MATCHING PATTERN "*.py" PATTERN "*.h" PATTERN "*.c" PATTERN "Makefile"
+    PATTERN "*.rs" PATTERN "*.f90" PATTERN "*.di" PATTERN "*.toml"
 )
 
-INSTALL(FILES
+install(FILES
   ${CMAKE_CURRENT_SOURCE_DIR}/bin/versions
   DESTINATION share/smack
   RENAME versions.py
 )
 
-INSTALL(FILES
+install(FILES
   ${CMAKE_CURRENT_SOURCE_DIR}/share/smack/lib/smack/Cargo.toml
   ${CMAKE_CURRENT_SOURCE_DIR}/share/smack/lib/smack/build.rs
   DESTINATION share/smack/lib
 )
 
-INSTALL(FILES
+install(FILES
   ${CMAKE_CURRENT_SOURCE_DIR}/share/smack/lib/smack-rust.c
   DESTINATION share/smack/lib/src
 )
 
-INSTALL(FILES
+install(FILES
   ${CMAKE_CURRENT_SOURCE_DIR}/share/smack/lib/smack.rs
   DESTINATION share/smack/lib/src
   RENAME lib.rs
diff --git a/Dockerfile b/Dockerfile
index fbb10f8bc..198ddeac8 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -1,5 +1,5 @@
-FROM ubuntu:18.04
-MAINTAINER Shaobo He <shaobo@cs.utah.edu>
+FROM ubuntu:20.04
+MAINTAINER Shaobo He <polarishehn@gmail.com>
 
 ENV SMACKDIR /home/user/smack
 
@@ -7,7 +7,8 @@ RUN apt-get update && \
       apt-get -y install \
       software-properties-common \
       wget \
-      sudo
+      sudo \
+      g++
 
 # Borrowed from JFS
 # Create `user` user for container with password `user`.  and give it
@@ -26,7 +27,7 @@ ADD --chown=user . $SMACKDIR
 WORKDIR $SMACKDIR
 
 # Build SMACK
-RUN sudo bin/build.sh
+RUN bin/build.sh
 
 # Add envinronment
 RUN echo "source /home/user/smack.environment" >> ~/.bashrc
diff --git a/Doxyfile b/Doxyfile
index 1dac17777..8b235a352 100644
--- a/Doxyfile
+++ b/Doxyfile
@@ -5,7 +5,7 @@
 #---------------------------------------------------------------------------
 DOXYFILE_ENCODING      = UTF-8
 PROJECT_NAME           = smack
-PROJECT_NUMBER         = 2.6.3
+PROJECT_NUMBER         = 2.7.0
 PROJECT_BRIEF          = "A bounded software verifier."
 PROJECT_LOGO           =
 OUTPUT_DIRECTORY       = docs
diff --git a/LICENSE b/LICENSE
index 28c461c44..0b3d59da5 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,8 +1,8 @@
 The MIT License
 
-Copyright (c) 2008-2020 Zvonimir Rakamaric (zvonimir@cs.utah.edu),
+Copyright (c) 2008-2021 Zvonimir Rakamaric (zvonimir@cs.utah.edu),
                         Michael Emmi (michael.emmi@gmail.com)
-Modified work Copyright (c) 2013-2020 Marek Baranowski,
+Modified work Copyright (c) 2013-2021 Marek Baranowski,
                                       Montgomery Carter,
                                       Pantazis Deligiannis,
                                       Jack J. Garzella,
diff --git a/README.md b/README.md
index c455600c2..8af7feac4 100644
--- a/README.md
+++ b/README.md
@@ -48,7 +48,7 @@ See below for system requirements, installation, usage, and everything else.
 ### Acknowledgements
 
 SMACK project has been partially supported by funding from the National Science
-Foundation, VMware, and Microsoft Research. We also rely on University of
+Foundation, VMware, Amazon, and Microsoft Research. We also rely on University of
 Utah's [Emulab](http://www.emulab.net/) infrastructure for extensive
 benchmarking of SMACK.
 
diff --git a/Vagrantfile b/Vagrantfile
index 67b33b4a7..069981207 100644
--- a/Vagrantfile
+++ b/Vagrantfile
@@ -26,8 +26,8 @@ Vagrant.configure(2) do |config|
   # end
 
   config.vm.provision "shell", binary: true, privileged: false, inline: <<-SHELL
-    apt-get update
-    apt-get install -y software-properties-common
+    sudo apt update
+    sudo apt install -y build-essential
     cd /home/vagrant
     ./#{project_name}/bin/build.sh
     echo source smack.environment >> .bashrc
diff --git a/bin/build.sh b/bin/build.sh
index 1094560b4..be9dd51ab 100755
--- a/bin/build.sh
+++ b/bin/build.sh
@@ -162,7 +162,7 @@ function upToDate {
   else
     cd $1
     hash=$(git rev-parse --short=10 HEAD)
-    if [ "$TRAVIS" != "true" ] || [ $hash == $2 ] ; then
+    if [ $hash == $2 ] ; then
       return 0
     else
       return 1
@@ -195,17 +195,17 @@ linux-opensuse*)
   ;;
 
 linux-@(ubuntu|neon)-16*)
-  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-16.04.zip"
+  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-18.04.zip"
   DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev"
   ;;
 
 linux-@(ubuntu|neon)-18*)
-  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-16.04.zip"
+  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-18.04.zip"
   DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev"
   ;;
 
 linux-@(ubuntu|neon)-20*)
-  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-16.04.zip"
+  Z3_DOWNLOAD_LINK="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/z3-${Z3_VERSION}-x64-ubuntu-18.04.zip"
   DEPENDENCIES+=" clang-${LLVM_SHORT_VERSION} llvm-${LLVM_SHORT_VERSION}-dev"
   ;;
 
@@ -237,7 +237,7 @@ do
 done
 
 
-if [ ${INSTALL_DEPENDENCIES} -eq 1 ] && [ "$TRAVIS" != "true" ] ; then
+if [ ${INSTALL_DEPENDENCIES} -eq 1 ] ; then
   puts "Installing required packages"
 
   case "$distro" in
@@ -278,11 +278,6 @@ if [ ${INSTALL_DEPENDENCIES} -eq 1 ] && [ "$TRAVIS" != "true" ] ; then
     sudo apt-get update
 
     sudo apt-get install -y ${DEPENDENCIES}
-    sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-${LLVM_SHORT_VERSION} 30
-    sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-${LLVM_SHORT_VERSION} 30
-    sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-${LLVM_SHORT_VERSION} 30
-    sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-${LLVM_SHORT_VERSION} 30
-    sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-${LLVM_SHORT_VERSION} 30
     ;;
 
   *)
@@ -295,7 +290,7 @@ if [ ${INSTALL_DEPENDENCIES} -eq 1 ] && [ "$TRAVIS" != "true" ] ; then
 fi
 
 
-if [ ${INSTALL_MONO} -eq 1 ] && [ "$TRAVIS" != "true" ] ; then
+if [ ${INSTALL_MONO} -eq 1 ] ; then
   puts "Installing mono"
   # Adding Mono repository
   sudo apt-key adv --keyserver hkp://keyserver.ubuntu.com:80 --recv-keys 3FA7E0328081BFF6A14DA29AA6A19B38D3D831EF
@@ -310,13 +305,12 @@ if [ ${BUILD_LLVM} -eq 1 ] ; then
   puts "Building LLVM"
   mkdir -p ${LLVM_DIR}/src/{tools/clang,projects/compiler-rt}
   mkdir -p ${LLVM_DIR}/build
-
-  ${WGET} http://llvm.org/releases/${LLVM_FULL_VERSION}/llvm-${LLVM_FULL_VERSION}.src.tar.xz
-  ${WGET} http://llvm.org/releases/${LLVM_FULL_VERSION}/cfe-${LLVM_FULL_VERSION}.src.tar.xz
-  ${WGET} http://llvm.org/releases/${LLVM_FULL_VERSION}/compiler-rt-${LLVM_FULL_VERSION}.src.tar.xz
+  ${WGET} https://github.com/llvm/llvm-project/releases/download/llvmorg-${LLVM_FULL_VERSION}/llvm-${LLVM_FULL_VERSION}.src.tar.xz
+  ${WGET} https://github.com/llvm/llvm-project/releases/download/llvmorg-${LLVM_FULL_VERSION}/clang-${LLVM_FULL_VERSION}.src.tar.xz
+  ${WGET} https://github.com/llvm/llvm-project/releases/download/llvmorg-${LLVM_FULL_VERSION}/compiler-rt-${LLVM_FULL_VERSION}.src.tar.xz
 
   tar -C ${LLVM_DIR}/src -xvf llvm-${LLVM_FULL_VERSION}.src.tar.xz --strip 1
-  tar -C ${LLVM_DIR}/src/tools/clang -xvf cfe-${LLVM_FULL_VERSION}.src.tar.xz --strip 1
+  tar -C ${LLVM_DIR}/src/tools/clang -xvf clang-${LLVM_FULL_VERSION}.src.tar.xz --strip 1
   tar -C ${LLVM_DIR}/src/projects/compiler-rt -xvf compiler-rt-${LLVM_FULL_VERSION}.src.tar.xz --strip 1
 
   cd ${LLVM_DIR}/build/
@@ -465,7 +459,6 @@ fi
 if [ ${INSTALL_DEV_DEPENDENCIES} -eq 1 ] ; then
   sudo apt-get install -y python3-pip clang-format-${LLVM_SHORT_VERSION}
   sudo pip3 install -U flake8
-  sudo update-alternatives --install /usr/bin/clang-format clang-format /usr/bin/clang-format-${LLVM_SHORT_VERSION} 30
   if [ "${GITHUB_ACTIONS}" = "true" ] ; then
     exit 0
   fi
@@ -481,7 +474,7 @@ if [ ${BUILD_SMACK} -eq 1 ] ; then
 
   mkdir -p ${SMACK_DIR}/build
   cd ${SMACK_DIR}/build
-  cmake ${CMAKE_INSTALL_PREFIX} -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ -DCMAKE_BUILD_TYPE=Debug .. -G Ninja
+  cmake ${CMAKE_INSTALL_PREFIX} -DCMAKE_BUILD_TYPE=Debug .. -G Ninja
   ninja
 
   if [ -n "${CMAKE_INSTALL_PREFIX}" ] ; then
@@ -503,7 +496,7 @@ if [ ${TEST_SMACK} -eq 1 ] ; then
   puts "Running SMACK regression tests"
 
   cd ${SMACK_DIR}/test
-  ./regtest.py ${TRAVIS_ENV}
+  ./regtest.py ${REGTEST_ENV}
   res=$?
 
   puts "Regression tests complete"
diff --git a/bin/versions b/bin/versions
index 4bb97308d..6bc11485a 100644
--- a/bin/versions
+++ b/bin/versions
@@ -1,10 +1,10 @@
-Z3_VERSION="4.8.9"
+Z3_VERSION="4.8.10"
 CVC4_VERSION="1.8"
 YICES2_VERSION="2.6.2"
-BOOGIE_VERSION="2.7.30"
-CORRAL_VERSION="1.0.14"
+BOOGIE_VERSION="2.8.26"
+CORRAL_VERSION="1.0.17"
 SYMBOOGLIX_COMMIT="ccb2e7f2b3"
 LOCKPWN_COMMIT="12ba58f1ec"
-LLVM_SHORT_VERSION="10"
-LLVM_FULL_VERSION="10.0.1"
-RUST_VERSION="nightly-2020-08-23"
\ No newline at end of file
+LLVM_SHORT_VERSION="11"
+LLVM_FULL_VERSION="11.1.0"
+RUST_VERSION="nightly-2021-03-01"
diff --git a/docs/installation.md b/docs/installation.md
index 183e158dd..778d48a6c 100644
--- a/docs/installation.md
+++ b/docs/installation.md
@@ -59,9 +59,20 @@ vagrant destroy
 SMACK can also be run in a [Docker][] container. We tested the Dockerfile on
 the following configurations:
 
-* Ubuntu 16.04, docker-ce version 18.09.7
-* OS X 10.14.5, Docker Desktop with Docker engine version 18.09.2
-* Windows 10, Docker Desktop with Docker engine version 18.09.2
+* Ubuntu 18.04, Docker version 19.03.6
+* Windows WSL Ubuntu 20.04, Docker Desktop with Docker engine version 20.10.2
+
+
+#### Docker Hub
+
+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:latest # built from the develop branch
+```
+
+#### Local Build
 
 Once Docker is successfully installed, build the Docker image by running the
 following command in SMACK's root directory that contains `Dockerfile`:
@@ -80,8 +91,8 @@ to Docker's official documentation.
 
 SMACK depends on the following projects:
 
-* [LLVM][] version [10.0.1][LLVM-10.0.1]
-* [Clang][] version [10.0.1][Clang-10.0.1]
+* [LLVM][] version [11.1.0][LLVM-11.1.0]
+* [Clang][] version [11.1.0][Clang-11.1.0]
 * [Boost][] version 1.55 or greater
 * [Python][] version 3.6.8 or greater
 * [Ninja][] version 1.5.1 or greater
@@ -210,9 +221,9 @@ shell in the `test` directory by executing
 [CMake]: http://www.cmake.org
 [Python]: http://www.python.org
 [LLVM]: http://llvm.org
-[LLVM-10.0.1]: http://llvm.org/releases/download.html#10.0.1
+[LLVM-11.1.0]: http://llvm.org/releases/download.html#11.1.0
 [Clang]: http://clang.llvm.org
-[Clang-10.0.1]: http://llvm.org/releases/download.html#10.0.1
+[Clang-11.1.0]: http://llvm.org/releases/download.html#11.1.0
 [Boogie]: https://github.com/boogie-org/boogie
 [Corral]: https://github.com/boogie-org/corral
 [Z3]: https://github.com/Z3Prover/z3/
diff --git a/format/run-clang-format.py b/format/run-clang-format.py
index 2923ee31a..b8598b29f 100755
--- a/format/run-clang-format.py
+++ b/format/run-clang-format.py
@@ -203,12 +203,19 @@ def print_trouble(prog, message, use_colors):
 
 
 def main():
+
+    with open(os.path.join(os.path.dirname(os.path.dirname(
+        os.path.abspath(__file__))), 'bin', 'versions'), 'r') as f:
+        for line in f.readlines():
+            if line.startswith('LLVM_SHORT_VERSION='):
+                llvm_version = line.strip()[len('LLVM_SHORT_VERSION='):].replace('"', '')
+
     parser = argparse.ArgumentParser(description=__doc__)
     parser.add_argument(
         '--clang-format-executable',
         metavar='EXECUTABLE',
-        help='path to the clang-format executable',
-        default='clang-format')
+        help='path to the clang-format executable (default: %(default)s)',
+        default='clang-format-' + llvm_version)
     parser.add_argument(
         '--extensions',
         help='comma separated list of file extensions (default: {})'.format(
diff --git a/include/smack/Naming.h b/include/smack/Naming.h
index e0abc112a..b0f584050 100644
--- a/include/smack/Naming.h
+++ b/include/smack/Naming.h
@@ -5,6 +5,7 @@
 #ifndef NAMING_H
 #define NAMING_H
 
+#include "llvm/ADT/StringRef.h"
 #include "llvm/IR/Value.h"
 #include "llvm/Support/Regex.h"
 #include <map>
@@ -116,8 +117,9 @@ class Naming {
   static std::string getIntWrapFunc(bool isUnsigned);
 
   static bool isBplKeyword(std::string s);
-  static bool isSmackName(std::string s);
+  static bool isSmackName(llvm::StringRef s);
   static bool isSmackGeneratedName(std::string s);
+  static bool isRustPanic(llvm::StringRef s);
   static std::string escape(std::string s);
 };
 } // namespace smack
diff --git a/include/smack/RustFixes.h b/include/smack/RustFixes.h
index 887997839..ca3c624fb 100644
--- a/include/smack/RustFixes.h
+++ b/include/smack/RustFixes.h
@@ -5,18 +5,16 @@
 #ifndef RUSTFIXES_H
 #define RUSTFIXES_H
 
-#include "llvm/IR/Instructions.h"
-#include "llvm/IR/Module.h"
 #include "llvm/Pass.h"
 
 namespace smack {
 
-class RustFixes : public llvm::ModulePass {
+class RustFixes : public llvm::FunctionPass {
 public:
   static char ID; // Pass identification, replacement for typeid
-  RustFixes() : llvm::ModulePass(ID) {}
+  RustFixes() : llvm::FunctionPass(ID) {}
   virtual llvm::StringRef getPassName() const;
-  virtual bool runOnModule(llvm::Module &m);
+  virtual bool runOnFunction(llvm::Function &F);
 };
 } // namespace smack
 
diff --git a/include/smack/SmackInstGenerator.h b/include/smack/SmackInstGenerator.h
index 47c963ca3..c42b6aa60 100644
--- a/include/smack/SmackInstGenerator.h
+++ b/include/smack/SmackInstGenerator.h
@@ -47,8 +47,6 @@ class SmackInstGenerator : public llvm::InstVisitor<SmackInstGenerator> {
   const Stmt *recordProcedureCall(const llvm::Value *V,
                                   std::list<const Attr *> attrs);
 
-  void generateUnModeledCall(llvm::CallInst *ci);
-
 public:
   void emit(const Stmt *s);
 
diff --git a/include/smack/SmackOptions.h b/include/smack/SmackOptions.h
index 6e6e69149..ce92d93e0 100644
--- a/include/smack/SmackOptions.h
+++ b/include/smack/SmackOptions.h
@@ -36,7 +36,7 @@ class SmackOptions {
   static const llvm::cl::opt<bool> AddTiming;
   static const llvm::cl::opt<bool> WrappedIntegerEncoding;
 
-  static bool isEntryPoint(std::string);
+  static bool isEntryPoint(llvm::StringRef);
 };
 } // namespace smack
 
diff --git a/include/smack/SmackWarnings.h b/include/smack/SmackWarnings.h
index 800d4f84d..b95aa2ed6 100644
--- a/include/smack/SmackWarnings.h
+++ b/include/smack/SmackWarnings.h
@@ -22,8 +22,8 @@ class SmackWarnings {
 public:
   enum class WarningLevel : unsigned {
     Silent = 0,
-    Unsound = 10, // Unhandled intrinsics, asm, etc
-    Info = 20     // Memory length, etc.
+    Imprecise = 10, // Unhandled intrinsics, asm, etc
+    Info = 20       // Memory length, etc.
   };
 
   enum class FlagRelation : unsigned { And = 0, Or = 1 };
@@ -31,23 +31,19 @@ class SmackWarnings {
   static UnsetFlagsT getUnsetFlags(RequiredFlagsT flags);
   static bool isSatisfied(RequiredFlagsT flags, FlagRelation rel);
 
-  // generate warnings about unsoundness
-  static void warnUnsound(std::string unmodeledOpName, Block *currBlock,
-                          const llvm::Instruction *i, bool ignore = false,
-                          FlagRelation rel = FlagRelation::And);
-  static void warnUnsound(std::string name, UnsetFlagsT unsetFlags,
-                          Block *currBlock, const llvm::Instruction *i,
-                          bool ignore = false,
-                          FlagRelation rel = FlagRelation::And);
-  static void warnIfUnsound(std::string name, RequiredFlagsT requiredFlags,
-                            Block *currBlock, const llvm::Instruction *i,
-                            bool ignore = false,
-                            FlagRelation rel = FlagRelation::And);
-  static void warnIfUnsound(std::string name, FlagT &requiredFlag,
-                            Block *currBlock, const llvm::Instruction *i,
-                            FlagRelation rel = FlagRelation::And);
-  static void warnIfUnsound(std::string name, FlagT &requiredFlag1,
-                            FlagT &requiredFlag2, Block *currBlock,
+  static void warnUnModeled(std::string unmodeledOpName, Block *currBlock,
+                            const llvm::Instruction *i);
+
+  static void warnIfIncomplete(std::string name, RequiredFlagsT requiredFlags,
+                               Block *currBlock, const llvm::Instruction *i,
+                               FlagRelation rel = FlagRelation::And);
+
+  static void warnIfIncomplete(std::string name, UnsetFlagsT unsetFlags,
+                               Block *currBlock, const llvm::Instruction *i,
+                               FlagRelation rel);
+
+  static void warnImprecise(std::string name, std::string description,
+                            UnsetFlagsT unsetFlags, Block *currBlock,
                             const llvm::Instruction *i,
                             FlagRelation rel = FlagRelation::And);
 
diff --git a/include/smack/SplitAggregateValue.h b/include/smack/SplitAggregateValue.h
index b09b1642a..94991a9b2 100644
--- a/include/smack/SplitAggregateValue.h
+++ b/include/smack/SplitAggregateValue.h
@@ -23,10 +23,11 @@ class SplitAggregateValue : public llvm::FunctionPass {
   virtual bool runOnFunction(llvm::Function &F);
 
 private:
-  llvm::Value *splitAggregateLoad(llvm::LoadInst *li, std::vector<InfoT> &info,
+  llvm::Value *splitAggregateLoad(llvm::Type *T, llvm::Value *P,
+                                  std::vector<InfoT> &info,
                                   llvm::IRBuilder<> &irb);
-  void splitAggregateStore(llvm::StoreInst *si, std::vector<InfoT> &info,
-                           llvm::IRBuilder<> &irb);
+  void splitAggregateStore(llvm::Value *P, llvm::Value *V,
+                           std::vector<InfoT> &info, llvm::IRBuilder<> &irb);
   void splitConstantReturn(llvm::ReturnInst *ri, std::vector<InfoT> &info);
   void splitConstantArg(llvm::CallInst *ci, unsigned i,
                         std::vector<InfoT> &info);
diff --git a/include/utils/Devirt.h b/include/utils/Devirt.h
index 2514c532c..06fc69d53 100644
--- a/include/utils/Devirt.h
+++ b/include/utils/Devirt.h
@@ -47,15 +47,15 @@ namespace llvm {
       const DataLayout * TD;
 
       // Worklist of call sites to transform
-      std::vector<Instruction *> Worklist;
+      std::vector<CallBase *> Worklist;
 
       // A cache of indirect call targets that have been converted already
       std::map<const Function *, std::set<const Function *> > bounceCache;
 
     protected:
-      void makeDirectCall (CallSite & CS);
-      Function* buildBounce (CallSite cs,std::vector<const Function*>& Targets);
-      const Function* findInCache (const CallSite & CS,
+      void makeDirectCall (CallBase *CS);
+      Function* buildBounce (CallBase *CS,std::vector<const Function*>& Targets);
+      const Function* findInCache (const CallBase *CS,
                                    std::set<const Function*>& Targets);
 
     public:
@@ -70,14 +70,12 @@ namespace llvm {
 
       // Visitor methods for analyzing instructions
       //void visitInstruction(Instruction &I);
-      void processCallSite(CallSite &CS);
+      void processCallSite(CallBase *CS);
       void visitCallInst(CallInst &CI) {
-        CallSite CS(&CI);
-        processCallSite(CS);
+        processCallSite(&CI);
       }
       void visitInvokeInst(InvokeInst &II) {
-        CallSite CS(&II);
-        processCallSite(CS);
+        processCallSite(&II);
       }
   };
 }
diff --git a/lib/smack/AddTiming.cpp b/lib/smack/AddTiming.cpp
index 7cc074857..b165e7634 100644
--- a/lib/smack/AddTiming.cpp
+++ b/lib/smack/AddTiming.cpp
@@ -52,8 +52,7 @@ const std::string AddTiming::INT_TIMING_COST_METADATA =
 const std::string AddTiming::INSTRUCTION_NAME_METADATA =
     "smack.LLVMInstructionName";
 
-static bool begins_with(const std::string &possible_prefix,
-                        const std::string &the_string) {
+static bool begins_with(StringRef possible_prefix, StringRef the_string) {
   return (0 == the_string.find(possible_prefix));
 }
 
@@ -169,8 +168,9 @@ unsigned AddTiming::getInstructionCost(const Instruction *I) const {
         getOperandInfo(I->getOperand(0));
     TargetTransformInfo::OperandValueKind Op2VK =
         getOperandInfo(I->getOperand(1));
-    return TTI->getArithmeticInstrCost(I->getOpcode(), I->getType(), Op1VK,
-                                       Op2VK);
+    return TTI->getArithmeticInstrCost(
+        I->getOpcode(), I->getType(),
+        TargetTransformInfo::TargetCostKind::TCK_Latency, Op1VK, Op2VK);
   }
   case Instruction::Select: {
     const SelectInst *SI = cast<SelectInst>(I);
@@ -188,7 +188,7 @@ unsigned AddTiming::getInstructionCost(const Instruction *I) const {
     assert(!ValTy->isStructTy() &&
            "Timing annotations do not currently work for struct sized stores");
     return TTI->getMemoryOpCost(I->getOpcode(), ValTy,
-                                MaybeAlign(SI->getAlignment()),
+                                Align(SI->getAlignment()),
                                 SI->getPointerAddressSpace());
   }
   case Instruction::Load: {
@@ -196,7 +196,7 @@ unsigned AddTiming::getInstructionCost(const Instruction *I) const {
     assert(!I->getType()->isStructTy() &&
            "Timing annotations do not currently work for struct sized loads");
     return TTI->getMemoryOpCost(I->getOpcode(), I->getType(),
-                                MaybeAlign(LI->getAlignment()),
+                                Align(LI->getAlignment()),
                                 LI->getPointerAddressSpace());
   }
   case Instruction::ZExt:
@@ -234,8 +234,10 @@ unsigned AddTiming::getInstructionCost(const Instruction *I) const {
       if (auto *FPMO = dyn_cast<FPMathOperator>(II)) {
         FMF = FPMO->getFastMathFlags();
       }
-      return TTI->getIntrinsicInstrCost(II->getIntrinsicID(), II->getType(),
-                                        Tys, FMF);
+      return TTI->getIntrinsicInstrCost(
+          IntrinsicCostAttributes(II->getIntrinsicID(), II->getType(), Tys,
+                                  FMF),
+          TargetTransformInfo::TargetCostKind::TCK_Latency);
     }
 
     return NO_TIMING_INFO;
diff --git a/lib/smack/Debug.cpp b/lib/smack/Debug.cpp
index 4a3c3d06d..a964aa494 100644
--- a/lib/smack/Debug.cpp
+++ b/lib/smack/Debug.cpp
@@ -55,7 +55,7 @@ struct DebugOnlyOpt {
     SmallVector<StringRef, 8> dbgTypes;
     StringRef(Val).split(dbgTypes, ',', -1, false);
     for (auto dbgType : dbgTypes)
-      CurrentDebugType->push_back(dbgType);
+      CurrentDebugType->push_back(dbgType.str());
   }
 };
 } // namespace
diff --git a/lib/smack/IntegerOverflowChecker.cpp b/lib/smack/IntegerOverflowChecker.cpp
index 5b92cb3aa..fe2d9a648 100644
--- a/lib/smack/IntegerOverflowChecker.cpp
+++ b/lib/smack/IntegerOverflowChecker.cpp
@@ -127,10 +127,10 @@ bool IntegerOverflowChecker::runOnModule(Module &m) {
       if (auto ci = dyn_cast<CallInst>(&*I)) {
         Function *f = ci->getCalledFunction();
         if (f && f->hasName()) {
-          std::string fn = f->getName();
+          auto fn = f->getName();
           if (fn.find("__ubsan_handle_shift_out_of_bounds") !=
-                  std::string::npos ||
-              fn.find("__ubsan_handle_divrem_overflow") != std::string::npos) {
+                  StringRef::npos ||
+              fn.find("__ubsan_handle_divrem_overflow") != StringRef::npos) {
             // If the call to __ubsan_handle_* is reachable,
             // then an overflow is possible.
             if (SmackOptions::IntegerOverflow) {
@@ -144,7 +144,7 @@ bool IntegerOverflowChecker::runOnModule(Module &m) {
             }
           }
           SmallVector<StringRef, 4> info;
-          if (OVERFLOW_INTRINSICS.match(f->getName(), &info)) {
+          if (OVERFLOW_INTRINSICS.match(fn, &info)) {
             /*
              * If ei is an ExtractValueInst whose value flows from an LLVM
              * checked value intrinsic f, then we do the following:
@@ -158,12 +158,13 @@ bool IntegerOverflowChecker::runOnModule(Module &m) {
              * - Finally, an assumption about the value of the flag is created
              *   to block erroneous checking of paths after the overflow check.
              */
-            SDEBUG(errs() << "Processing intrinsic: " << f->getName().str()
-                          << "\n");
+            SDEBUG(errs() << "Processing intrinsic: " << fn << "\n");
             assert(info.size() == 4 && "Must capture three matched strings.");
             bool isSigned = (info[1] == "s");
-            std::string op = info[2];
-            int bits = std::stoi(info[3]);
+            std::string op = info[2].str();
+            unsigned bits = 0;
+            auto res = info[3].getAsInteger(10, bits);
+            assert(!res && "Invalid bit widths.");
             Value *eo1 =
                 extendBitWidth(ci->getArgOperand(0), bits, isSigned, ci);
             Value *eo2 =
diff --git a/lib/smack/Naming.cpp b/lib/smack/Naming.cpp
index ad6ba73e0..9d8bb5f1c 100644
--- a/lib/smack/Naming.cpp
+++ b/lib/smack/Naming.cpp
@@ -161,12 +161,23 @@ Regex Naming::SMACK_NAME(".*__SMACK_.*");
 
 bool Naming::isBplKeyword(std::string s) { return BPL_KW.match(s); }
 
-bool Naming::isSmackName(std::string n) { return SMACK_NAME.match(n); }
+bool Naming::isSmackName(llvm::StringRef n) { return SMACK_NAME.match(n); }
 
 bool Naming::isSmackGeneratedName(std::string n) {
   return n.size() > 0 && n[0] == '$';
 }
 
+bool Naming::isRustPanic(llvm::StringRef name) {
+  for (const auto &panic : Naming::RUST_PANICS) {
+    // We are interested in exact functional matches.
+    // Rust mangled names include a 17 byte hash at the end.
+    if (name.find(panic) == 0 && name.size() == panic.size() + 17) {
+      return true;
+    }
+  }
+  return false;
+}
+
 std::string Naming::escape(std::string s) {
   std::string Str(s);
   for (unsigned i = 0; i != Str.length(); ++i)
diff --git a/lib/smack/RemoveDeadDefs.cpp b/lib/smack/RemoveDeadDefs.cpp
index 0caecdaea..dc51819ac 100644
--- a/lib/smack/RemoveDeadDefs.cpp
+++ b/lib/smack/RemoveDeadDefs.cpp
@@ -23,15 +23,15 @@ bool RemoveDeadDefs::runOnModule(Module &M) {
   do {
     dead.clear();
     for (Function &F : M) {
-      std::string name = F.getName();
+      auto name = F.getName();
 
       if (!(F.isDefTriviallyDead() || F.getNumUses() == 0))
         continue;
 
-      if (name.find("__SMACK_") != std::string::npos)
+      if (name.find("__SMACK_") != StringRef::npos)
         continue;
 
-      if (name.find("__VERIFIER_assume") != std::string::npos)
+      if (name.find("__VERIFIER_assume") != StringRef::npos)
         continue;
 
       if (SmackOptions::isEntryPoint(name))
diff --git a/lib/smack/RustFixes.cpp b/lib/smack/RustFixes.cpp
index 32c5809de..fcfb01566 100644
--- a/lib/smack/RustFixes.cpp
+++ b/lib/smack/RustFixes.cpp
@@ -7,18 +7,58 @@
 
 #include "smack/RustFixes.h"
 #include "smack/Naming.h"
-#include "llvm/Analysis/CallGraph.h"
-#include "llvm/IR/IRBuilder.h"
 #include "llvm/IR/InstIterator.h"
+#include "llvm/IR/Instructions.h"
 #include "llvm/IR/Module.h"
 #include "llvm/Support/raw_ostream.h"
-#include <set>
+#include <map>
 #include <string>
 
 namespace smack {
 
 using namespace llvm;
 
+bool isRustNameMatch(StringRef search, StringRef name) {
+  // Check if we are looking for a Rust mangled name with a 17 character hash
+  // suffix, denoted by `17h'
+  bool hashed_match = search.endswith("17h") && name.startswith(search) &&
+                      search.size() + 17 == name.size();
+  bool exact_match = search == name;
+  return hashed_match || exact_match;
+}
+
+bool replaceRustMemoryFunctions(Function &f) {
+  bool changed = false;
+  static const std::map<StringRef, StringRef> alloc_fns = {
+      {"_ZN5alloc5alloc5alloc17h", "__smack_rust_std_alloc"},
+      {"_ZN5alloc5alloc12alloc_zeroed17h", "__smack_rust_std_alloc_zeroed"},
+      {"_ZN5alloc5alloc7dealloc17h", "__smack_rust_std_dealloc"},
+      {"_ZN5alloc5alloc7realloc17h", "__smack_rust_std_realloc"},
+      {"__rust_alloc", "__smack_rust_prim_alloc"},
+      {"__rust_alloc_zeroed", "__smack_rust_prim_alloc_zeroed"},
+      {"__rust_dealloc", "__smack_rust_prim_dealloc"},
+      {"__rust_realloc", "__smack_rust_prim_realloc"},
+  };
+
+  for (inst_iterator I = inst_begin(f), E = inst_end(f); I != E; ++I) {
+    if (auto ci = dyn_cast<CallInst>(&*I)) {
+      if (Function *f = ci->getCalledFunction()) {
+        auto name = f->hasName() ? f->getName() : "";
+        for (auto &kv : alloc_fns) {
+          if (isRustNameMatch(std::get<0>(kv), name)) {
+            Function *replacement =
+                f->getParent()->getFunction(std::get<1>(kv));
+            assert(replacement != NULL && "Function should be present.");
+            changed = true;
+            ci->setCalledFunction(replacement);
+          }
+        }
+      }
+    }
+  }
+  return changed;
+}
+
 /*
 The main function of rust programs looks like this:
 ...
@@ -30,15 +70,18 @@ This patches the main function to:
 %r = 0
 call void @real_main(...)
 ...
+
+Returns true if this is a Rust program entry point, false
+otherwise.
 */
-void fixEntry(Function &main) {
+bool fixEntry(Function &main) {
   std::vector<Instruction *> instToErase;
 
   for (inst_iterator I = inst_begin(main), E = inst_end(main); I != E; ++I) {
     if (auto ci = dyn_cast<CallInst>(&*I)) {
       if (Function *f = ci->getCalledFunction()) {
-        std::string name = f->hasName() ? f->getName() : "";
-        if (name.find(Naming::RUST_ENTRY) != std::string::npos) {
+        StringRef name = f->hasName() ? f->getName() : "";
+        if (name.find(Naming::RUST_ENTRY) != StringRef::npos) {
           // Get real Rust main
           auto castExpr = ci->getArgOperand(0);
           auto mainFunction = cast<Function>(castExpr);
@@ -64,31 +107,30 @@ void fixEntry(Function &main) {
   for (auto I : instToErase) {
     I->eraseFromParent();
   }
+
+  return instToErase.size();
 }
 
-bool RustFixes::runOnModule(Module &m) {
-  std::set<Function *> funcToErase;
-
-  for (auto &F : m) {
-    if (F.hasName()) {
-      auto name = F.getName();
-      if (Naming::isSmackName(name))
-        continue;
-      if (name == "main") {
-        fixEntry(F);
-      } else if (name.find(Naming::RUST_LANG_START_INTERNAL) !=
-                     std::string::npos ||
-                 name.find(Naming::RUST_ENTRY) != std::string::npos) {
-        funcToErase.insert(&F);
-      }
+bool RustFixes::runOnFunction(Function &F) {
+  bool result = false;
+  if (F.hasName()) {
+    StringRef name = F.getName();
+    if (Naming::isSmackName(name)) {
+      return false;
+    } else if (name.find(Naming::RUST_LANG_START_INTERNAL) != StringRef::npos ||
+               name.find(Naming::RUST_ENTRY) != StringRef::npos ||
+               Naming::isRustPanic(name)) {
+      F.dropAllReferences();
+      return true;
     }
-  }
 
-  for (auto F : funcToErase) {
-    F->dropAllReferences();
+    if (name == "main") {
+      result |= fixEntry(F);
+    }
+    result |= replaceRustMemoryFunctions(F);
   }
 
-  return true;
+  return result;
 }
 
 // Pass ID variable
diff --git a/lib/smack/SimplifyLibCalls.cpp b/lib/smack/SimplifyLibCalls.cpp
index 8400fc13e..d22675796 100644
--- a/lib/smack/SimplifyLibCalls.cpp
+++ b/lib/smack/SimplifyLibCalls.cpp
@@ -12,6 +12,7 @@
 #include "llvm/Analysis/OptimizationRemarkEmitter.h"
 #include "llvm/Analysis/ProfileSummaryInfo.h"
 #include "llvm/Analysis/TargetLibraryInfo.h"
+#include "llvm/IR/IRBuilder.h"
 #include "llvm/Transforms/Utils/BasicBlockUtils.h"
 
 #include <map>
@@ -42,9 +43,11 @@ bool SimplifyLibCalls::runOnFunction(Function &F) {
 }
 
 void SimplifyLibCalls::visitCallInst(CallInst &I) {
-  if (I.getCalledFunction())
-    if (simplifier->optimizeCall(&I))
+  if (I.getCalledFunction()) {
+    IRBuilder<> B(I.getContext());
+    if (simplifier->optimizeCall(&I, B))
       I.eraseFromParent();
+  }
 }
 
 // Pass ID variable
diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp
index fd9c650bd..4ae9e1ce5 100644
--- a/lib/smack/SmackInstGenerator.cpp
+++ b/lib/smack/SmackInstGenerator.cpp
@@ -117,7 +117,7 @@ void SmackInstGenerator::annotate(llvm::Instruction &I, Block *B) {
 
   //  for(auto II = MDForInst.begin(), EE = MDForInst.end(); II !=EE; ++II) {
   for (auto II : MDForInst) {
-    std::string name = Names[II.first];
+    StringRef name = Names[II.first];
     if (name.find("smack.") == 0 || name.find("verifier.") == 0) {
       std::list<const Expr *> attrs;
       for (auto AI = II.second->op_begin(), AE = II.second->op_end(); AI != AE;
@@ -127,27 +127,16 @@ void SmackInstGenerator::annotate(llvm::Instruction &I, Block *B) {
           attrs.push_back(Expr::lit((long long)value));
         } else if (auto *CI = dyn_cast<MDString>(*AI)) {
           auto value = CI->getString();
-          attrs.push_back(Expr::lit(value));
+          attrs.push_back(Expr::lit(value.str()));
         } else {
           llvm_unreachable("unexpected attribute type in smack metadata");
         }
       }
-      B->addStmt(Stmt::annot(Attr::attr(name, attrs)));
+      B->addStmt(Stmt::annot(Attr::attr(name.str(), attrs)));
     }
   }
 }
 
-bool isRustPanic(const std::string &name) {
-  for (const auto &panic : Naming::RUST_PANICS) {
-    // We are interested in exact functional matches.
-    // Rust mangled names include a 17 byte hash at the end.
-    if (name.find(panic) == 0 && name.size() == panic.size() + 17) {
-      return true;
-    }
-  }
-  return false;
-}
-
 void SmackInstGenerator::processInstruction(llvm::Instruction &inst) {
   SDEBUG(errs() << "Inst: " << inst << "\n");
   annotate(inst, currBlock);
@@ -316,13 +305,11 @@ void SmackInstGenerator::visitSwitchInst(llvm::SwitchInst &si) {
 void SmackInstGenerator::visitInvokeInst(llvm::InvokeInst &ii) {
   processInstruction(ii);
   llvm::Function *f = ii.getCalledFunction();
-  if (f) {
+  if (f)
     emit(rep->call(f, ii));
-  } else {
-    // llvm_unreachable("Unexpected invoke instruction.");
-    SmackWarnings::warnUnsound("invoke instruction", currBlock, &ii,
-                               ii.getType()->isVoidTy());
-  }
+  else
+    llvm_unreachable("Unexpected invoke instruction.");
+
   std::vector<std::pair<const Expr *, llvm::BasicBlock *>> targets;
   targets.push_back(
       {Expr::not_(Expr::id(Naming::EXN_VAR)), ii.getNormalDest()});
@@ -352,13 +339,13 @@ void SmackInstGenerator::visitUnreachableInst(llvm::UnreachableInst &ii) {
 void SmackInstGenerator::visitBinaryOperator(llvm::BinaryOperator &I) {
   processInstruction(I);
   if (rep->isBitwiseOp(&I) && I.getType()->getIntegerBitWidth() > 1)
-    SmackWarnings::warnIfUnsound(std::string("bitwise operation ") +
-                                     I.getOpcodeName(),
-                                 SmackOptions::BitPrecise, currBlock, &I);
+    SmackWarnings::warnIfIncomplete(std::string("bitwise operation ") +
+                                        I.getOpcodeName(),
+                                    {&SmackOptions::BitPrecise}, currBlock, &I);
   if (rep->isFpArithOp(&I))
-    SmackWarnings::warnIfUnsound(std::string("floating-point arithmetic ") +
-                                     I.getOpcodeName(),
-                                 SmackOptions::FloatEnabled, currBlock, &I);
+    SmackWarnings::warnIfIncomplete(
+        std::string("floating-point arithmetic ") + I.getOpcodeName(),
+        {&SmackOptions::FloatEnabled}, currBlock, &I);
 
   const Expr *E;
   if (isa<VectorType>(I.getType())) {
@@ -380,9 +367,9 @@ void SmackInstGenerator::visitUnaryOperator(llvm::UnaryOperator &I) {
   assert(I.getOpcode() == Instruction::FNeg && !isa<VectorType>(I.getType()) &&
          "Unsupported unary operation!");
   processInstruction(I);
-  SmackWarnings::warnIfUnsound(std::string("floating-point arithmetic ") +
-                                   I.getOpcodeName(),
-                               SmackOptions::FloatEnabled, currBlock, &I);
+  SmackWarnings::warnIfIncomplete(std::string("floating-point arithmetic ") +
+                                      I.getOpcodeName(),
+                                  {&SmackOptions::FloatEnabled}, currBlock, &I);
   emit(Stmt::assign(rep->expr(&I), rep->uop(&I)));
 }
 
@@ -647,42 +634,41 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst &ci) {
   processInstruction(ci);
 
   if (ci.isInlineAsm()) {
-    SmackWarnings::warnUnsound("inline asm call " + i2s(ci), currBlock, &ci,
-                               ci.getType()->isVoidTy());
+    SmackWarnings::warnUnModeled("inline asm call " + i2s(ci), currBlock, &ci);
     emit(Stmt::skip());
     return;
   }
 
   Function *f = ci.getCalledFunction();
   if (!f) {
-    assert(ci.getCalledValue() && "Called value is null");
-    f = cast<Function>(ci.getCalledValue()->stripPointerCastsAndAliases());
+    assert(ci.getCalledOperand() && "Called value is null");
+    f = cast<Function>(ci.getCalledOperand()->stripPointerCastsAndAliases());
   }
 
-  std::string name = f->hasName() ? f->getName() : "";
+  StringRef name = f->hasName() ? f->getName() : "";
 
-  if (SmackOptions::RustPanics && isRustPanic(name)) {
+  if (SmackOptions::RustPanics && Naming::isRustPanic(name)) {
     // Convert Rust's panic functions into assertion violations
     emit(Stmt::assert_(Expr::lit(false),
                        {Attr::attr(Naming::RUST_PANIC_ANNOTATION)}));
 
-  } else if (name.find(Naming::VALUE_PROC) != std::string::npos) {
+  } else if (name.find(Naming::VALUE_PROC) != StringRef::npos) {
     emit(rep->valueAnnotation(ci));
 
-  } else if (name.find(Naming::RETURN_VALUE_PROC) != std::string::npos) {
+  } else if (name.find(Naming::RETURN_VALUE_PROC) != StringRef::npos) {
     emit(rep->returnValueAnnotation(ci));
 
-  } else if (name.find(Naming::MOD_PROC) != std::string::npos) {
+  } else if (name.find(Naming::MOD_PROC) != StringRef::npos) {
     proc->getModifies().push_back(rep->code(ci));
 
-  } else if (name.find(Naming::CODE_PROC) != std::string::npos) {
+  } else if (name.find(Naming::CODE_PROC) != StringRef::npos) {
     emit(Stmt::code(rep->code(ci)));
 
-  } else if (name.find(Naming::DECL_PROC) != std::string::npos) {
+  } else if (name.find(Naming::DECL_PROC) != StringRef::npos) {
     std::string code = rep->code(ci);
     proc->getDeclarations().push_back(Decl::code(code, code));
 
-  } else if (name.find(Naming::TOP_DECL_PROC) != std::string::npos) {
+  } else if (name.find(Naming::TOP_DECL_PROC) != StringRef::npos) {
     std::string decl = rep->code(ci);
     rep->getProgram()->getDeclarations().push_back(Decl::code(decl, decl));
     if (VAR_DECL.match(decl)) {
@@ -748,7 +734,7 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst &ci) {
       args.push_back(rep->expr(V));
     for (auto m : rep->memoryMaps())
       args.push_back(Expr::id(m.first));
-    auto E = Expr::fn(F->getName(), args);
+    auto E = Expr::fn(F->getName().str(), args);
     if (name == Naming::CONTRACT_REQUIRES)
       proc->getRequires().push_back(E);
     else if (name == Naming::CONTRACT_ENSURES)
@@ -825,8 +811,8 @@ void SmackInstGenerator::visitCallInst(llvm::CallInst &ci) {
 
 void SmackInstGenerator::visitCallBrInst(llvm::CallBrInst &cbi) {
   processInstruction(cbi);
-  SmackWarnings::warnUnsound("callbr instruction " + i2s(cbi), currBlock, &cbi,
-                             cbi.getType()->isVoidTy());
+  SmackWarnings::warnUnModeled("callbr instruction " + i2s(cbi), currBlock,
+                               &cbi);
   emit(Stmt::skip());
 }
 
@@ -876,7 +862,7 @@ void SmackInstGenerator::visitLandingPadInst(llvm::LandingPadInst &lpi) {
   emit(Stmt::assign(rep->expr(&lpi), Expr::id(Naming::EXN_VAL_VAR)));
   if (lpi.isCleanup())
     emit(Stmt::assign(Expr::id(Naming::EXN_VAR), Expr::lit(false)));
-  SmackWarnings::warnUnsound("landingpad clauses", currBlock, &lpi, true);
+  SmackWarnings::warnUnModeled("landingpad clauses", currBlock, &lpi);
 }
 
 /******************************************************************************/
@@ -893,12 +879,6 @@ void SmackInstGenerator::visitMemSetInst(llvm::MemSetInst &msi) {
   emit(rep->memset(msi));
 }
 
-void SmackInstGenerator::generateUnModeledCall(llvm::CallInst *ci) {
-  SmackWarnings::warnUnsound(ci->getCalledFunction()->getName(), currBlock, ci,
-                             ci->getType()->isVoidTy());
-  emit(rep->call(ci->getCalledFunction(), *ci));
-}
-
 void SmackInstGenerator::visitIntrinsicInst(llvm::IntrinsicInst &ii) {
   processInstruction(ii);
 
@@ -914,9 +894,9 @@ void SmackInstGenerator::visitIntrinsicInst(llvm::IntrinsicInst &ii) {
           if (satisfied)
             modelGenFunc(ci);
           else {
-            SmackWarnings::warnUnsound(
+            SmackWarnings::warnIfIncomplete(
                 "call to " + ci->getCalledFunction()->getName().str(),
-                unsetFlags, currBlock, ci, false, rel);
+                unsetFlags, currBlock, ci, rel);
             emit(rep->call(ci->getCalledFunction(), *ci));
           }
         };
@@ -1229,8 +1209,11 @@ void SmackInstGenerator::visitIntrinsicInst(llvm::IntrinsicInst &ii) {
   auto it = stmtMap.find(ii.getIntrinsicID());
   if (it != stmtMap.end())
     it->second(&ii);
-  else
-    generateUnModeledCall(&ii);
+  else {
+    SmackWarnings::warnUnModeled(ii.getCalledFunction()->getName().str(),
+                                 currBlock, &ii);
+    emit(rep->call(ii.getCalledFunction(), ii));
+  }
 }
 
 } // namespace smack
diff --git a/lib/smack/SmackOptions.cpp b/lib/smack/SmackOptions.cpp
index 22f5f7a00..a6455d87f 100644
--- a/lib/smack/SmackOptions.cpp
+++ b/lib/smack/SmackOptions.cpp
@@ -14,14 +14,14 @@ const llvm::cl::list<std::string>
 
 const llvm::cl::opt<SmackWarnings::WarningLevel> SmackOptions::WarningLevel(
     "warn-type", llvm::cl::desc("Enable certain type of warning messages."),
-    llvm::cl::values(
-        clEnumValN(SmackWarnings::WarningLevel::Silent, "silent",
-                   "No warning messages"),
-        clEnumValN(SmackWarnings::WarningLevel::Unsound, "unsound",
-                   "Enable warnings about unsoundness"),
-        clEnumValN(
-            SmackWarnings::WarningLevel::Info, "info",
-            "Enable warnings about unsoundness and translation information")));
+    llvm::cl::values(clEnumValN(SmackWarnings::WarningLevel::Silent, "silent",
+                                "No warning messages"),
+                     clEnumValN(SmackWarnings::WarningLevel::Imprecise,
+                                "imprecise",
+                                "Enable warnings about imprecise modeling"),
+                     clEnumValN(SmackWarnings::WarningLevel::Info, "info",
+                                "Enable warnings about imprecise modeling and "
+                                "translation information")));
 
 const llvm::cl::opt<bool> SmackOptions::ColoredWarnings(
     "colored-warnings", llvm::cl::desc("Enable colored warning messages."));
@@ -91,7 +91,7 @@ const llvm::cl::opt<bool> SmackOptions::WrappedIntegerEncoding(
     llvm::cl::desc(
         "Enable wrapped integer arithmetic and signedness-aware comparison"));
 
-bool SmackOptions::isEntryPoint(std::string name) {
+bool SmackOptions::isEntryPoint(llvm::StringRef name) {
   for (auto EP : EntryPoints)
     if (name == EP)
       return true;
diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp
index 451ee725c..97cfbc754 100644
--- a/lib/smack/SmackRep.cpp
+++ b/lib/smack/SmackRep.cpp
@@ -130,7 +130,7 @@ std::string SmackRep::getString(const llvm::Value *v) {
         if (const llvm::ConstantDataSequential *cds =
                 llvm::dyn_cast<const llvm::ConstantDataSequential>(
                     cc->getOperand(0)))
-          return cds->getAsCString();
+          return cds->getAsCString().str();
   return "";
 }
 
@@ -857,8 +857,8 @@ const Expr *SmackRep::expr(const llvm::Value *v, bool isConstIntUnsigned,
     }
 
   } else if (isa<InlineAsm>(v)) {
-    SmackWarnings::warnUnsound("inline asm passed as argument", nullptr,
-                               nullptr);
+    SmackWarnings::warnUnModeled("inline asm passed as argument", nullptr,
+                                 nullptr);
     return pointerLit(0ULL);
 
   } else {
diff --git a/lib/smack/SmackWarnings.cpp b/lib/smack/SmackWarnings.cpp
index a6c22243e..8c08181b8 100644
--- a/lib/smack/SmackWarnings.cpp
+++ b/lib/smack/SmackWarnings.cpp
@@ -54,29 +54,32 @@ std::string SmackWarnings::getFlagStr(UnsetFlagsT flags) {
   return ret + "}";
 }
 
-void SmackWarnings::warnIfUnsound(std::string name,
-                                  RequiredFlagsT requiredFlags,
-                                  Block *currBlock, const Instruction *i,
-                                  bool ignore, FlagRelation rel) {
-  if (!isSatisfied(requiredFlags, rel))
-    warnUnsound(name, getUnsetFlags(requiredFlags), currBlock, i, ignore);
+void SmackWarnings::warnUnModeled(std::string unmodeledOpName, Block *currBlock,
+                                  const Instruction *i) {
+  warnImprecise("unmodeled operation " + unmodeledOpName, "", {}, currBlock, i);
 }
 
-void SmackWarnings::warnUnsound(std::string unmodeledOpName, Block *currBlock,
-                                const Instruction *i, bool ignore,
-                                FlagRelation rel) {
-  warnUnsound("unmodeled operation " + unmodeledOpName, UnsetFlagsT(),
-              currBlock, i, ignore, rel);
+void SmackWarnings::warnIfIncomplete(std::string name, UnsetFlagsT unsetFlags,
+                                     Block *currBlock, const Instruction *i,
+                                     FlagRelation rel) {
+  warnImprecise(name, "over-approximating", unsetFlags, currBlock, i, rel);
+}
+
+void SmackWarnings::warnIfIncomplete(std::string name,
+                                     RequiredFlagsT requiredFlags,
+                                     Block *currBlock, const Instruction *i,
+                                     FlagRelation rel) {
+  if (!isSatisfied(requiredFlags, rel))
+    warnIfIncomplete(name, getUnsetFlags(requiredFlags), currBlock, i, rel);
 }
 
-void SmackWarnings::warnUnsound(std::string name, UnsetFlagsT unsetFlags,
-                                Block *currBlock, const Instruction *i,
-                                bool ignore, FlagRelation rel) {
-  if (!isSufficientWarningLevel(WarningLevel::Unsound))
+void SmackWarnings::warnImprecise(std::string name, std::string description,
+                                  UnsetFlagsT unsetFlags, Block *currBlock,
+                                  const Instruction *i, FlagRelation rel) {
+  if (!isSufficientWarningLevel(WarningLevel::Imprecise))
     return;
   std::string beginning = std::string("llvm2bpl: ") + buildDebugInfo(i);
-  std::string end =
-      (ignore ? "unsoundly ignoring " : "over-approximating ") + name + ";";
+  std::string end = description + " " + name + ";";
   if (currBlock)
     currBlock->addStmt(Stmt::comment(beginning + "warning: " + end));
   std::string hint = "";
@@ -91,19 +94,6 @@ void SmackWarnings::warnUnsound(std::string name, UnsetFlagsT unsetFlags,
       << end << hint << "\n";
 }
 
-void SmackWarnings::warnIfUnsound(std::string name, FlagT &requiredFlag,
-                                  Block *currBlock, const Instruction *i,
-                                  FlagRelation rel) {
-  warnIfUnsound(name, {&requiredFlag}, currBlock, i, false, rel);
-}
-
-void SmackWarnings::warnIfUnsound(std::string name, FlagT &requiredFlag1,
-                                  FlagT &requiredFlag2, Block *currBlock,
-                                  const Instruction *i, FlagRelation rel) {
-  warnIfUnsound(name, {&requiredFlag1, &requiredFlag2}, currBlock, i, false,
-                rel);
-}
-
 void SmackWarnings::warnInfo(std::string info) {
   if (!isSufficientWarningLevel(WarningLevel::Info))
     return;
diff --git a/lib/smack/SplitAggregateValue.cpp b/lib/smack/SplitAggregateValue.cpp
index 0c27514f9..6004944bf 100644
--- a/lib/smack/SplitAggregateValue.cpp
+++ b/lib/smack/SplitAggregateValue.cpp
@@ -33,7 +33,8 @@ bool SplitAggregateValue::runOnFunction(Function &F) {
         if (li->getType()->isAggregateType()) {
           visitAggregateValue(nullptr, li->getType(), idx, info, C);
           IRBuilder<> irb(li);
-          li->replaceAllUsesWith(splitAggregateLoad(li, info, irb));
+          li->replaceAllUsesWith(splitAggregateLoad(
+              li->getType(), li->getPointerOperand(), info, irb));
           toRemove.push_back(li);
         }
       } else if (StoreInst *si = dyn_cast<StoreInst>(&I)) {
@@ -42,7 +43,8 @@ bool SplitAggregateValue::runOnFunction(Function &F) {
           visitAggregateValue(dyn_cast_or_null<Constant>(V), V->getType(), idx,
                               info, C);
           IRBuilder<> irb(si);
-          splitAggregateStore(si, info, irb);
+          splitAggregateStore(si->getPointerOperand(), si->getValueOperand(),
+                              info, irb);
           toRemove.push_back(si);
         }
       } else if (ReturnInst *ri = dyn_cast<ReturnInst>(&I)) {
@@ -80,11 +82,10 @@ bool SplitAggregateValue::isConstantAggregate(Value *V) {
     return false;
 }
 
-Value *SplitAggregateValue::splitAggregateLoad(LoadInst *li,
+Value *SplitAggregateValue::splitAggregateLoad(Type *T, Value *P,
                                                std::vector<InfoT> &info,
                                                IRBuilder<> &irb) {
-  Value *V = UndefValue::get(li->getType());
-  Value *P = li->getPointerOperand();
+  Value *V = UndefValue::get(T);
   for (auto &e : info) {
     IndexT idxs = std::get<0>(e);
     V = irb.CreateInsertValue(
@@ -94,11 +95,9 @@ Value *SplitAggregateValue::splitAggregateLoad(LoadInst *li,
   return V;
 }
 
-void SplitAggregateValue::splitAggregateStore(StoreInst *si,
+void SplitAggregateValue::splitAggregateStore(Value *P, Value *V,
                                               std::vector<InfoT> &info,
                                               IRBuilder<> &irb) {
-  Value *P = si->getPointerOperand();
-  Value *V = si->getValueOperand();
   for (auto &e : info) {
     IndexT idxs = std::get<0>(e);
     Constant *c = std::get<1>(e);
@@ -116,10 +115,8 @@ Value *SplitAggregateValue::createInsertedValue(IRBuilder<> &irb, Type *T,
                                                 std::vector<InfoT> &info,
                                                 Value *V) {
   Value *box = irb.CreateAlloca(T);
-  StoreInst *si = new StoreInst(V, box);
-  LoadInst *li = new LoadInst(box);
-  splitAggregateStore(si, info, irb);
-  return splitAggregateLoad(li, info, irb);
+  splitAggregateStore(box, V, info, irb);
+  return splitAggregateLoad(T, box, info, irb);
 }
 
 void SplitAggregateValue::splitConstantReturn(ReturnInst *ri,
diff --git a/lib/utils/Devirt.cpp b/lib/utils/Devirt.cpp
index 5be7fe530..90b3e407e 100644
--- a/lib/utils/Devirt.cpp
+++ b/lib/utils/Devirt.cpp
@@ -91,12 +91,12 @@ static inline bool isZExtOrBitCastable(Value* V, Type* T) {
   }
 }
 
-static inline bool match(CallSite &CS, const Function &F) {
-  auto N = CS.arg_size();
+static inline bool match(CallBase *CS, const Function &F) {
+  auto N = CS->arg_size();
   auto T = F.getFunctionType();
   auto M = T->getNumParams();
   auto RT = T->getReturnType();
-  auto IT = CS.getInstruction()->getType();
+  auto IT = CS->getType();
 
   if (RT != IT && !CastInst::isBitCastable(RT, IT))
     return false;
@@ -108,7 +108,7 @@ static inline bool match(CallSite &CS, const Function &F) {
     return false;
 
   for (unsigned i=0; i<M; i++) {
-    auto A = CS.getArgument(i);
+    auto A = CS->getArgOperand(i);
     auto PT = T->getParamType(i);
     if (A->getType() != PT && !isZExtOrBitCastable(A, PT))
       return false;
@@ -117,8 +117,8 @@ static inline bool match(CallSite &CS, const Function &F) {
   return true;
 }
 
-static inline bool checkArgs(const CallSite &CS, const Function *F) {
-  auto N = CS.arg_size();
+static inline bool checkArgs(const CallBase *CS, const Function *F) {
+  auto N = CS->arg_size();
   auto T = F->getFunctionType();
   auto M = T->getNumParams();
 
@@ -126,7 +126,7 @@ static inline bool checkArgs(const CallSite &CS, const Function *F) {
     return false;
 
   for (unsigned i=0; i<N; i++) {
-    auto A = CS.getArgument(i);
+    auto A = CS->getArgOperand(i);
     auto PT = T->getParamType(i+1);
     if (A->getType() != PT && !isZExtOrBitCastable(A, PT))
       return false;
@@ -147,7 +147,7 @@ static inline bool checkArgs(const CallSite &CS, const Function *F) {
 //  returned.
 //
 const Function *
-Devirtualize::findInCache (const CallSite & CS,
+Devirtualize::findInCache (const CallBase *CS,
                            std::set<const Function*>& Targets) {
   //
   // Iterate through all of the existing bounce functions to see if one of them
@@ -162,13 +162,13 @@ Devirtualize::findInCache (const CallSite & CS,
     const Function * bounceFunc = I->first;
 
     // Check the return type
-    if (CS.getType() != bounceFunc->getReturnType())
+    if (CS->getType() != bounceFunc->getReturnType())
       continue;
 
     // Check the type of the function pointer and the argumentsa
     PointerType* PT = dyn_cast<PointerType>(bounceFunc->arg_begin()->getType());
     assert(PT);
-    if (CS.getCalledValue()->stripPointerCastsAndAliases()->getType() != PT)
+    if (CS->getCalledOperand()->stripPointerCastsAndAliases()->getType() != PT)
       continue;
 
     FunctionType* FT = dyn_cast<FunctionType>(PT->getElementType());
@@ -200,7 +200,7 @@ Devirtualize::findInCache (const CallSite & CS,
 //  matches.
 //
 Function*
-Devirtualize::buildBounce (CallSite CS, std::vector<const Function*>& Targets) {
+Devirtualize::buildBounce (CallBase *CS, std::vector<const Function*>& Targets) {
   //
   // Update the statistics on the number of bounce functions added to the
   // module.
@@ -212,17 +212,17 @@ Devirtualize::buildBounce (CallSite CS, std::vector<const Function*>& Targets) {
   // an additional pointer argument at the beginning of its argument list that
   // will be the function to call.
   //
-  Value* ptr = CS.getCalledValue();
+  Value* ptr = CS->getCalledOperand();
   std::vector<Type *> TP;
   TP.insert (TP.begin(), ptr->getType());
-  for (CallSite::arg_iterator i = CS.arg_begin();
-       i != CS.arg_end();
+  for (auto i = CS->arg_begin();
+       i != CS->arg_end();
        ++i) {
     TP.push_back ((*i)->getType());
   }
 
-  FunctionType* NewTy = FunctionType::get(CS.getType(), TP, false);
-  Module * M = CS.getInstruction()->getParent()->getParent()->getParent();
+  FunctionType* NewTy = FunctionType::get(CS->getType(), TP, false);
+  Module * M = CS->getParent()->getParent()->getParent();
   Function* F = Function::Create (NewTy,
                                   GlobalValue::InternalLinkage,
                                   "devirtbounce",
@@ -269,7 +269,7 @@ Devirtualize::buildBounce (CallSite CS, std::vector<const Function*>& Targets) {
                                           BL);
 
     // Add the return instruction for the basic block
-    if (CS.getType()->isVoidTy())
+    if (CS->getType()->isVoidTy())
       ReturnInst::Create (M->getContext(), BL);
     else
       ReturnInst::Create (M->getContext(), directCall, BL);
@@ -362,7 +362,7 @@ Devirtualize::buildBounce (CallSite CS, std::vector<const Function*>& Targets) {
 //     already been acquired by the class.
 //
 void
-Devirtualize::makeDirectCall (CallSite & CS) {
+Devirtualize::makeDirectCall (CallBase *CS) {
   //
   // Find the targets of the indirect function call.
   //
@@ -371,12 +371,12 @@ Devirtualize::makeDirectCall (CallSite & CS) {
 
   // TODO should we allow non-matching targets?
   // TODO non-matching targets leads to crashes in bounce creation
-  if (CCG->isComplete(CS)) {
-    for (auto F = CCG->begin(CS); F != CCG->end(CS); ++F)
+  if (CCG->isComplete(*CS)) {
+    for (auto F = CCG->begin(*CS); F != CCG->end(*CS); ++F)
       if (match(CS, **F))
         Targets.push_back(*F);
   } else {
-    for (auto &F : *CS.getInstruction()->getParent()->getParent()->getParent())
+    for (auto &F : *CS->getParent()->getParent()->getParent())
       if (F.hasAddressTaken() && match(CS, F))
         Targets.push_back(&F);
   }
@@ -401,12 +401,12 @@ Devirtualize::makeDirectCall (CallSite & CS) {
   //
   // Replace the original call with a call to the bounce function.
   //
-  if (CallInst* CI = dyn_cast<CallInst>(CS.getInstruction())) {
+  if (CallInst* CI = dyn_cast<CallInst>(CS)) {
     std::vector<Value*> Params;
-    Params.push_back(CI->getCalledValue());
+    Params.push_back(CI->getCalledOperand());
     for (unsigned i=0; i<CI->getNumArgOperands(); i++) {
       Params.push_back(
-        castTo(CI->getArgOperand(i), NF->getFunctionType()->getParamType(i+1), "", CS.getInstruction())
+        castTo(CI->getArgOperand(i), NF->getFunctionType()->getParamType(i+1), "", CS)
       );
     }
 
@@ -417,12 +417,12 @@ Devirtualize::makeDirectCall (CallSite & CS) {
                                        CI);
     CI->replaceAllUsesWith(CN);
     CI->eraseFromParent();
-  } else if (InvokeInst* CI = dyn_cast<InvokeInst>(CS.getInstruction())) {
+  } else if (InvokeInst* CI = dyn_cast<InvokeInst>(CS)) {
     std::vector<Value*> Params;
-    Params.push_back(CI->getCalledValue());
+    Params.push_back(CI->getCalledOperand());
     for (unsigned i=0; i<CI->getNumArgOperands(); i++)
       Params.push_back(
-        castTo(CI->getArgOperand(i), NF->getFunctionType()->getParamType(i+1), "", CS.getInstruction())
+        castTo(CI->getArgOperand(i), NF->getFunctionType()->getParamType(i+1), "", CS)
       );
     std::string name = CI->hasName() ? CI->getName().str() + ".dv" : "";
     InvokeInst* CN = InvokeInst::Create(const_cast<Function*>(NF),
@@ -451,26 +451,25 @@ Devirtualize::makeDirectCall (CallSite & CS) {
 //  transformation into a direct call.
 //
 void
-Devirtualize::processCallSite (CallSite &CS) {
+Devirtualize::processCallSite (CallBase *CS) {
   //
   // First, determine if this is a direct call.  If so, then just ignore it.
   //
-  Value * CalledValue = CS.getCalledValue();
-  if (!CS.isIndirectCall())
+  if (!CS->isIndirectCall())
     return;
 
   //
   // Second, we will only transform those call sites which are complete (i.e.,
   // for which we know all of the call targets).
   //
-  if (SKIP_INCOMPLETE_NODES && !CCG->isComplete(CS))
+  if (SKIP_INCOMPLETE_NODES && !CCG->isComplete(*CS))
     return;
 
   //
   // This is an indirect call site.  Put it in the worklist of call sites to
   // transforms.
   //
-  Worklist.push_back (CS.getInstruction());
+  Worklist.push_back(CS);
   return;
 }
 
@@ -505,8 +504,7 @@ Devirtualize::runOnModule (Module & M) {
   //
   for (unsigned index = 0; index < Worklist.size(); ++index) {
     // Autobots, transform (the call site)!
-    CallSite CS (Worklist[index]);
-    makeDirectCall (CS);
+    makeDirectCall (Worklist[index]);
   }
 
   //
diff --git a/lib/utils/SimplifyExtractValue.cpp b/lib/utils/SimplifyExtractValue.cpp
index 8cf04ecf9..ea14e816b 100644
--- a/lib/utils/SimplifyExtractValue.cpp
+++ b/lib/utils/SimplifyExtractValue.cpp
@@ -136,7 +136,7 @@ bool SimplifyEV::runOnModule(Module& M) {
 
             GetElementPtrInst *GEP = GetElementPtrInst::CreateInBounds(LI->getOperand(0), Indices,
                                                                        LI->getName(), LI) ;
-            LoadInst *LINew = new LoadInst(GEP, "", LI);
+            LoadInst *LINew = new LoadInst(GEP->getResultElementType(), GEP, "", LI);
             EV->replaceAllUsesWith(LINew);
             EV->eraseFromParent();
             changed = true;
diff --git a/sea-dsa b/sea-dsa
index 77fa9ef09..e967981b4 160000
--- a/sea-dsa
+++ b/sea-dsa
@@ -1 +1 @@
-Subproject commit 77fa9ef0935aee4085a5ecdf52f67fcf2f87513b
+Subproject commit e967981b4600afeb5f0bc557fb1301ffa90da689
diff --git a/share/smack/frontend.py b/share/smack/frontend.py
index 417646c97..555703955 100644
--- a/share/smack/frontend.py
+++ b/share/smack/frontend.py
@@ -4,6 +4,7 @@
 import json
 from .utils import temporary_file, try_command, temporary_directory
 from .versions import RUST_VERSION
+from .versions import LLVM_SHORT_VERSION
 
 # Needed for cargo operations
 try:
@@ -85,8 +86,19 @@ def smack_lib():
     return os.path.join(smack_root(), 'share', 'smack', 'lib')
 
 
+def llvm_exact_bin(name):
+    return name + '-' + LLVM_SHORT_VERSION
+
+
 def default_clang_compile_command(args, lib=False):
-    cmd = ['clang', '-c', '-emit-llvm', '-O0', '-g', '-gcolumn-info']
+    cmd = [
+           llvm_exact_bin('clang'),
+           '-c',
+           '-emit-llvm',
+           '-O0',
+           '-g',
+           '-gcolumn-info'
+          ]
     # Starting from LLVM 5.0, we need the following two options
     # in order to enable optimization passes.
     # See: https://stackoverflow.com/a/46753969.
@@ -165,7 +177,7 @@ def fortran_compile_to_bc(input_file, compile_command, args):
          '-i',
          's/i32 1, !\"Debug Info Version\"/i32 2, !\"Debug Info Version\"/g',
          ll])
-    try_command(['llvm-as', ll])
+    try_command([llvm_exact_bin('llvm-as'), ll])
     try_command(['rm', ll])
     bc = '.'.join(ll.split('.')[:-1] + ['bc'])
     return bc
@@ -189,7 +201,7 @@ def clang_frontend(input_file, args):
 def clang_plusplus_frontend(input_file, args):
     """Generate LLVM IR from C++ language source(s)."""
     compile_command = default_clang_compile_command(args)
-    compile_command[0] = 'clang++'
+    compile_command[0] = llvm_exact_bin('clang++')
     return compile_to_bc(input_file, compile_command, args)
 
 
@@ -263,9 +275,17 @@ def json_compilation_database_frontend(input_file, args):
             if 'objects' in cc:
                 # TODO what to do when there are multiple linkings?
                 bit_codes = [re.sub('[.]o$', '.bc', f) for f in cc['objects']]
-                try_command(['llvm-link', '-o', args.bc_file] + bit_codes)
-                try_command(['llvm-link', '-o', args.linked_bc_file,
-                             args.bc_file] + default_build_libs(args))
+                try_command([
+                             llvm_exact_bin('llvm-link'),
+                             '-o',
+                             args.bc_file
+                            ] + bit_codes)
+                try_command([
+                             llvm_exact_bin('llvm-link'),
+                             '-o',
+                             args.linked_bc_file,
+                             args.bc_file
+                            ] + default_build_libs(args))
 
             else:
                 command = cc['command']
@@ -288,6 +308,16 @@ def default_cargo_compile_command(args):
 
 def cargo_frontend(input_file, args):
     """Generate LLVM bitcode from a cargo build."""
+
+    def find_target(config, options=None):
+        target_name = config['package']['name']
+        # TODO: Shaobo: target selection can be done via Cargo options.
+        # But we don't capture Cargo options for now.
+        if options is None:
+            if 'lib' in config and 'name' in config['lib']:
+                target_name = config['lib']['name']
+        return target_name.replace('-', '_')
+
     targetdir = temporary_directory(
         os.path.splitext(
             os.path.basename(input_file))[0],
@@ -300,7 +330,7 @@ def cargo_frontend(input_file, args):
     try_command(compile_command, console=True,
                 env={'RUSTFLAGS': " ".join(rustargs)})
 
-    crate_name = toml.load(input_file)['package']['name'].replace('-', '_')
+    target_name = find_target(toml.load(input_file))
 
     # Find the name of the crate's bc file
     bcbase = targetdir + '/debug/deps/'
@@ -308,7 +338,7 @@ def cargo_frontend(input_file, args):
     bcs = []
 
     for entry in entries:
-        if entry.startswith(crate_name + '-') and entry.endswith('.bc'):
+        if entry.startswith(target_name + '-') and entry.endswith('.bc'):
             bcs.append(bcbase + entry)
 
     bc_file = temporary_file(
@@ -316,7 +346,7 @@ def cargo_frontend(input_file, args):
             os.path.basename(input_file))[0],
         '.bc',
         args)
-    try_command(['llvm-link'] + bcs + ['-o', bc_file])
+    try_command([llvm_exact_bin('llvm-link')] + bcs + ['-o', bc_file])
     return bc_file
 
 
@@ -410,7 +440,7 @@ def cplusplus_build_libs(args):
     libs = ['smack.cpp']
 
     compile_command = default_clang_compile_command(args, True)
-    compile_command[0] = 'clang++'
+    compile_command[0] = llvm_exact_bin('clang++')
 
     for c in [os.path.join(smack_lib(), c) for c in libs]:
         bc = compile_to_bc(c, compile_command, args)
@@ -443,8 +473,8 @@ def link_bc_files(bitcodes, libs, args):
     for build_lib in libs:
         smack_libs += build_lib(args)
 
-    try_command(['llvm-link', '-o', args.bc_file] + bitcodes)
-    try_command(['llvm-link', '-o', args.linked_bc_file,
+    try_command([llvm_exact_bin('llvm-link'), '-o', args.bc_file] + bitcodes)
+    try_command([llvm_exact_bin('llvm-link'), '-o', args.linked_bc_file,
                  args.bc_file] + smack_libs)
 
     # import here to avoid a circular import
diff --git a/share/smack/include/math.h b/share/smack/include/math.h
index d49ee6d50..b51929b29 100644
--- a/share/smack/include/math.h
+++ b/share/smack/include/math.h
@@ -11,29 +11,29 @@
 #define FP_NORMAL 4
 
 #define isnormal(x)                                                            \
-  (sizeof(x) == sizeof(long double)                                            \
-       ? __isnormall(x)                                                        \
-       : sizeof(x) == sizeof(double) ? __isnormal(x) : __isnormalf(x))
+  (sizeof(x) == sizeof(long double) ? __isnormall(x)                           \
+   : sizeof(x) == sizeof(double)    ? __isnormal(x)                            \
+                                    : __isnormalf(x))
 #define isinf(x)                                                               \
-  (sizeof(x) == sizeof(long double)                                            \
-       ? __isinfl(x)                                                           \
-       : sizeof(x) == sizeof(double) ? __isinf(x) : __isinff(x))
+  (sizeof(x) == sizeof(long double) ? __isinfl(x)                              \
+   : sizeof(x) == sizeof(double)    ? __isinf(x)                               \
+                                    : __isinff(x))
 #define isnan(x)                                                               \
-  (sizeof(x) == sizeof(long double)                                            \
-       ? __isnanl(x)                                                           \
-       : sizeof(x) == sizeof(double) ? __isnan(x) : __isnanf(x))
+  (sizeof(x) == sizeof(long double) ? __isnanl(x)                              \
+   : sizeof(x) == sizeof(double)    ? __isnan(x)                               \
+                                    : __isnanf(x))
 #define signbit(x)                                                             \
-  (sizeof(x) == sizeof(long double)                                            \
-       ? __signbitl(x)                                                         \
-       : sizeof(x) == sizeof(double) ? __signbit(x) : __signbitf(x))
+  (sizeof(x) == sizeof(long double) ? __signbitl(x)                            \
+   : sizeof(x) == sizeof(double)    ? __signbit(x)                             \
+                                    : __signbitf(x))
 #define fpclassify(x)                                                          \
-  (sizeof(x) == sizeof(long double)                                            \
-       ? __fpclassifyl(x)                                                      \
-       : sizeof(x) == sizeof(double) ? __fpclassify(x) : __fpclassifyf(x))
+  (sizeof(x) == sizeof(long double) ? __fpclassifyl(x)                         \
+   : sizeof(x) == sizeof(double)    ? __fpclassify(x)                          \
+                                    : __fpclassifyf(x))
 #define isfinite(x)                                                            \
-  (sizeof(x) == sizeof(long double)                                            \
-       ? __finitel(x)                                                          \
-       : sizeof(x) == sizeof(double) ? __finite(x) : __finitef(x))
+  (sizeof(x) == sizeof(long double) ? __finitel(x)                             \
+   : sizeof(x) == sizeof(double)    ? __finite(x)                              \
+                                    : __finitef(x))
 
 typedef union {
   float f;
diff --git a/share/smack/lib/smack.rs b/share/smack/lib/smack.rs
index 06beb7a6d..da6c71734 100644
--- a/share/smack/lib/smack.rs
+++ b/share/smack/lib/smack.rs
@@ -1,5 +1,7 @@
 #![crate_type = "staticlib"]
 
+use std::alloc::Layout;
+
 #[cfg(verifier = "smack")]
 extern "C" {
     pub fn __VERIFIER_assert(x: i32);
@@ -17,6 +19,8 @@ extern "C" {
     pub fn malloc(size: usize) -> *mut u8;
     pub fn __VERIFIER_memcpy(dest: *mut u8, src: *mut u8, count: usize) -> *mut u8;
     pub fn free(ptr: *mut u8);
+    pub fn memset(ptr: *mut u8, ch: i32, count: usize);
+    pub fn realloc(ptr: *mut u8, new_size: usize) -> *mut u8;
 }
 
 #[macro_export]
@@ -144,6 +148,59 @@ make_verifier_nondet!(usize, __VERIFIER_nondet_u64);
 make_verifier_nondet!(f32, __VERIFIER_nondet_float);
 make_verifier_nondet!(f64, __VERIFIER_nondet_double);
 
+/* Rust memory function models. */
+#[no_mangle]
+pub unsafe fn __smack_rust_std_alloc(layout: Layout) -> *mut u8 {
+    __smack_rust_prim_alloc(layout.size(), layout.align())
+}
+
+#[no_mangle]
+pub unsafe fn __smack_rust_std_alloc_zeroed(layout: Layout) -> *mut u8 {
+    __smack_rust_prim_alloc(layout.size(), layout.align())
+}
+
+#[no_mangle]
+pub unsafe fn __smack_rust_std_dealloc(ptr: *mut u8, layout: Layout) {
+    __smack_rust_prim_dealloc(ptr, layout.size(), layout.align())
+}
+
+#[no_mangle]
+pub unsafe fn __smack_rust_std_realloc(ptr: *mut u8, layout: Layout, new_size: usize) -> *mut u8 {
+    __smack_rust_prim_realloc(ptr, layout.size(), layout.align(), new_size)
+}
+
+#[no_mangle]
+pub unsafe fn __smack_rust_prim_alloc(size: usize, _align: usize) -> *mut u8 {
+    // Currently ignores alignment
+    malloc(size)
+}
+
+#[no_mangle]
+pub unsafe fn __smack_rust_prim_alloc_zeroed(size: usize, _align: usize) -> *mut u8 {
+    // Currently ignores alignment
+    let result = malloc(size);
+    memset(result, 0, size);
+    result
+}
+
+#[no_mangle]
+pub unsafe fn __smack_rust_prim_dealloc(ptr: *mut u8, _size: usize, _align: usize) {
+    // Currently ignoring size and alignment
+    free(ptr);
+}
+
+#[no_mangle]
+pub unsafe fn __smack_rust_prim_realloc(
+    ptr: *mut u8,
+    _old_size: usize,
+    _align: usize,
+    new_size: usize,
+) -> *mut u8 {
+    // Needs proper implementation of realloc
+    // Ignores size and alignment
+    realloc(ptr, new_size)
+}
+
 #[cfg(not(verifier = "smack"))]
 #[cfg(feature = "std")]
 #[allow(dead_code)]
diff --git a/share/smack/reach.py b/share/smack/reach.py
index ccc21e531..c5e72341e 100755
--- a/share/smack/reach.py
+++ b/share/smack/reach.py
@@ -11,7 +11,7 @@
 from smackgen import *
 from smackverify import *
 
-VERSION = '2.6.3'
+VERSION = '2.7.0'
 
 
 def reachParser():
diff --git a/share/smack/top.py b/share/smack/top.py
index daca4fdb0..0d8626721 100755
--- a/share/smack/top.py
+++ b/share/smack/top.py
@@ -13,7 +13,7 @@
 from .frontend import link_bc_files, frontends, languages, extra_libs
 from .errtrace import error_trace, smackdOutput
 
-VERSION = '2.6.3'
+VERSION = '2.7.0'
 
 
 class VResult(Flag):
@@ -309,12 +309,12 @@ def arguments():
         type=str,
         help='limit debugging output to given MODULES')
 
-    noise_group.add_argument('--warn', default="unsound",
-                             choices=['silent', 'unsound', 'info'],
+    noise_group.add_argument('--warn', default="imprecise",
+                             choices=['silent', 'imprecise', 'info'],
                              help='''enable certain type of warning messages
             (silent: no warning messages;
-            unsound: warnings about unsoundness;
-            info: warnings about unsoundness and translation information)
+            unsound: warnings about imprecise modeling;
+            info: warnings about imprecise modeling/translation information)
             [default: %(default)s]''')
 
     parser.add_argument(
@@ -866,7 +866,7 @@ def verify_bpl(args):
     elif args.verifier == 'boogie' or args.modular:
         command = ["boogie"]
         command += [args.bpl_file]
-        command += ["/nologo", "/doModSetAnalysis"]
+        command += ["/doModSetAnalysis"]
         command += ["/useArrayTheory"]
         command += ["/timeLimit:%s" % args.time_limit]
         command += ["/errorLimit:%s" % args.max_violations]
diff --git a/share/smack/utils.py b/share/smack/utils.py
index fb16db72c..2467c5e72 100644
--- a/share/smack/utils.py
+++ b/share/smack/utils.py
@@ -71,7 +71,7 @@ def try_command(cmd, cwd=None, console=False, timeout=None, env=None):
                 line = proc.stdout.readline()
                 if line:
                     output += line
-                    print(line, end=' ')
+                    print(line, end='')
                 elif proc.poll() is not None:
                     break
             proc.wait
diff --git a/test/c/failing/floppy_false.i.cil.c b/test/c/failing/floppy_false.i.cil.c
index 9d57493ea..59443e964 100644
--- a/test/c/failing/floppy_false.i.cil.c
+++ b/test/c/failing/floppy_false.i.cil.c
@@ -2275,9 +2275,7 @@ NTSTATUS FloppyAddDevice(PDRIVER_OBJECT DriverObject,
                                                   &arcNameString, 1);
         }
         if (ntStatus >= 0L) {
-          {
-            IoCreateSymbolicLink(&disketteExtension->ArcName, &deviceName);
-          }
+          { IoCreateSymbolicLink(&disketteExtension->ArcName, &deviceName); }
         } else {
         }
         deviceObject->Flags |= 8208UL;
@@ -2912,8 +2910,7 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                                 if (irpSp->Parameters.DeviceIoControl
                                         .InputBufferLength <
                                     (ULONG)sizeof(FORMAT_PARAMETERS)) {
-                                  {
-                                  }
+                                  {}
                                   ntStatus = -1073741811L;
                                   goto switch_16_break;
                                 } else {
@@ -2999,8 +2996,7 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                                         .OutputBufferLength;
                                 if (outputBufferLength <
                                     (ULONG)sizeof(DISK_GEOMETRY)) {
-                                  {
-                                  }
+                                  {}
                                   ntStatus = -1073741789L;
                                   goto switch_16_break;
                                 } else {
@@ -3014,8 +3010,7 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                                                         (int)
                                                             lowestDriveMediaType) +
                                                        1))) {
-                                  {
-                                  }
+                                  {}
                                   ntStatus = -2147483643L;
                                   highestDriveMediaType =
                                       (enum _DRIVE_MEDIA_TYPE)(
@@ -3069,8 +3064,7 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                               switch_16_exp_10: /* CIL Label */;
                                 if ((int)((KUSER_SHARED_DATA *const)4292804608U)
                                         ->AlternativeArchitecture == 1) {
-                                  {
-                                  }
+                                  {}
                                   if (!(DeviceObject->Characteristics & 1UL)) {
                                     ntStatus = -1073741275L;
                                     goto switch_16_break;
@@ -3215,13 +3209,11 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                               switch_16_exp_11: /* CIL Label */;
                                 if ((int)((KUSER_SHARED_DATA *const)4292804608U)
                                         ->AlternativeArchitecture == 1) {
-                                  {
-                                  }
+                                  {}
                                   if (irpSp->Parameters.DeviceIoControl
                                           .OutputBufferLength <
                                       (ULONG)sizeof(SENSE_DEVISE_STATUS_PTOS)) {
-                                    {
-                                    }
+                                    {}
                                     ntStatus = -1073741811L;
                                     goto switch_16_break;
                                   } else {
@@ -3382,8 +3374,7 @@ NTSTATUS FloppyPnp(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                     switch_32_5: /* CIL Label */;
                     switch_32_1: /* CIL Label */;
                       if ((int)irpSp->MinorFunction == 5) {
-                        {
-                        }
+                        {}
                       } else {
                         {}
                       }
@@ -3454,8 +3445,7 @@ NTSTATUS FloppyPnp(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                     switch_32_6: /* CIL Label */;
                     switch_32_3: /* CIL Label */;
                       if ((int)irpSp->MinorFunction == 6) {
-                        {
-                        }
+                        {}
                       } else {
                         {}
                       }
@@ -3494,14 +3484,10 @@ NTSTATUS FloppyPnp(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                            * 1, 0); */ /* INLINED */
                         }
                         if (s != NP) {
-                          {
-                            errorFn();
-                          }
+                          { errorFn(); }
                         } else {
                           if (compRegistered != 0) {
-                            {
-                              errorFn();
-                            }
+                            { errorFn(); }
                           } else {
                             compRegistered = 1;
                             compFptr = &FloppyPnpComplete;
@@ -3696,14 +3682,10 @@ NTSTATUS FloppyStartDevice(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
       nextIrpSp->Control = 0;
     }
     if (s != NP) {
-      {
-        errorFn();
-      }
+      { errorFn(); }
     } else {
       if (compRegistered != 0) {
-        {
-          errorFn();
-        }
+        { errorFn(); }
       } else {
         compRegistered = 1;
         compFptr = &FloppyPnpComplete;
@@ -3738,9 +3720,7 @@ NTSTATUS FloppyStartDevice(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
       disketteExtension->MaxTransferSize = fdcInfo.MaxTransferSize;
       if (fdcInfo.AcpiBios) {
         if (fdcInfo.AcpiFdiSupported) {
-          {
-            ntStatus = FlAcpiConfigureFloppy(disketteExtension, &fdcInfo);
-          }
+          { ntStatus = FlAcpiConfigureFloppy(disketteExtension, &fdcInfo); }
           if ((int)disketteExtension->DriveType == 4) {
             disketteExtension->PerpendicularMode =
                 (int)disketteExtension->PerpendicularMode |
@@ -3775,8 +3755,7 @@ NTSTATUS FloppyStartDevice(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                   &FlConfigCallBack, disketteExtension);
             }
             if (ntStatus >= 0L) {
-              {
-              }
+              {}
               goto while_43_break;
             } else {
             }
@@ -3903,8 +3882,7 @@ NTSTATUS FloppyPower(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                  * disketteExtension->PowerDownMutex); */ /* INLINED */
               }
               if ((int)state.SystemState == 1) {
-                {
-                }
+                {}
                 disketteExtension->PoweringDown = 0;
                 WaitForCompletion = 0;
               } else {
@@ -4053,8 +4031,7 @@ NTSTATUS FlInterpretError(UCHAR StatusRegister1, UCHAR StatusRegister2) {
       }
     }
     if ((int)StatusRegister1 & 16) {
-      {
-      }
+      {}
       return (-1073741764L);
     } else {
     }
@@ -4083,20 +4060,17 @@ NTSTATUS FlInterpretError(UCHAR StatusRegister1, UCHAR StatusRegister2) {
       }
     }
     if ((int)StatusRegister1 & 2) {
-      {
-      }
+      {}
       return (-1073741662L);
     } else {
     }
     if ((int)StatusRegister1 & 1) {
-      {
-      }
+      {}
       return (-1073741467L);
     } else {
     }
     if ((int)StatusRegister2 & 16) {
-      {
-      }
+      {}
       return (-1073741466L);
     } else {
     }
@@ -4115,12 +4089,9 @@ void FlFinishOperation(PIRP Irp, PDISKETTE_EXTENSION DisketteExtension) {
         DisketteExtension->HardwareFailCount =
             (UCHAR)((int)DisketteExtension->HardwareFailCount + 1);
         if ((int)DisketteExtension->HardwareFailCount < 2) {
-          {
-            ntStatus = FlInitializeControllerHardware(DisketteExtension);
-          }
+          { ntStatus = FlInitializeControllerHardware(DisketteExtension); }
           if (ntStatus >= 0L) {
-            {
-            }
+            {}
             DisketteExtension->MediaType = -1;
             {} {
               /*           ExAcquireFastMutex(&
@@ -4186,8 +4157,7 @@ void FlFinishOperation(PIRP Irp, PDISKETTE_EXTENSION DisketteExtension) {
     if (myStatus != 0L) {
       if (myStatus != -2147483626L) {
         if (myStatus != -1073741805L) {
-          {
-          }
+          {}
         } else {
           goto _L___0;
         }
@@ -4289,8 +4259,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
                     DisketteExtension->FifoBuffer, (void *)0, 0, 0);
               }
               if (!(ntStatus >= 0L)) {
-                {
-                }
+                {}
                 return (ntStatus);
               } else {
               }
@@ -4300,8 +4269,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
                 driveStatus = 128;
               }
               if ((int)driveStatus & 128) {
-                {
-                }
+                {}
                 if ((int)((DisketteExtension->DeviceObject)->Vpb)->Flags & 1) {
                   (DisketteExtension->DeviceObject)->Flags &= 4294967293UL;
                 } else {
@@ -4320,8 +4288,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
                   DisketteExtension->FifoBuffer, (void *)0, 0, 0);
             }
             if (!(ntStatus >= 0L)) {
-              {
-              }
+              {}
               return (ntStatus);
             } else {
               if (!((int)DisketteExtension->FifoBuffer[0] & 32)) {
@@ -4351,8 +4318,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
               KeDelayExecutionThread(0, 0, &delay);
             }
             if (!(ntStatus >= 0L)) {
-              {
-              }
+              {}
               return (ntStatus);
             } else {
               if (!((int)DisketteExtension->FifoBuffer[0] & 32)) {
@@ -4378,8 +4344,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
                     DisketteExtension->FifoBuffer, (void *)0, 0, 0);
               }
               if (!(ntStatus >= 0L)) {
-                {
-                }
+                {}
                 return (ntStatus);
               } else {
               }
@@ -4401,8 +4366,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
               }
             }
             if ((int)driveStatus & 128) {
-              {
-              }
+              {}
               if ((int)((DisketteExtension->DeviceObject)->Vpb)->Flags & 1) {
                 (DisketteExtension->DeviceObject)->Flags &= 4294967293UL;
               } else {
@@ -4414,8 +4378,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
           }
           if ((int)IgnoreChange == 0) {
             if ((int)((DisketteExtension->DeviceObject)->Vpb)->Flags & 1) {
-              {
-              }
+              {}
               return (-2147483626L);
             } else {
               return (-1073741435L);
@@ -4429,32 +4392,24 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
       _L___2: /* CIL Label */
         if ((int)((KUSER_SHARED_DATA *const)4292804608U)
                 ->AlternativeArchitecture == 1) {
-          {
-            FlHdbit(DisketteExtension);
-          }
+          { FlHdbit(DisketteExtension); }
         } else {
         }
       }
     }
     if (SetUpMedia) {
       if ((int)DisketteExtension->MediaType == -1) {
-        {
-          ntStatus = FlDetermineMediaType(DisketteExtension);
-        }
+        { ntStatus = FlDetermineMediaType(DisketteExtension); }
       } else {
         if ((int)DisketteExtension->MediaType == 0) {
-          {
-          }
+          {}
           return (-1073741804L);
         } else {
           if ((int)DisketteExtension->DriveMediaType !=
               (int)DisketteExtension->LastDriveMediaType) {
-            {
-              ntStatus = FlDatarateSpecifyConfigure(DisketteExtension);
-            }
+            { ntStatus = FlDatarateSpecifyConfigure(DisketteExtension); }
             if (!(ntStatus >= 0L)) {
-              {
-              }
+              {}
             } else {
             }
           } else {
@@ -4473,24 +4428,21 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
                              DisketteExtension->FifoBuffer, (void *)0, 0, 0);
         }
         if (!(ntStatus >= 0L)) {
-          {
-          }
+          {}
           return (ntStatus);
         } else {
         }
         if ((int)((KUSER_SHARED_DATA *const)4292804608U)
                 ->AlternativeArchitecture == 1) {
           if (!((int)DisketteExtension->FifoBuffer[0] & 32)) {
-            {
-            }
+            {}
             return (-1073741805L);
           } else {
           }
         } else {
         }
         if ((int)DisketteExtension->FifoBuffer[0] & 64) {
-          {
-          }
+          {}
           return (-1073741662L);
         } else {
         }
@@ -4552,9 +4504,7 @@ NTSTATUS FlDatarateSpecifyConfigure(PDISKETTE_EXTENSION DisketteExtension) {
                 &DisketteExtension->DriveMediaConstants.DataTransferRate);
           }
           if (ntStatus >= 0L) {
-            {
-              ntStatus = FlRecalibrateDrive(DisketteExtension);
-            }
+            { ntStatus = FlRecalibrateDrive(DisketteExtension); }
           } else {
           }
         } else {
@@ -4591,8 +4541,7 @@ NTSTATUS FlRecalibrateDrive(PDISKETTE_EXTENSION DisketteExtension) {
                              DisketteExtension->FifoBuffer, (void *)0, 0, 0);
         }
         if (!(ntStatus >= 0L)) {
-          {
-          }
+          {}
         } else {
         }
         if (ntStatus >= 0L) {
@@ -4608,8 +4557,7 @@ NTSTATUS FlRecalibrateDrive(PDISKETTE_EXTENSION DisketteExtension) {
                   DisketteExtension->FifoBuffer, (void *)0, 0, 0);
             }
             if (!(ntStatus >= 0L)) {
-              {
-              }
+              {}
               return (ntStatus);
             } else {
             }
@@ -4698,8 +4646,7 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) {
             }
             { ntStatus = FlDatarateSpecifyConfigure(DisketteExtension); }
             if (!(ntStatus >= 0L)) {
-              {
-              }
+              {}
               mediaTypesExhausted = 1;
             } else {
               {
@@ -4831,8 +4778,7 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) {
                             /*                     ExFreePool(bootSector); */ /* INLINED */
                           }
                           if (!(ntStatus >= 0L)) {
-                            {
-                            }
+                            {}
                             DisketteExtension->DriveMediaType =
                                 (DRIVE_MEDIA_TYPE)(
                                     (int)DisketteExtension->DriveMediaType - 1);
@@ -4875,8 +4821,7 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) {
         while_101_break: /* CIL Label */;
         }
         if (ntStatus >= 0L) {
-          {
-          }
+          {}
           goto while_99_break;
         } else {
         }
@@ -5270,8 +5215,7 @@ void FloppyThread(PVOID Context) {
                         }
                         if ((disketteExtension->DeviceObject)->Flags & 2UL) {
                           if (!((int)irpSp->Flags & 2)) {
-                            {
-                            }
+                            {}
                             ntStatus = -2147483626L;
                           } else {
                             {
@@ -5303,8 +5247,7 @@ void FloppyThread(PVOID Context) {
                         }
                         if ((disketteExtension->DeviceObject)->Flags & 2UL) {
                           if (!((int)irpSp->Flags & 2)) {
-                            {
-                            }
+                            {}
                             ntStatus = -2147483626L;
                           } else {
                             goto _L___2;
@@ -5394,8 +5337,7 @@ void FloppyThread(PVOID Context) {
                                                   disketteExtension->MediaType;
                                               if ((int)disketteExtension
                                                       ->MediaType == 0) {
-                                                {
-                                                }
+                                                {}
                                                 outputBuffer->Cylinders
                                                     .__annonCompField1.LowPart =
                                                     0;
@@ -5559,9 +5501,7 @@ void FloppyThread(PVOID Context) {
             } else {
               irp->IoStatus.__annonCompField4.Status = ntStatus;
               if (disketteExtension->IoBuffer) {
-                {
-                  FlFreeIoBuffer(disketteExtension);
-                }
+                { FlFreeIoBuffer(disketteExtension); }
               } else {
               }
               { FlFinishOperation(irp, disketteExtension); }
@@ -5990,8 +5930,7 @@ NTSTATUS FlReadWriteTrack(PDISKETTE_EXTENSION DisketteExtension, PMDL IoMdl,
           }
         }
         if (!(status >= 0L)) {
-          {
-          }
+          {}
           recalibrateDrive = 1;
           goto __Cont;
         } else {
@@ -6075,8 +6014,7 @@ NTSTATUS FlReadWriteTrack(PDISKETTE_EXTENSION DisketteExtension, PMDL IoMdl,
             } else {
             }
             if (ioRetry >= 2UL) {
-              {
-              }
+              {}
               goto while_149_break;
             } else {
             }
@@ -6096,8 +6034,7 @@ NTSTATUS FlReadWriteTrack(PDISKETTE_EXTENSION DisketteExtension, PMDL IoMdl,
     }
     if (!(status >= 0L)) {
       if ((int)NumberOfSectors > 1) {
-        {
-        }
+        {}
         i = 0;
         {
           while (1) {
@@ -6115,8 +6052,7 @@ NTSTATUS FlReadWriteTrack(PDISKETTE_EXTENSION DisketteExtension, PMDL IoMdl,
                   (unsigned char)((int)Sector + (int)i), 1, 0);
             }
             if (!(status >= 0L)) {
-              {
-              }
+              {}
               DisketteExtension->HardwareFailed = 1;
               goto while_153_break;
             } else {
@@ -6163,8 +6099,7 @@ NTSTATUS FlReadWrite(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
     {}
     if ((int)irpSp->MajorFunction == 4) {
       if (DisketteExtension->IsReadOnly) {
-        {
-        }
+        {}
         return (-1073741811L);
       } else {
       }
@@ -6182,21 +6117,17 @@ NTSTATUS FlReadWrite(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
       }
     }
     if (!(status >= 0L)) {
-      {
-      }
+      {}
       return (status);
     } else {
     }
     if ((int)((KUSER_SHARED_DATA *const)4292804608U)->AlternativeArchitecture ==
         1) {
-      {
-        FlHdbit(DisketteExtension);
-      }
+      { FlHdbit(DisketteExtension); }
     } else {
     }
     if ((int)DisketteExtension->MediaType == 0) {
-      {
-      }
+      {}
       return (-1073741804L);
     } else {
     }
@@ -6219,8 +6150,7 @@ NTSTATUS FlReadWrite(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
       }
     }
     if ((unsigned int)userBuffer == (unsigned int)((void *)0)) {
-      {
-      }
+      {}
       return (-1073741670L);
     } else {
     }
@@ -6251,8 +6181,7 @@ NTSTATUS FlReadWrite(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
         if (trackSize > DisketteExtension->MaxTransferSize) {
           {} { FlAllocateIoBuffer(DisketteExtension, trackSize); }
           if (!DisketteExtension->IoBuffer) {
-            {
-            }
+            {}
             return (-1073741670L);
           } else {
           }
@@ -6431,15 +6360,11 @@ NTSTATUS FlFormat(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp) {
     {}
     if ((int)((KUSER_SHARED_DATA *const)4292804608U)->AlternativeArchitecture ==
         1) {
-      {
-        FlHdbit(DisketteExtension);
-      }
+      { FlHdbit(DisketteExtension); }
     } else {
     }
     if ((int)DisketteExtension->LastDriveMediaType != (int)driveMediaType) {
-      {
-        ntStatus = FlDatarateSpecifyConfigure(DisketteExtension);
-      }
+      { ntStatus = FlDatarateSpecifyConfigure(DisketteExtension); }
       if (!(ntStatus >= 0L)) {
         return (ntStatus);
       } else {
@@ -6500,8 +6425,7 @@ NTSTATUS FlFormat(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp) {
         } else {
         }
         if (!(ntStatus >= 0L)) {
-          {
-          }
+          {}
           return (ntStatus);
         } else {
         }
@@ -6558,8 +6482,7 @@ NTSTATUS FlFormat(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp) {
                   0, length);
             }
             if (!(ntStatus >= 0L)) {
-              {
-              }
+              {}
             } else {
             }
             if (ntStatus >= 0L) {
@@ -6609,8 +6532,7 @@ NTSTATUS FlFormat(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp) {
                   DisketteExtension->FifoBuffer, (void *)0, 0, 0);
             }
             if (!(ntStatus >= 0L)) {
-              {
-              }
+              {}
               return (ntStatus);
             } else {
             }
@@ -6821,8 +6743,7 @@ NTSTATUS FlFdcDeviceIo(PDEVICE_OBJECT DeviceObject, ULONG Ioctl, PVOID Data) {
                                         (void *)0, 0, 1, &doneEvent, &ioStatus);
     }
     if ((unsigned int)irp == (unsigned int)((void *)0)) {
-      {
-      }
+      {}
       return (-1073741670L);
     } else {
     }
@@ -7000,9 +6921,7 @@ NTSTATUS FlHdbit(PDISKETTE_EXTENSION DisketteExtension) {
     } else {
     }
     if (setHdBitParameter.ChangedHdBit) {
-      {
-        ntStatus = FlDatarateSpecifyConfigure(DisketteExtension);
-      }
+      { ntStatus = FlDatarateSpecifyConfigure(DisketteExtension); }
     } else {
     }
     return (ntStatus);
@@ -7376,9 +7295,7 @@ int main(void) {
         }
       }
       if (we_should_unload) {
-        {
-          FloppyUnload(&d);
-        }
+        { FloppyUnload(&d); }
       } else {
       }
     } else {
@@ -7408,9 +7325,7 @@ int main(void) {
             if (s != SKIP2) {
               if (s != IPC) {
                 if (s != DC) {
-                  {
-                    errorFn();
-                  }
+                  { errorFn(); }
                 } else {
                   goto _L___0;
                 }
@@ -7426,14 +7341,10 @@ int main(void) {
                 }
               } else {
                 if (s == DC) {
-                  {
-                    errorFn();
-                  }
+                  { errorFn(); }
                 } else {
                   if (status != (NTSTATUS)lowerDriverReturn) {
-                    {
-                      errorFn();
-                    }
+                    { errorFn(); }
                   } else {
                   }
                 }
@@ -7871,9 +7782,7 @@ NTSTATUS IofCallDriver(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
         compRetStatus1 = tmp;
       }
       if ((long)compRetStatus1 == -1073741802L) {
-        {
-          stubMoreProcessingRequired();
-        }
+        { stubMoreProcessingRequired(); }
       } else {
       }
     } else {
@@ -8027,9 +7936,7 @@ NTSTATUS KeWaitForSingleObject(PVOID Object, KWAIT_REASON WaitReason,
         customIrp = 0;
       } else {
         if (s == MPR3) {
-          {
-            errorFn();
-          }
+          { errorFn(); }
         } else {
         }
       }
@@ -8164,9 +8071,7 @@ NTSTATUS PoCallDriver(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
         compRetStatus = tmp;
       }
       if ((long)compRetStatus == -1073741802L) {
-        {
-          stubMoreProcessingRequired();
-        }
+        { stubMoreProcessingRequired(); }
       } else {
       }
     } else {
diff --git a/test/c/failing/floppy_true.i.cil.c b/test/c/failing/floppy_true.i.cil.c
index 67388109c..4b8b6a688 100644
--- a/test/c/failing/floppy_true.i.cil.c
+++ b/test/c/failing/floppy_true.i.cil.c
@@ -2275,9 +2275,7 @@ NTSTATUS FloppyAddDevice(PDRIVER_OBJECT DriverObject,
                                                   &arcNameString, 1);
         }
         if (ntStatus >= 0L) {
-          {
-            IoCreateSymbolicLink(&disketteExtension->ArcName, &deviceName);
-          }
+          { IoCreateSymbolicLink(&disketteExtension->ArcName, &deviceName); }
         } else {
         }
         deviceObject->Flags |= 8208UL;
@@ -2912,8 +2910,7 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                                 if (irpSp->Parameters.DeviceIoControl
                                         .InputBufferLength <
                                     (ULONG)sizeof(FORMAT_PARAMETERS)) {
-                                  {
-                                  }
+                                  {}
                                   ntStatus = -1073741811L;
                                   goto switch_16_break;
                                 } else {
@@ -2999,8 +2996,7 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                                         .OutputBufferLength;
                                 if (outputBufferLength <
                                     (ULONG)sizeof(DISK_GEOMETRY)) {
-                                  {
-                                  }
+                                  {}
                                   ntStatus = -1073741789L;
                                   goto switch_16_break;
                                 } else {
@@ -3014,8 +3010,7 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                                                         (int)
                                                             lowestDriveMediaType) +
                                                        1))) {
-                                  {
-                                  }
+                                  {}
                                   ntStatus = -2147483643L;
                                   highestDriveMediaType =
                                       (enum _DRIVE_MEDIA_TYPE)(
@@ -3069,8 +3064,7 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                               switch_16_exp_10: /* CIL Label */;
                                 if ((int)((KUSER_SHARED_DATA *const)4292804608U)
                                         ->AlternativeArchitecture == 1) {
-                                  {
-                                  }
+                                  {}
                                   if (!(DeviceObject->Characteristics & 1UL)) {
                                     ntStatus = -1073741275L;
                                     goto switch_16_break;
@@ -3215,13 +3209,11 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                               switch_16_exp_11: /* CIL Label */;
                                 if ((int)((KUSER_SHARED_DATA *const)4292804608U)
                                         ->AlternativeArchitecture == 1) {
-                                  {
-                                  }
+                                  {}
                                   if (irpSp->Parameters.DeviceIoControl
                                           .OutputBufferLength <
                                       (ULONG)sizeof(SENSE_DEVISE_STATUS_PTOS)) {
-                                    {
-                                    }
+                                    {}
                                     ntStatus = -1073741811L;
                                     goto switch_16_break;
                                   } else {
@@ -3382,8 +3374,7 @@ NTSTATUS FloppyPnp(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                     switch_32_5: /* CIL Label */;
                     switch_32_1: /* CIL Label */;
                       if ((int)irpSp->MinorFunction == 5) {
-                        {
-                        }
+                        {}
                       } else {
                         {}
                       }
@@ -3454,8 +3445,7 @@ NTSTATUS FloppyPnp(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                     switch_32_6: /* CIL Label */;
                     switch_32_3: /* CIL Label */;
                       if ((int)irpSp->MinorFunction == 6) {
-                        {
-                        }
+                        {}
                       } else {
                         {}
                       }
@@ -3494,14 +3484,10 @@ NTSTATUS FloppyPnp(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                            * 1, 0); */ /* INLINED */
                         }
                         if (s != NP) {
-                          {
-                            errorFn();
-                          }
+                          { errorFn(); }
                         } else {
                           if (compRegistered != 0) {
-                            {
-                              errorFn();
-                            }
+                            { errorFn(); }
                           } else {
                             compRegistered = 1;
                             compFptr = &FloppyPnpComplete;
@@ -3696,14 +3682,10 @@ NTSTATUS FloppyStartDevice(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
       nextIrpSp->Control = 0;
     }
     if (s != NP) {
-      {
-        errorFn();
-      }
+      { errorFn(); }
     } else {
       if (compRegistered != 0) {
-        {
-          errorFn();
-        }
+        { errorFn(); }
       } else {
         compRegistered = 1;
         compFptr = &FloppyPnpComplete;
@@ -3738,9 +3720,7 @@ NTSTATUS FloppyStartDevice(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
       disketteExtension->MaxTransferSize = fdcInfo.MaxTransferSize;
       if (fdcInfo.AcpiBios) {
         if (fdcInfo.AcpiFdiSupported) {
-          {
-            ntStatus = FlAcpiConfigureFloppy(disketteExtension, &fdcInfo);
-          }
+          { ntStatus = FlAcpiConfigureFloppy(disketteExtension, &fdcInfo); }
           if ((int)disketteExtension->DriveType == 4) {
             disketteExtension->PerpendicularMode =
                 (int)disketteExtension->PerpendicularMode |
@@ -3775,8 +3755,7 @@ NTSTATUS FloppyStartDevice(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                   &FlConfigCallBack, disketteExtension);
             }
             if (ntStatus >= 0L) {
-              {
-              }
+              {}
               goto while_43_break;
             } else {
             }
@@ -3903,8 +3882,7 @@ NTSTATUS FloppyPower(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                  * disketteExtension->PowerDownMutex); */ /* INLINED */
               }
               if ((int)state.SystemState == 1) {
-                {
-                }
+                {}
                 disketteExtension->PoweringDown = 0;
                 WaitForCompletion = 0;
               } else {
@@ -4053,8 +4031,7 @@ NTSTATUS FlInterpretError(UCHAR StatusRegister1, UCHAR StatusRegister2) {
       }
     }
     if ((int)StatusRegister1 & 16) {
-      {
-      }
+      {}
       return (-1073741764L);
     } else {
     }
@@ -4083,20 +4060,17 @@ NTSTATUS FlInterpretError(UCHAR StatusRegister1, UCHAR StatusRegister2) {
       }
     }
     if ((int)StatusRegister1 & 2) {
-      {
-      }
+      {}
       return (-1073741662L);
     } else {
     }
     if ((int)StatusRegister1 & 1) {
-      {
-      }
+      {}
       return (-1073741467L);
     } else {
     }
     if ((int)StatusRegister2 & 16) {
-      {
-      }
+      {}
       return (-1073741466L);
     } else {
     }
@@ -4115,12 +4089,9 @@ void FlFinishOperation(PIRP Irp, PDISKETTE_EXTENSION DisketteExtension) {
         DisketteExtension->HardwareFailCount =
             (UCHAR)((int)DisketteExtension->HardwareFailCount + 1);
         if ((int)DisketteExtension->HardwareFailCount < 2) {
-          {
-            ntStatus = FlInitializeControllerHardware(DisketteExtension);
-          }
+          { ntStatus = FlInitializeControllerHardware(DisketteExtension); }
           if (ntStatus >= 0L) {
-            {
-            }
+            {}
             DisketteExtension->MediaType = -1;
             {} {
               /*           ExAcquireFastMutex(&
@@ -4186,8 +4157,7 @@ void FlFinishOperation(PIRP Irp, PDISKETTE_EXTENSION DisketteExtension) {
     if (myStatus != 0L) {
       if (myStatus != -2147483626L) {
         if (myStatus != -1073741805L) {
-          {
-          }
+          {}
         } else {
           goto _L___0;
         }
@@ -4289,8 +4259,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
                     DisketteExtension->FifoBuffer, (void *)0, 0, 0);
               }
               if (!(ntStatus >= 0L)) {
-                {
-                }
+                {}
                 return (ntStatus);
               } else {
               }
@@ -4300,8 +4269,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
                 driveStatus = 128;
               }
               if ((int)driveStatus & 128) {
-                {
-                }
+                {}
                 if ((int)((DisketteExtension->DeviceObject)->Vpb)->Flags & 1) {
                   (DisketteExtension->DeviceObject)->Flags &= 4294967293UL;
                 } else {
@@ -4320,8 +4288,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
                   DisketteExtension->FifoBuffer, (void *)0, 0, 0);
             }
             if (!(ntStatus >= 0L)) {
-              {
-              }
+              {}
               return (ntStatus);
             } else {
               if (!((int)DisketteExtension->FifoBuffer[0] & 32)) {
@@ -4351,8 +4318,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
               KeDelayExecutionThread(0, 0, &delay);
             }
             if (!(ntStatus >= 0L)) {
-              {
-              }
+              {}
               return (ntStatus);
             } else {
               if (!((int)DisketteExtension->FifoBuffer[0] & 32)) {
@@ -4378,8 +4344,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
                     DisketteExtension->FifoBuffer, (void *)0, 0, 0);
               }
               if (!(ntStatus >= 0L)) {
-                {
-                }
+                {}
                 return (ntStatus);
               } else {
               }
@@ -4401,8 +4366,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
               }
             }
             if ((int)driveStatus & 128) {
-              {
-              }
+              {}
               if ((int)((DisketteExtension->DeviceObject)->Vpb)->Flags & 1) {
                 (DisketteExtension->DeviceObject)->Flags &= 4294967293UL;
               } else {
@@ -4414,8 +4378,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
           }
           if ((int)IgnoreChange == 0) {
             if ((int)((DisketteExtension->DeviceObject)->Vpb)->Flags & 1) {
-              {
-              }
+              {}
               return (-2147483626L);
             } else {
               return (-1073741435L);
@@ -4429,32 +4392,24 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
       _L___2: /* CIL Label */
         if ((int)((KUSER_SHARED_DATA *const)4292804608U)
                 ->AlternativeArchitecture == 1) {
-          {
-            FlHdbit(DisketteExtension);
-          }
+          { FlHdbit(DisketteExtension); }
         } else {
         }
       }
     }
     if (SetUpMedia) {
       if ((int)DisketteExtension->MediaType == -1) {
-        {
-          ntStatus = FlDetermineMediaType(DisketteExtension);
-        }
+        { ntStatus = FlDetermineMediaType(DisketteExtension); }
       } else {
         if ((int)DisketteExtension->MediaType == 0) {
-          {
-          }
+          {}
           return (-1073741804L);
         } else {
           if ((int)DisketteExtension->DriveMediaType !=
               (int)DisketteExtension->LastDriveMediaType) {
-            {
-              ntStatus = FlDatarateSpecifyConfigure(DisketteExtension);
-            }
+            { ntStatus = FlDatarateSpecifyConfigure(DisketteExtension); }
             if (!(ntStatus >= 0L)) {
-              {
-              }
+              {}
             } else {
             }
           } else {
@@ -4473,24 +4428,21 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
                              DisketteExtension->FifoBuffer, (void *)0, 0, 0);
         }
         if (!(ntStatus >= 0L)) {
-          {
-          }
+          {}
           return (ntStatus);
         } else {
         }
         if ((int)((KUSER_SHARED_DATA *const)4292804608U)
                 ->AlternativeArchitecture == 1) {
           if (!((int)DisketteExtension->FifoBuffer[0] & 32)) {
-            {
-            }
+            {}
             return (-1073741805L);
           } else {
           }
         } else {
         }
         if ((int)DisketteExtension->FifoBuffer[0] & 64) {
-          {
-          }
+          {}
           return (-1073741662L);
         } else {
         }
@@ -4552,9 +4504,7 @@ NTSTATUS FlDatarateSpecifyConfigure(PDISKETTE_EXTENSION DisketteExtension) {
                 &DisketteExtension->DriveMediaConstants.DataTransferRate);
           }
           if (ntStatus >= 0L) {
-            {
-              ntStatus = FlRecalibrateDrive(DisketteExtension);
-            }
+            { ntStatus = FlRecalibrateDrive(DisketteExtension); }
           } else {
           }
         } else {
@@ -4591,8 +4541,7 @@ NTSTATUS FlRecalibrateDrive(PDISKETTE_EXTENSION DisketteExtension) {
                              DisketteExtension->FifoBuffer, (void *)0, 0, 0);
         }
         if (!(ntStatus >= 0L)) {
-          {
-          }
+          {}
         } else {
         }
         if (ntStatus >= 0L) {
@@ -4608,8 +4557,7 @@ NTSTATUS FlRecalibrateDrive(PDISKETTE_EXTENSION DisketteExtension) {
                   DisketteExtension->FifoBuffer, (void *)0, 0, 0);
             }
             if (!(ntStatus >= 0L)) {
-              {
-              }
+              {}
               return (ntStatus);
             } else {
             }
@@ -4698,8 +4646,7 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) {
             }
             { ntStatus = FlDatarateSpecifyConfigure(DisketteExtension); }
             if (!(ntStatus >= 0L)) {
-              {
-              }
+              {}
               mediaTypesExhausted = 1;
             } else {
               {
@@ -4831,8 +4778,7 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) {
                             /*                     ExFreePool(bootSector); */ /* INLINED */
                           }
                           if (!(ntStatus >= 0L)) {
-                            {
-                            }
+                            {}
                             DisketteExtension->DriveMediaType =
                                 (DRIVE_MEDIA_TYPE)(
                                     (int)DisketteExtension->DriveMediaType - 1);
@@ -4875,8 +4821,7 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) {
         while_101_break: /* CIL Label */;
         }
         if (ntStatus >= 0L) {
-          {
-          }
+          {}
           goto while_99_break;
         } else {
         }
@@ -5270,8 +5215,7 @@ void FloppyThread(PVOID Context) {
                         }
                         if ((disketteExtension->DeviceObject)->Flags & 2UL) {
                           if (!((int)irpSp->Flags & 2)) {
-                            {
-                            }
+                            {}
                             ntStatus = -2147483626L;
                           } else {
                             {
@@ -5303,8 +5247,7 @@ void FloppyThread(PVOID Context) {
                         }
                         if ((disketteExtension->DeviceObject)->Flags & 2UL) {
                           if (!((int)irpSp->Flags & 2)) {
-                            {
-                            }
+                            {}
                             ntStatus = -2147483626L;
                           } else {
                             goto _L___2;
@@ -5394,8 +5337,7 @@ void FloppyThread(PVOID Context) {
                                                   disketteExtension->MediaType;
                                               if ((int)disketteExtension
                                                       ->MediaType == 0) {
-                                                {
-                                                }
+                                                {}
                                                 outputBuffer->Cylinders
                                                     .__annonCompField1.LowPart =
                                                     0;
@@ -5559,9 +5501,7 @@ void FloppyThread(PVOID Context) {
             } else {
               irp->IoStatus.__annonCompField4.Status = ntStatus;
               if (disketteExtension->IoBuffer) {
-                {
-                  FlFreeIoBuffer(disketteExtension);
-                }
+                { FlFreeIoBuffer(disketteExtension); }
               } else {
               }
               { FlFinishOperation(irp, disketteExtension); }
@@ -5990,8 +5930,7 @@ NTSTATUS FlReadWriteTrack(PDISKETTE_EXTENSION DisketteExtension, PMDL IoMdl,
           }
         }
         if (!(status >= 0L)) {
-          {
-          }
+          {}
           recalibrateDrive = 1;
           goto __Cont;
         } else {
@@ -6075,8 +6014,7 @@ NTSTATUS FlReadWriteTrack(PDISKETTE_EXTENSION DisketteExtension, PMDL IoMdl,
             } else {
             }
             if (ioRetry >= 2UL) {
-              {
-              }
+              {}
               goto while_149_break;
             } else {
             }
@@ -6096,8 +6034,7 @@ NTSTATUS FlReadWriteTrack(PDISKETTE_EXTENSION DisketteExtension, PMDL IoMdl,
     }
     if (!(status >= 0L)) {
       if ((int)NumberOfSectors > 1) {
-        {
-        }
+        {}
         i = 0;
         {
           while (1) {
@@ -6115,8 +6052,7 @@ NTSTATUS FlReadWriteTrack(PDISKETTE_EXTENSION DisketteExtension, PMDL IoMdl,
                   (unsigned char)((int)Sector + (int)i), 1, 0);
             }
             if (!(status >= 0L)) {
-              {
-              }
+              {}
               DisketteExtension->HardwareFailed = 1;
               goto while_153_break;
             } else {
@@ -6163,8 +6099,7 @@ NTSTATUS FlReadWrite(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
     {}
     if ((int)irpSp->MajorFunction == 4) {
       if (DisketteExtension->IsReadOnly) {
-        {
-        }
+        {}
         return (-1073741811L);
       } else {
       }
@@ -6182,21 +6117,17 @@ NTSTATUS FlReadWrite(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
       }
     }
     if (!(status >= 0L)) {
-      {
-      }
+      {}
       return (status);
     } else {
     }
     if ((int)((KUSER_SHARED_DATA *const)4292804608U)->AlternativeArchitecture ==
         1) {
-      {
-        FlHdbit(DisketteExtension);
-      }
+      { FlHdbit(DisketteExtension); }
     } else {
     }
     if ((int)DisketteExtension->MediaType == 0) {
-      {
-      }
+      {}
       return (-1073741804L);
     } else {
     }
@@ -6219,8 +6150,7 @@ NTSTATUS FlReadWrite(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
       }
     }
     if ((unsigned int)userBuffer == (unsigned int)((void *)0)) {
-      {
-      }
+      {}
       return (-1073741670L);
     } else {
     }
@@ -6251,8 +6181,7 @@ NTSTATUS FlReadWrite(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp,
         if (trackSize > DisketteExtension->MaxTransferSize) {
           {} { FlAllocateIoBuffer(DisketteExtension, trackSize); }
           if (!DisketteExtension->IoBuffer) {
-            {
-            }
+            {}
             return (-1073741670L);
           } else {
           }
@@ -6431,15 +6360,11 @@ NTSTATUS FlFormat(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp) {
     {}
     if ((int)((KUSER_SHARED_DATA *const)4292804608U)->AlternativeArchitecture ==
         1) {
-      {
-        FlHdbit(DisketteExtension);
-      }
+      { FlHdbit(DisketteExtension); }
     } else {
     }
     if ((int)DisketteExtension->LastDriveMediaType != (int)driveMediaType) {
-      {
-        ntStatus = FlDatarateSpecifyConfigure(DisketteExtension);
-      }
+      { ntStatus = FlDatarateSpecifyConfigure(DisketteExtension); }
       if (!(ntStatus >= 0L)) {
         return (ntStatus);
       } else {
@@ -6500,8 +6425,7 @@ NTSTATUS FlFormat(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp) {
         } else {
         }
         if (!(ntStatus >= 0L)) {
-          {
-          }
+          {}
           return (ntStatus);
         } else {
         }
@@ -6558,8 +6482,7 @@ NTSTATUS FlFormat(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp) {
                   0, length);
             }
             if (!(ntStatus >= 0L)) {
-              {
-              }
+              {}
             } else {
             }
             if (ntStatus >= 0L) {
@@ -6609,8 +6532,7 @@ NTSTATUS FlFormat(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp) {
                   DisketteExtension->FifoBuffer, (void *)0, 0, 0);
             }
             if (!(ntStatus >= 0L)) {
-              {
-              }
+              {}
               return (ntStatus);
             } else {
             }
@@ -6821,8 +6743,7 @@ NTSTATUS FlFdcDeviceIo(PDEVICE_OBJECT DeviceObject, ULONG Ioctl, PVOID Data) {
                                         (void *)0, 0, 1, &doneEvent, &ioStatus);
     }
     if ((unsigned int)irp == (unsigned int)((void *)0)) {
-      {
-      }
+      {}
       return (-1073741670L);
     } else {
     }
@@ -7000,9 +6921,7 @@ NTSTATUS FlHdbit(PDISKETTE_EXTENSION DisketteExtension) {
     } else {
     }
     if (setHdBitParameter.ChangedHdBit) {
-      {
-        ntStatus = FlDatarateSpecifyConfigure(DisketteExtension);
-      }
+      { ntStatus = FlDatarateSpecifyConfigure(DisketteExtension); }
     } else {
     }
     return (ntStatus);
@@ -7377,9 +7296,7 @@ int main(void) {
         }
       }
       if (we_should_unload) {
-        {
-          FloppyUnload(&d);
-        }
+        { FloppyUnload(&d); }
       } else {
       }
     } else {
@@ -7409,9 +7326,7 @@ int main(void) {
             if (s != SKIP2) {
               if (s != IPC) {
                 if (s != DC) {
-                  {
-                    errorFn();
-                  }
+                  { errorFn(); }
                 } else {
                   goto _L___0;
                 }
@@ -7428,16 +7343,12 @@ int main(void) {
               } else {
                 if (s == DC) {
                   if (status == 259L) {
-                    {
-                      errorFn();
-                    }
+                    { errorFn(); }
                   } else {
                   }
                 } else {
                   if (status != (NTSTATUS)lowerDriverReturn) {
-                    {
-                      errorFn();
-                    }
+                    { errorFn(); }
                   } else {
                   }
                 }
@@ -7875,9 +7786,7 @@ NTSTATUS IofCallDriver(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
         compRetStatus1 = tmp;
       }
       if ((long)compRetStatus1 == -1073741802L) {
-        {
-          stubMoreProcessingRequired();
-        }
+        { stubMoreProcessingRequired(); }
       } else {
       }
     } else {
@@ -8031,9 +7940,7 @@ NTSTATUS KeWaitForSingleObject(PVOID Object, KWAIT_REASON WaitReason,
         customIrp = 0;
       } else {
         if (s == MPR3) {
-          {
-            errorFn();
-          }
+          { errorFn(); }
         } else {
         }
       }
@@ -8168,9 +8075,7 @@ NTSTATUS PoCallDriver(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
         compRetStatus = tmp;
       }
       if ((long)compRetStatus == -1073741802L) {
-        {
-          stubMoreProcessingRequired();
-        }
+        { stubMoreProcessingRequired(); }
       } else {
       }
     } else {
diff --git a/test/c/float/floor.c b/test/c/float/floor.c
index 17f6abefa..86b3944e0 100644
--- a/test/c/float/floor.c
+++ b/test/c/float/floor.c
@@ -9,17 +9,17 @@ int main(void) {
   assert(floor(-2.7) == -3.0);
   double c = floor(-0.0);
   assert(c == -0.0);
-  assert(sizeof(c) == sizeof(float)
-             ? __signbitf(c)
-             : sizeof(c) == sizeof(double) ? __signbit(c) : __signbitl(c));
+  assert(sizeof(c) == sizeof(float)    ? __signbitf(c)
+         : sizeof(c) == sizeof(double) ? __signbit(c)
+                                       : __signbitl(c));
   c = floor(-(__builtin_inff()));
   assert(sizeof((__builtin_inff())) == sizeof(float)
              ? __isinff((__builtin_inff()))
-             : sizeof((__builtin_inff())) == sizeof(double)
-                   ? __isinf((__builtin_inff()))
-                   : __isinfl((__builtin_inff())));
-  assert(sizeof(c) == sizeof(float)
-             ? __signbitf(c)
-             : sizeof(c) == sizeof(double) ? __signbit(c) : __signbitl(c));
+         : sizeof((__builtin_inff())) == sizeof(double)
+             ? __isinf((__builtin_inff()))
+             : __isinfl((__builtin_inff())));
+  assert(sizeof(c) == sizeof(float)    ? __signbitf(c)
+         : sizeof(c) == sizeof(double) ? __signbit(c)
+                                       : __signbitl(c));
   return 0;
 }
diff --git a/test/c/float/floor_fail.c b/test/c/float/floor_fail.c
index d19a4ee40..619bc7e52 100644
--- a/test/c/float/floor_fail.c
+++ b/test/c/float/floor_fail.c
@@ -9,17 +9,17 @@ int main(void) {
   assert(floor(-2.7) == -3.0);
   double c = floor(-0.0);
   assert(c == -0.0);
-  assert(sizeof(c) == sizeof(float)
-             ? __signbitf(c)
-             : sizeof(c) == sizeof(double) ? __signbit(c) : __signbitl(c));
+  assert(sizeof(c) == sizeof(float)    ? __signbitf(c)
+         : sizeof(c) == sizeof(double) ? __signbit(c)
+                                       : __signbitl(c));
   c = floor(__builtin_inff());
   assert(sizeof((__builtin_inff())) == sizeof(float)
              ? __isinff((__builtin_inff()))
-             : sizeof((__builtin_inff())) == sizeof(double)
-                   ? __isinf((__builtin_inff()))
-                   : __isinfl((__builtin_inff())));
-  assert(sizeof(c) == sizeof(float)
-             ? __signbitf(c)
-             : sizeof(c) == sizeof(double) ? __signbit(c) : __signbitl(c));
+         : sizeof((__builtin_inff())) == sizeof(double)
+             ? __isinf((__builtin_inff()))
+             : __isinfl((__builtin_inff())));
+  assert(sizeof(c) == sizeof(float)    ? __signbitf(c)
+         : sizeof(c) == sizeof(double) ? __signbit(c)
+                                       : __signbitl(c));
   return 0;
 }
diff --git a/test/c/ntdrivers-simplified/cdaudio_simpl1_false.cil.c b/test/c/ntdrivers-simplified/cdaudio_simpl1_false.cil.c
index 979cfcdb9..136b23ccd 100644
--- a/test/c/ntdrivers-simplified/cdaudio_simpl1_false.cil.c
+++ b/test/c/ntdrivers-simplified/cdaudio_simpl1_false.cil.c
@@ -2768,9 +2768,7 @@ int main(void) {
                 }
               } else {
                 if (status != 259) {
-                  {
-                    errorFn();
-                  }
+                  { errorFn(); }
                 } else {
                 }
               }
diff --git a/test/c/ntdrivers/cdaudio_true.i.cil.c b/test/c/ntdrivers/cdaudio_true.i.cil.c
index eaf4246e8..c1912ab78 100644
--- a/test/c/ntdrivers/cdaudio_true.i.cil.c
+++ b/test/c/ntdrivers/cdaudio_true.i.cil.c
@@ -3387,9 +3387,7 @@ NTSTATUS CdAudioStartDevice(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
       } else {
         { tmp___7 = memcmp(inquiryDataPtr + 16, "CDR-3650/1650S  ", 16); }
         if (tmp___7) {
-          {
-            tmp___8 = memcmp(inquiryDataPtr + 16, "CDR-1750S       ", 16);
-          }
+          { tmp___8 = memcmp(inquiryDataPtr + 16, "CDR-1750S       ", 16); }
           if (tmp___8) {
 
           } else {
@@ -3580,9 +3578,7 @@ NTSTATUS CdAudioPnp(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
             return (status);
           switch_2_22: /* CIL Label */;
             if ((int)irpSp->Parameters.UsageNotification.Type != 1) {
-              {
-                tmp = CdAudioSendToNextDriver(DeviceObject, Irp);
-              }
+              { tmp = CdAudioSendToNextDriver(DeviceObject, Irp); }
               return (tmp);
             } else {
             }
@@ -3607,9 +3603,7 @@ NTSTATUS CdAudioPnp(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
             { status = CdAudioForwardIrpSynchronous(DeviceObject, Irp); }
             if (status >= 0L) {
               if (irpSp->Parameters.UsageNotification.InPath) {
-                {
-                  InterlockedIncrement(&deviceExtension->PagingPathCount);
-                }
+                { InterlockedIncrement(&deviceExtension->PagingPathCount); }
               } else {
                 { InterlockedDecrement(&deviceExtension->PagingPathCount); }
               }
@@ -8065,14 +8059,10 @@ NTSTATUS CdAudioHPCdrDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
         nextIrpSp->Control = 0;
       }
       if (s != NP) {
-        {
-          errorFn();
-        }
+        { errorFn(); }
       } else {
         if (compRegistered != 0) {
-          {
-            errorFn();
-          }
+          { errorFn(); }
         } else {
           compRegistered = 1;
           routine = 0;
@@ -8122,14 +8112,10 @@ NTSTATUS CdAudioForwardIrpSynchronous(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
       nextIrpSp->Control = 0;
     }
     if (s != NP) {
-      {
-        errorFn();
-      }
+      { errorFn(); }
     } else {
       if (compRegistered != 0) {
-        {
-          errorFn();
-        }
+        { errorFn(); }
       } else {
         compRegistered = 1;
         routine = 1;
@@ -8334,9 +8320,7 @@ int main(void) {
             if (s != SKIP2) {
               if (s != IPC) {
                 if (s != DC) {
-                  {
-                    errorFn();
-                  }
+                  { errorFn(); }
                 } else {
                   goto _L___0;
                 }
@@ -8347,24 +8331,18 @@ int main(void) {
             _L___0: /* CIL Label */
               if (pended == 1) {
                 if (status != 259L) {
-                  {
-                    errorFn();
-                  }
+                  { errorFn(); }
                 } else {
                 }
               } else {
                 if (s == DC) {
                   if (status == 259L) {
-                    {
-                      errorFn();
-                    }
+                    { errorFn(); }
                   } else {
                   }
                 } else {
                   if (status != (NTSTATUS)lowerDriverReturn) {
-                    {
-                      errorFn();
-                    }
+                    { errorFn(); }
                   } else {
                   }
                 }
@@ -8820,9 +8798,7 @@ NTSTATUS IofCallDriver(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
         }
       }
       if ((long)compRetStatus == -1073741802L) {
-        {
-          stubMoreProcessingRequired();
-        }
+        { stubMoreProcessingRequired(); }
       } else {
       }
     } else {
@@ -8980,9 +8956,7 @@ NTSTATUS KeWaitForSingleObject(PVOID Object, KWAIT_REASON WaitReason,
         customIrp = 0;
       } else {
         if (s == MPR3) {
-          {
-            errorFn();
-          }
+          { errorFn(); }
         } else {
         }
       }
@@ -9128,9 +9102,7 @@ NTSTATUS PoCallDriver(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
         }
       }
       if ((long)compRetStatus == -1073741802L) {
-        {
-          stubMoreProcessingRequired();
-        }
+        { stubMoreProcessingRequired(); }
       } else {
       }
     } else {
diff --git a/test/c/ntdrivers/diskperf_false.i.cil.c b/test/c/ntdrivers/diskperf_false.i.cil.c
index 96d7530bb..5c4b1e53a 100644
--- a/test/c/ntdrivers/diskperf_false.i.cil.c
+++ b/test/c/ntdrivers/diskperf_false.i.cil.c
@@ -2402,14 +2402,10 @@ NTSTATUS DiskPerfForwardIrpSynchronous(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
       nextIrpSp->Control = 0;
     }
     if (s != NP) {
-      {
-        errorFn();
-      }
+      { errorFn(); }
     } else {
       if (compRegistered != 0) {
-        {
-          errorFn();
-        }
+        { errorFn(); }
       } else {
         compRegistered = 1;
         compFptr = &DiskPerfIrpCompletion;
@@ -2484,21 +2480,15 @@ NTSTATUS DiskPerfReadWrite(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
     } else {
     }
     if (deviceExtension->CountersEnabled <= 0L) {
-      {
-        tmp___0 = DiskPerfSendToNextDriver(DeviceObject, Irp);
-      }
+      { tmp___0 = DiskPerfSendToNextDriver(DeviceObject, Irp); }
       return (tmp___0);
     } else {
       if ((int)deviceExtension->PhysicalDeviceNameBuffer[0] == 0) {
-        {
-          tmp___0 = DiskPerfSendToNextDriver(DeviceObject, Irp);
-        }
+        { tmp___0 = DiskPerfSendToNextDriver(DeviceObject, Irp); }
         return (tmp___0);
       } else {
         if ((unsigned int)partitionCounters == (unsigned int)((void *)0)) {
-          {
-            tmp___0 = DiskPerfSendToNextDriver(DeviceObject, Irp);
-          }
+          { tmp___0 = DiskPerfSendToNextDriver(DeviceObject, Irp); }
           return (tmp___0);
         } else {
         }
@@ -2517,14 +2507,10 @@ NTSTATUS DiskPerfReadWrite(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
     } else {
     }
     if (s != NP) {
-      {
-        errorFn();
-      }
+      { errorFn(); }
     } else {
       if (compRegistered != 0) {
-        {
-          errorFn();
-        }
+        { errorFn(); }
       } else {
         compRegistered = 1;
         compFptr = &DiskPerfIoCompletion;
@@ -2579,9 +2565,7 @@ NTSTATUS DiskPerfIoCompletion(PDEVICE_OBJECT DeviceObject, PIRP Irp,
       queueLen = InterlockedDecrement(&deviceExtension->QueueDepth);
     }
     if (queueLen < 0L) {
-      {
-        queueLen = InterlockedIncrement(&deviceExtension->QueueDepth);
-      }
+      { queueLen = InterlockedIncrement(&deviceExtension->QueueDepth); }
     } else {
     }
     if (queueLen == 0L) {
@@ -2728,9 +2712,7 @@ NTSTATUS DiskPerfWmi(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
     deviceExtension = DeviceObject->DeviceExtension;
     wmilibContext = &deviceExtension->WmilibContext;
     if (wmilibContext->GuidCount == 0UL) {
-      {
-        tmp = DiskPerfSendToNextDriver(DeviceObject, Irp);
-      }
+      { tmp = DiskPerfSendToNextDriver(DeviceObject, Irp); }
       return (tmp);
     } else {
     }
@@ -2813,9 +2795,7 @@ NTSTATUS DiskPerfRegisterDevice(PDEVICE_OBJECT DeviceObject) {
           (void *)0, 0, &number, sizeof(number), 0, &event, &ioStatus);
     }
     if (!irp) {
-      {
-        DiskPerfLogError(DeviceObject, 256, 0L, -1073479678L);
-      }
+      { DiskPerfLogError(DeviceObject, 256, 0L, -1073479678L); }
       return (-1073741670L);
     } else {
     }
@@ -2848,9 +2828,7 @@ NTSTATUS DiskPerfRegisterDevice(PDEVICE_OBJECT DeviceObject) {
         output = tmp;
       }
       if (!output) {
-        {
-          DiskPerfLogError(DeviceObject, 257, 0L, -1073479678L);
-        }
+        { DiskPerfLogError(DeviceObject, 257, 0L, -1073479678L); }
         return (-1073741670L);
       } else {
       }
@@ -2885,9 +2863,7 @@ NTSTATUS DiskPerfRegisterDevice(PDEVICE_OBJECT DeviceObject) {
           output = tmp___0;
         }
         if (!output) {
-          {
-            DiskPerfLogError(DeviceObject, 258, 0L, -1073479678L);
-          }
+          { DiskPerfLogError(DeviceObject, 258, 0L, -1073479678L); }
           return (-1073741670L);
         } else {
         }
@@ -2944,9 +2920,7 @@ NTSTATUS DiskPerfRegisterDevice(PDEVICE_OBJECT DeviceObject) {
             sizeof(VOLUME_NUMBER), 0, &event, &ioStatus);
       }
       if (!irp) {
-        {
-          DiskPerfLogError(DeviceObject, 265, 0L, -1073479678L);
-        }
+        { DiskPerfLogError(DeviceObject, 265, 0L, -1073479678L); }
         return (-1073741670L);
       } else {
       }
@@ -2983,9 +2957,7 @@ NTSTATUS DiskPerfRegisterDevice(PDEVICE_OBJECT DeviceObject) {
     }
     { status = IoWMIRegistrationControl(DeviceObject, 1UL | registrationFlag); }
     if (!(status >= 0L)) {
-      {
-        DiskPerfLogError(DeviceObject, 261, 0L, -1073479668L);
-      }
+      { DiskPerfLogError(DeviceObject, 261, 0L, -1073479668L); }
     } else {
     }
     return (status);
@@ -3156,9 +3128,7 @@ NTSTATUS DiskperfWmiFunctionControl(PDEVICE_OBJECT DeviceObject, PIRP Irp,
     if (GuidIndex == 0UL) {
       if ((int)Function == 1) {
         if (Enable) {
-          {
-            tmp = InterlockedIncrement(&deviceExtension->CountersEnabled);
-          }
+          { tmp = InterlockedIncrement(&deviceExtension->CountersEnabled); }
           if (tmp == 1L) {
             if ((unsigned int)deviceExtension->DiskCounters !=
                 (unsigned int)((void *)0)) {
@@ -3381,9 +3351,7 @@ int main(void) {
             if (s != SKIP2) {
               if (s != IPC) {
                 if (s != DC) {
-                  {
-                    errorFn();
-                  }
+                  { errorFn(); }
                 } else {
                   goto _L___0;
                 }
@@ -3394,21 +3362,15 @@ int main(void) {
             _L___0: /* CIL Label */
               if (pended == 1) {
                 if (status != 259L) {
-                  {
-                    errorFn();
-                  }
+                  { errorFn(); }
                 } else {
                 }
               } else {
                 if (s == DC) {
-                  {
-                    errorFn();
-                  }
+                  { errorFn(); }
                 } else {
                   if (status != (NTSTATUS)lowerDriverReturn) {
-                    {
-                      errorFn();
-                    }
+                    { errorFn(); }
                   } else {
                   }
                 }
@@ -3848,9 +3810,7 @@ NTSTATUS IofCallDriver(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
         }
       }
       if ((long)compRetStatus == -1073741802L) {
-        {
-          stubMoreProcessingRequired();
-        }
+        { stubMoreProcessingRequired(); }
       } else {
       }
     } else {
@@ -4004,9 +3964,7 @@ NTSTATUS KeWaitForSingleObject(PVOID Object, KWAIT_REASON WaitReason,
         customIrp = 0;
       } else {
         if (s == MPR3) {
-          {
-            errorFn();
-          }
+          { errorFn(); }
         } else {
         }
       }
@@ -4152,9 +4110,7 @@ NTSTATUS PoCallDriver(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
         }
       }
       if ((long)compRetStatus == -1073741802L) {
-        {
-          stubMoreProcessingRequired();
-        }
+        { stubMoreProcessingRequired(); }
       } else {
       }
     } else {
diff --git a/test/c/ntdrivers/diskperf_true.i.cil.c b/test/c/ntdrivers/diskperf_true.i.cil.c
index f24b841e8..a497dd592 100644
--- a/test/c/ntdrivers/diskperf_true.i.cil.c
+++ b/test/c/ntdrivers/diskperf_true.i.cil.c
@@ -2402,14 +2402,10 @@ NTSTATUS DiskPerfForwardIrpSynchronous(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
       nextIrpSp->Control = 0;
     }
     if (s != NP) {
-      {
-        errorFn();
-      }
+      { errorFn(); }
     } else {
       if (compRegistered != 0) {
-        {
-          errorFn();
-        }
+        { errorFn(); }
       } else {
         compRegistered = 1;
         compFptr = &DiskPerfIrpCompletion;
@@ -2484,21 +2480,15 @@ NTSTATUS DiskPerfReadWrite(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
     } else {
     }
     if (deviceExtension->CountersEnabled <= 0L) {
-      {
-        tmp___0 = DiskPerfSendToNextDriver(DeviceObject, Irp);
-      }
+      { tmp___0 = DiskPerfSendToNextDriver(DeviceObject, Irp); }
       return (tmp___0);
     } else {
       if ((int)deviceExtension->PhysicalDeviceNameBuffer[0] == 0) {
-        {
-          tmp___0 = DiskPerfSendToNextDriver(DeviceObject, Irp);
-        }
+        { tmp___0 = DiskPerfSendToNextDriver(DeviceObject, Irp); }
         return (tmp___0);
       } else {
         if ((unsigned int)partitionCounters == (unsigned int)((void *)0)) {
-          {
-            tmp___0 = DiskPerfSendToNextDriver(DeviceObject, Irp);
-          }
+          { tmp___0 = DiskPerfSendToNextDriver(DeviceObject, Irp); }
           return (tmp___0);
         } else {
         }
@@ -2517,14 +2507,10 @@ NTSTATUS DiskPerfReadWrite(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
     } else {
     }
     if (s != NP) {
-      {
-        errorFn();
-      }
+      { errorFn(); }
     } else {
       if (compRegistered != 0) {
-        {
-          errorFn();
-        }
+        { errorFn(); }
       } else {
         compRegistered = 1;
         compFptr = &DiskPerfIoCompletion;
@@ -2579,9 +2565,7 @@ NTSTATUS DiskPerfIoCompletion(PDEVICE_OBJECT DeviceObject, PIRP Irp,
       queueLen = InterlockedDecrement(&deviceExtension->QueueDepth);
     }
     if (queueLen < 0L) {
-      {
-        queueLen = InterlockedIncrement(&deviceExtension->QueueDepth);
-      }
+      { queueLen = InterlockedIncrement(&deviceExtension->QueueDepth); }
     } else {
     }
     if (queueLen == 0L) {
@@ -2728,9 +2712,7 @@ NTSTATUS DiskPerfWmi(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
     deviceExtension = DeviceObject->DeviceExtension;
     wmilibContext = &deviceExtension->WmilibContext;
     if (wmilibContext->GuidCount == 0UL) {
-      {
-        tmp = DiskPerfSendToNextDriver(DeviceObject, Irp);
-      }
+      { tmp = DiskPerfSendToNextDriver(DeviceObject, Irp); }
       return (tmp);
     } else {
     }
@@ -2813,9 +2795,7 @@ NTSTATUS DiskPerfRegisterDevice(PDEVICE_OBJECT DeviceObject) {
           (void *)0, 0, &number, sizeof(number), 0, &event, &ioStatus);
     }
     if (!irp) {
-      {
-        DiskPerfLogError(DeviceObject, 256, 0L, -1073479678L);
-      }
+      { DiskPerfLogError(DeviceObject, 256, 0L, -1073479678L); }
       return (-1073741670L);
     } else {
     }
@@ -2848,9 +2828,7 @@ NTSTATUS DiskPerfRegisterDevice(PDEVICE_OBJECT DeviceObject) {
         output = tmp;
       }
       if (!output) {
-        {
-          DiskPerfLogError(DeviceObject, 257, 0L, -1073479678L);
-        }
+        { DiskPerfLogError(DeviceObject, 257, 0L, -1073479678L); }
         return (-1073741670L);
       } else {
       }
@@ -2885,9 +2863,7 @@ NTSTATUS DiskPerfRegisterDevice(PDEVICE_OBJECT DeviceObject) {
           output = tmp___0;
         }
         if (!output) {
-          {
-            DiskPerfLogError(DeviceObject, 258, 0L, -1073479678L);
-          }
+          { DiskPerfLogError(DeviceObject, 258, 0L, -1073479678L); }
           return (-1073741670L);
         } else {
         }
@@ -2944,9 +2920,7 @@ NTSTATUS DiskPerfRegisterDevice(PDEVICE_OBJECT DeviceObject) {
             sizeof(VOLUME_NUMBER), 0, &event, &ioStatus);
       }
       if (!irp) {
-        {
-          DiskPerfLogError(DeviceObject, 265, 0L, -1073479678L);
-        }
+        { DiskPerfLogError(DeviceObject, 265, 0L, -1073479678L); }
         return (-1073741670L);
       } else {
       }
@@ -2983,9 +2957,7 @@ NTSTATUS DiskPerfRegisterDevice(PDEVICE_OBJECT DeviceObject) {
     }
     { status = IoWMIRegistrationControl(DeviceObject, 1UL | registrationFlag); }
     if (!(status >= 0L)) {
-      {
-        DiskPerfLogError(DeviceObject, 261, 0L, -1073479668L);
-      }
+      { DiskPerfLogError(DeviceObject, 261, 0L, -1073479668L); }
     } else {
     }
     return (status);
@@ -3156,9 +3128,7 @@ NTSTATUS DiskperfWmiFunctionControl(PDEVICE_OBJECT DeviceObject, PIRP Irp,
     if (GuidIndex == 0UL) {
       if ((int)Function == 1) {
         if (Enable) {
-          {
-            tmp = InterlockedIncrement(&deviceExtension->CountersEnabled);
-          }
+          { tmp = InterlockedIncrement(&deviceExtension->CountersEnabled); }
           if (tmp == 1L) {
             if ((unsigned int)deviceExtension->DiskCounters !=
                 (unsigned int)((void *)0)) {
@@ -3381,9 +3351,7 @@ int main(void) {
             if (s != SKIP2) {
               if (s != IPC) {
                 if (s != DC) {
-                  {
-                    errorFn();
-                  }
+                  { errorFn(); }
                 } else {
                   goto _L___0;
                 }
@@ -3394,24 +3362,18 @@ int main(void) {
             _L___0: /* CIL Label */
               if (pended == 1) {
                 if (status != 259L) {
-                  {
-                    errorFn();
-                  }
+                  { errorFn(); }
                 } else {
                 }
               } else {
                 if (s == DC) {
                   if (status == 259L) {
-                    {
-                      errorFn();
-                    }
+                    { errorFn(); }
                   } else {
                   }
                 } else {
                   if (status != (NTSTATUS)lowerDriverReturn) {
-                    {
-                      errorFn();
-                    }
+                    { errorFn(); }
                   } else {
                   }
                 }
@@ -3851,9 +3813,7 @@ NTSTATUS IofCallDriver(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
         }
       }
       if ((long)compRetStatus == -1073741802L) {
-        {
-          stubMoreProcessingRequired();
-        }
+        { stubMoreProcessingRequired(); }
       } else {
       }
     } else {
@@ -4007,9 +3967,7 @@ NTSTATUS KeWaitForSingleObject(PVOID Object, KWAIT_REASON WaitReason,
         customIrp = 0;
       } else {
         if (s == MPR3) {
-          {
-            errorFn();
-          }
+          { errorFn(); }
         } else {
         }
       }
@@ -4155,9 +4113,7 @@ NTSTATUS PoCallDriver(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
         }
       }
       if ((long)compRetStatus == -1073741802L) {
-        {
-          stubMoreProcessingRequired();
-        }
+        { stubMoreProcessingRequired(); }
       } else {
       }
     } else {
diff --git a/test/c/ntdrivers/kbfiltr_false.i.cil.c b/test/c/ntdrivers/kbfiltr_false.i.cil.c
index 70f9ab73b..ad13bc678 100644
--- a/test/c/ntdrivers/kbfiltr_false.i.cil.c
+++ b/test/c/ntdrivers/kbfiltr_false.i.cil.c
@@ -2064,14 +2064,10 @@ NTSTATUS KbFilter_PnP(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                                                    * event, 0, 0); */ /* INLINED */
                                                 }
                                                   if (s != NP) {
-                                                    {
-                                                      errorFn();
-                                                    }
+                                                    { errorFn(); }
                                                   } else {
                                                     if (compRegistered != 0) {
-                                                      {
-                                                        errorFn();
-                                                      }
+                                                      { errorFn(); }
                                                     } else {
                                                       compRegistered = 1;
                                                       compFptr =
@@ -2576,17 +2572,13 @@ int main(void) {
             _L___0: /* CIL Label */
               if (pended == 1) {
                 if (status != 259L) {
-                  {
-                    errorFn();
-                  }
+                  { errorFn(); }
                 } else {
                 }
               } else {
                 if (s == DC) {
                   if (status == 259L) {
-                    {
-                      errorFn();
-                    }
+                    { errorFn(); }
                   } else {
                   }
                 } else {
@@ -3023,9 +3015,7 @@ NTSTATUS IofCallDriver(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
         compRetStatus = tmp;
       }
       if ((long)compRetStatus == -1073741802L) {
-        {
-          stubMoreProcessingRequired();
-        }
+        { stubMoreProcessingRequired(); }
       } else {
       }
     } else {
@@ -3179,9 +3169,7 @@ NTSTATUS KeWaitForSingleObject(PVOID Object, KWAIT_REASON WaitReason,
         customIrp = 0;
       } else {
         if (s == MPR3) {
-          {
-            errorFn();
-          }
+          { errorFn(); }
         } else {
         }
       }
@@ -3316,9 +3304,7 @@ NTSTATUS PoCallDriver(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
         compRetStatus = tmp;
       }
       if ((long)compRetStatus == -1073741802L) {
-        {
-          stubMoreProcessingRequired();
-        }
+        { stubMoreProcessingRequired(); }
       } else {
       }
     } else {
diff --git a/test/c/ntdrivers/parport_false.i.cil.c b/test/c/ntdrivers/parport_false.i.cil.c
index 8f6290522..b2076c5c9 100644
--- a/test/c/ntdrivers/parport_false.i.cil.c
+++ b/test/c/ntdrivers/parport_false.i.cil.c
@@ -2617,9 +2617,7 @@ void PptLogError(PDRIVER_OBJECT DriverObject, PDEVICE_OBJECT DeviceObject,
     ErrorLogEntry->FinalStatus = FinalStatus;
     ErrorLogEntry->DumpDataSize = DumpToAllocate;
     if (DumpToAllocate) {
-      {
-        memcpy(ErrorLogEntry->DumpData, &P1, sizeof(PHYSICAL_ADDRESS));
-      }
+      { memcpy(ErrorLogEntry->DumpData, &P1, sizeof(PHYSICAL_ADDRESS)); }
       if ((unsigned int)DumpToAllocate > sizeof(PHYSICAL_ADDRESS)) {
         {
           memcpy((UCHAR *)(ErrorLogEntry->DumpData) + sizeof(PHYSICAL_ADDRESS),
@@ -2672,8 +2670,7 @@ NTSTATUS DriverEntry(PDRIVER_OBJECT DriverObject,
           ExAllocatePoolWithTag(1, pRegistryPath->MaximumLength, 1349673296UL);
     }
     if ((unsigned int)((void *)0) == (unsigned int)Buffer) {
-      {
-      }
+      {}
       return (-1073741670L);
     } else {
       {
@@ -2721,9 +2718,7 @@ void PptUnload(PDRIVER_OBJECT DriverObject) {
         }
         Extension = CurrentDevice->DeviceExtension;
         if (Extension->InterruptRefCount) {
-          {
-            PptDisconnectInterrupt(Extension);
-          }
+          { PptDisconnectInterrupt(Extension); }
         } else {
         }
         {
@@ -2860,8 +2855,7 @@ PptAddPptRemovalRelation(PDEVICE_EXTENSION Extension,
     }
     {}
     if (!node) {
-      {
-      }
+      {}
       return (-1073741670L);
     } else {
     }
@@ -2957,19 +2951,16 @@ PptRemovePptRemovalRelation(PDEVICE_EXTENSION Extension,
                        (unsigned long)(&((REMOVAL_RELATIONS_LIST_ENTRY *)0)
                                             ->ListEntry));
         if ((unsigned int)node->DeviceObject == (unsigned int)callerDevObj) {
-          {
-          }
+          {}
           found = 1;
           done = 1;
         } else {
           if ((unsigned int)firstListEntry == (unsigned int)thisListEntry) {
-            {
-            }
+            {}
             done = 1;
           } else {
             if (!firstListEntry) {
-              {
-              }
+              {}
               firstListEntry = thisListEntry;
             } else {
             }
@@ -3126,8 +3117,7 @@ NTSTATUS PptDispatchInternalDeviceControl(PDEVICE_OBJECT DeviceObject,
     }
     { Status = PptAcquireRemoveLockOrFailIrp(DeviceObject, Irp); }
     if (!(Status >= 0L)) {
-      {
-      }
+      {}
       return (Status);
     } else {
     }
@@ -3206,8 +3196,7 @@ NTSTATUS PptDispatchInternalDeviceControl(PDEVICE_OBJECT DeviceObject,
                                               .InputBufferLength <
                                           (ULONG)sizeof(
                                               PARPORT_REMOVAL_RELATIONS)) {
-                                        {
-                                        }
+                                        {}
                                         Status = -1073741789L;
                                       } else {
                                         {
@@ -3240,8 +3229,7 @@ NTSTATUS PptDispatchInternalDeviceControl(PDEVICE_OBJECT DeviceObject,
                                               .InputBufferLength <
                                           (ULONG)sizeof(
                                               PARPORT_REMOVAL_RELATIONS)) {
-                                        {
-                                        }
+                                        {}
                                         Status = -1073741789L;
                                       } else {
                                         {
@@ -3415,8 +3403,7 @@ NTSTATUS PptDispatchInternalDeviceControl(PDEVICE_OBJECT DeviceObject,
                                       EnableConnectInterruptIoctl = 0;
                                       {}
                                       if (0UL == EnableConnectInterruptIoctl) {
-                                        {
-                                        }
+                                        {}
                                         Status = -1073741823L;
                                         goto targetExit;
                                       } else {
@@ -3578,9 +3565,7 @@ NTSTATUS PptDispatchInternalDeviceControl(PDEVICE_OBJECT DeviceObject,
                                           }
                                         }
                                         if (DisconnectInterrupt) {
-                                          {
-                                            PptDisconnectInterrupt(Extension);
-                                          }
+                                          { PptDisconnectInterrupt(Extension); }
                                         } else {
                                         }
                                       }
@@ -3631,8 +3616,7 @@ NTSTATUS PptDispatchInternalDeviceControl(PDEVICE_OBJECT DeviceObject,
                                               .InputBufferLength <
                                           (ULONG)sizeof(
                                               PARALLEL_1284_COMMAND)) {
-                                        {
-                                        }
+                                        {}
                                         Status = -1073741789L;
                                       } else {
                                         if (Irp->Cancel) {
@@ -3700,8 +3684,7 @@ NTSTATUS PptDispatchInternalDeviceControl(PDEVICE_OBJECT DeviceObject,
                                               .InputBufferLength <
                                           (ULONG)sizeof(
                                               PARALLEL_1284_COMMAND)) {
-                                        {
-                                        }
+                                        {}
                                         Status = -1073741789L;
                                       } else {
                                         {
@@ -3882,8 +3865,7 @@ NTSTATUS PptDispatchCreate(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
     }
     { status = PptAcquireRemoveLockOrFailIrp(DeviceObject, Irp); }
     if (!(status >= 0L)) {
-      {
-      }
+      {}
       return (status);
     } else {
     }
@@ -3933,13 +3915,9 @@ NTSTATUS PptDispatchClose(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
     { /*   ExAcquireFastMutex(& extension->OpenCloseMutex); */ /* INLINED */
     }
     if (extension->OpenCloseRefCount > 0L) {
-      {
-        tmp = InterlockedDecrement(&extension->OpenCloseRefCount);
-      }
+      { tmp = InterlockedDecrement(&extension->OpenCloseRefCount); }
       if (tmp < 0L) {
-        {
-          InterlockedIncrement(&extension->OpenCloseRefCount);
-        }
+        { InterlockedIncrement(&extension->OpenCloseRefCount); }
       } else {
       }
       {
@@ -4050,15 +4028,11 @@ NTSTATUS PptTrySelectDevice(PVOID Context, PVOID TrySelectCommand) {
     success = 0;
     {}
     if (Command->CommandFlags & 4UL) {
-      {
-        tmp = PptTrySelectLegacyZip(Context, TrySelectCommand);
-      }
+      { tmp = PptTrySelectLegacyZip(Context, TrySelectCommand); }
       return (tmp);
     } else {
       if ((int)Command->ID == 5) {
-        {
-          tmp = PptTrySelectLegacyZip(Context, TrySelectCommand);
-        }
+        { tmp = PptTrySelectLegacyZip(Context, TrySelectCommand); }
         return (tmp);
       } else {
       }
@@ -4066,8 +4040,7 @@ NTSTATUS PptTrySelectDevice(PVOID Context, PVOID TrySelectCommand) {
     DeviceID = Command->ID;
     if (!(Command->CommandFlags & 1UL)) {
       if ((ULONG)DeviceID > Extension->PnpInfo.Ieee1284_3DeviceCount) {
-        {
-        }
+        {}
         Status = -1073741811L;
       } else {
         goto _L___1;
@@ -4100,8 +4073,7 @@ NTSTATUS PptTrySelectDevice(PVOID Context, PVOID TrySelectCommand) {
             while_79_break: /* CIL Label */;
             }
             if (success) {
-              {
-              }
+              {}
               Status = 0L;
             } else {
               {}
@@ -4163,8 +4135,7 @@ NTSTATUS PptTrySelectDevice(PVOID Context, PVOID TrySelectCommand) {
               while_85_break: /* CIL Label */;
               }
               if (success) {
-                {
-                }
+                {}
                 Status = 0L;
               } else {
                 {}
@@ -4200,15 +4171,11 @@ NTSTATUS PptDeselectDevice(PVOID Context, PVOID DeselectCommand) {
     success = 0;
     {}
     if (Command->CommandFlags & 4UL) {
-      {
-        tmp = PptDeselectLegacyZip(Context, DeselectCommand);
-      }
+      { tmp = PptDeselectLegacyZip(Context, DeselectCommand); }
       return (tmp);
     } else {
       if ((int)Command->ID == 5) {
-        {
-          tmp = PptDeselectLegacyZip(Context, DeselectCommand);
-        }
+        { tmp = PptDeselectLegacyZip(Context, DeselectCommand); }
         return (tmp);
       } else {
       }
@@ -4216,8 +4183,7 @@ NTSTATUS PptDeselectDevice(PVOID Context, PVOID DeselectCommand) {
     DeviceID = Command->ID;
     if (!(Command->CommandFlags & 1UL)) {
       if ((ULONG)DeviceID > Extension->PnpInfo.Ieee1284_3DeviceCount) {
-        {
-        }
+        {}
         Status = -1073741811L;
       } else {
         goto _L___0;
@@ -4248,12 +4214,9 @@ NTSTATUS PptDeselectDevice(PVOID Context, PVOID DeselectCommand) {
           while_91_break: /* CIL Label */;
           }
           if (success) {
-            {
-            }
+            {}
             if (!(Command->CommandFlags & 2UL)) {
-              {
-                PptFreePort(Extension);
-              }
+              { PptFreePort(Extension); }
             } else {
             }
             Status = 0L;
@@ -4268,9 +4231,7 @@ NTSTATUS PptDeselectDevice(PVOID Context, PVOID DeselectCommand) {
       _L : /* CIL Label */
       {}
         if (!(Command->CommandFlags & 2UL)) {
-          {
-            PptFreePort(Extension);
-          }
+          { PptFreePort(Extension); }
         } else {
         }
         Status = 0L;
@@ -4327,9 +4288,7 @@ ULONG Ppt1284_3AssignAddress(PDEVICE_EXTENSION DeviceExtension) {
           status = READ_PORT_UCHAR(CurrentStatus);
         }
         if (((int)status & 48) == 48) {
-          {
-            KeStallExecutionProcessor(Delay);
-          }
+          { KeStallExecutionProcessor(Delay); }
           {
             while (1) {
             while_95_continue: /* CIL Label */;
@@ -4389,9 +4348,7 @@ ULONG Ppt1284_3AssignAddress(PDEVICE_EXTENSION DeviceExtension) {
                 } else {
                 }
                 if (1 == (int)bStlNon1284_3Found) {
-                  {
-                    tmp___1 = PptCheckIfStlProductId(DeviceExtension, idx);
-                  }
+                  { tmp___1 = PptCheckIfStlProductId(DeviceExtension, idx); }
                   if (1 == (int)tmp___1) {
                     bStlNon1284_3Valid = 1;
                     goto __Cont;
@@ -4812,8 +4769,7 @@ BOOLEAN PptSend1284_3Command(PDEVICE_EXTENSION DeviceExtension, UCHAR Command) {
                   } else {
                   }
                   if (!success) {
-                    {
-                    }
+                    {}
                   } else {
                   }
                   goto switch_99_break;
@@ -4827,8 +4783,7 @@ BOOLEAN PptSend1284_3Command(PDEVICE_EXTENSION DeviceExtension, UCHAR Command) {
                   } else {
                   }
                   if (!success) {
-                    {
-                    }
+                    {}
                   } else {
                   }
                   goto switch_99_break;
@@ -5016,9 +4971,7 @@ NTSTATUS PptDetectPortCapabilities(PDEVICE_EXTENSION Extension) {
           if (!Extension->NationalChipFound) {
             {} {} { PptDetectEppPortIfDot3DevicePresent(Extension); }
             if (!Extension->CheckedForGenericEpp) {
-              {
-                PptDetectEppPortIfUserRequested(Extension);
-              }
+              { PptDetectEppPortIfUserRequested(Extension); }
             } else {
             }
           } else {
@@ -5037,8 +4990,7 @@ NTSTATUS PptDetectPortCapabilities(PDEVICE_EXTENSION Extension) {
     }
     {} { PptDetectBytePort(Extension); }
     if (Extension->PnpInfo.HardwareCapabilities & 11UL) {
-      {
-      }
+      {}
       return (0L);
     } else {
     }
@@ -5059,8 +5011,7 @@ void PptDetectEcpPort(PDEVICE_EXTENSION Extension) {
     wPortDCR = Controller + 2;
     if ((unsigned int)((PUCHAR)0) ==
         (unsigned int)Extension->PnpInfo.EcpController) {
-      {
-      }
+      {}
       return;
     } else {
     }
@@ -5151,8 +5102,7 @@ void PptDetectEppPortIfDot3DevicePresent(PDEVICE_EXTENSION Extension) {
     Forward = (unsigned char)6;
     daisyChainDevicePresent = 0;
     if (0UL == Extension->PnpInfo.Ieee1284_3DeviceCount) {
-      {
-      }
+      {}
       return;
     } else {
     }
@@ -5163,8 +5113,7 @@ void PptDetectEppPortIfDot3DevicePresent(PDEVICE_EXTENSION Extension) {
       status = PptTrySelectDevice(Extension, &Command);
     }
     if (!(status >= 0L)) {
-      {
-      }
+      {}
       return;
     } else {
     }
@@ -5176,8 +5125,7 @@ void PptDetectEppPortIfDot3DevicePresent(PDEVICE_EXTENSION Extension) {
       status = PptDeselectDevice(Extension, &Command);
     }
     if (!(status >= 0L)) {
-      {
-      }
+      {}
     } else {
       {}
     }
@@ -5190,9 +5138,7 @@ void PptDetectEppPortIfUserRequested(PDEVICE_EXTENSION Extension) {
   {
     RequestEppTest = 0;
     if (RequestEppTest) {
-      {
-        PptDetectEppPort(Extension);
-      }
+      { PptDetectEppPort(Extension); }
     } else {
     }
     return;
@@ -5237,8 +5183,7 @@ void PptDetectEppPort(PDEVICE_EXTENSION Extension) {
       Extension->CheckedForGenericEpp = 1;
     }
     if (Extension->PnpInfo.HardwareCapabilities & 2UL) {
-      {
-      }
+      {}
     } else {
       {}
     }
@@ -5252,8 +5197,7 @@ void PptDetectBytePort(PDEVICE_EXTENSION Extension) {
     Status = 0L;
     {} { Status = PptSetByteMode(Extension, 52); }
     if (Status >= 0L) {
-      {
-      }
+      {}
       Extension->PnpInfo.HardwareCapabilities |= 8UL;
     } else {
       {}
@@ -5329,9 +5273,7 @@ void PptDetermineFifoDepth(PDEVICE_EXTENSION Extension) {
           }
           { testData = READ_PORT_UCHAR(wPortDFIFO); }
           if ((int)testData != ((int)readFifoDepth & 255)) {
-            {
-              WRITE_PORT_UCHAR(wPortECR, ecrLast);
-            }
+            { WRITE_PORT_UCHAR(wPortECR, ecrLast); }
             {}
             return;
           } else {
@@ -5387,8 +5329,7 @@ NTSTATUS PptSetChipMode(PDEVICE_EXTENSION Extension, UCHAR ChipMode) {
     EcrMode = (unsigned char)((int)ChipMode & -32);
     {}
     if (Extension->PnpInfo.CurrentMode != 0UL) {
-      {
-      }
+      {}
       Status = -1073741436L;
       goto ExitSetChipModeNoChange;
     } else {
@@ -5402,8 +5343,7 @@ NTSTATUS PptSetChipMode(PDEVICE_EXTENSION Extension, UCHAR ChipMode) {
       {}
       if ((int)EcrMode == 96) {
         if ((Extension->PnpInfo.HardwareCapabilities & 1UL) ^ 1UL) {
-          {
-          }
+          {}
           return (-1073741810L);
         } else {
         }
@@ -5413,8 +5353,7 @@ NTSTATUS PptSetChipMode(PDEVICE_EXTENSION Extension, UCHAR ChipMode) {
       }
       if ((int)EcrMode == 128) {
         if ((Extension->PnpInfo.HardwareCapabilities & 2UL) ^ 2UL) {
-          {
-          }
+          {}
           return (-1073741810L);
         } else {
         }
@@ -5424,8 +5363,7 @@ NTSTATUS PptSetChipMode(PDEVICE_EXTENSION Extension, UCHAR ChipMode) {
       }
       if ((int)EcrMode == 32) {
         if ((Extension->PnpInfo.HardwareCapabilities & 8UL) ^ 8UL) {
-          {
-          }
+          {}
           return (-1073741810L);
         } else {
         }
@@ -5436,8 +5374,7 @@ NTSTATUS PptSetChipMode(PDEVICE_EXTENSION Extension, UCHAR ChipMode) {
     }
   ExitSetChipModeWithChanges:
     if (Status >= 0L) {
-      {
-      }
+      {}
       Extension->PnpInfo.CurrentMode = EcrMode;
     } else {
       {}
@@ -5455,8 +5392,7 @@ NTSTATUS PptClearChipMode(PDEVICE_EXTENSION Extension, UCHAR ChipMode) {
     EcrMode = (int)ChipMode & -32;
     {}
     if (EcrMode != Extension->PnpInfo.CurrentMode) {
-      {
-      }
+      {}
       Status = -1073741436L;
       goto ExitClearChipModeNoChange;
     } else {
@@ -5469,31 +5405,24 @@ NTSTATUS PptClearChipMode(PDEVICE_EXTENSION Extension, UCHAR ChipMode) {
     } else {
       {}
       if (EcrMode == 96UL) {
-        {
-          Status = PptEcrClearMode(Extension);
-        }
+        { Status = PptEcrClearMode(Extension); }
         goto ExitClearChipModeWithChanges;
       } else {
       }
       if (EcrMode == 128UL) {
-        {
-          Status = PptEcrClearMode(Extension);
-        }
+        { Status = PptEcrClearMode(Extension); }
         goto ExitClearChipModeWithChanges;
       } else {
       }
       if (EcrMode == 32UL) {
-        {
-          Status = PptClearByteMode(Extension);
-        }
+        { Status = PptClearByteMode(Extension); }
         goto ExitClearChipModeWithChanges;
       } else {
       }
     }
   ExitClearChipModeWithChanges:
     if (Status >= 0L) {
-      {
-      }
+      {}
       Extension->PnpInfo.CurrentMode = 0;
     } else {
     }
@@ -5526,9 +5455,7 @@ NTSTATUS PptSetByteMode(PDEVICE_EXTENSION Extension, UCHAR ChipMode) {
 
   {
     if (Extension->PnpInfo.HardwareCapabilities & 1UL) {
-      {
-        Status = PptEcrSetMode(Extension, ChipMode);
-      }
+      { Status = PptEcrSetMode(Extension, ChipMode); }
     } else {
     }
     { Status = PptCheckByteMode(Extension); }
@@ -5541,9 +5468,7 @@ NTSTATUS PptClearByteMode(PDEVICE_EXTENSION Extension) {
   {
     Status = 0L;
     if (Extension->PnpInfo.HardwareCapabilities & 1UL) {
-      {
-        Status = PptEcrClearMode(Extension);
-      }
+      { Status = PptEcrClearMode(Extension); }
     } else {
     }
     return (Status);
@@ -5637,8 +5562,7 @@ NTSTATUS PptFindNatChip(PDEVICE_EXTENSION Extension) {
     NationalChecked = 0;
     NationalChipFound = 0;
     if ((int)Extension->NationalChecked == 1) {
-      {
-      }
+      {}
       return (0L);
     } else {
     }
@@ -5661,8 +5585,7 @@ NTSTATUS PptFindNatChip(PDEVICE_EXTENSION Extension) {
       Resources = (struct _CM_RESOURCE_LIST *)tmp;
     }
     if ((unsigned int)Resources == (unsigned int)((void *)0)) {
-      {
-      }
+      {}
       return (-1073741823L);
     } else {
     }
@@ -5684,14 +5607,12 @@ NTSTATUS PptFindNatChip(PDEVICE_EXTENSION Extension) {
       /*   ExFreePool(Resources); */ /* INLINED */
     }
     if (!(Status >= 0L)) {
-      {
-      }
+      {}
       return (Status);
     } else {
     }
     if (Conflict) {
-      {
-      }
+      {}
       return (-1073741823L);
     } else {
     }
@@ -5713,9 +5634,7 @@ NTSTATUS PptFindNatChip(PDEVICE_EXTENSION Extension) {
           tmp___1 = READ_PORT_UCHAR(PortAddr);
         }
         if ((int)tmp___1 == 136) {
-          {
-            tmp___2 = READ_PORT_UCHAR(PortAddr);
-          }
+          { tmp___2 = READ_PORT_UCHAR(PortAddr); }
           if ((int)tmp___2 < 32) {
             OkToLook = 1;
           } else {
@@ -5728,9 +5647,7 @@ NTSTATUS PptFindNatChip(PDEVICE_EXTENSION Extension) {
           cr = READ_PORT_UCHAR(PortAddr);
         }
           if ((int)cr != 255) {
-            {
-              tmp___0 = READ_PORT_UCHAR(PortAddr);
-            }
+            { tmp___0 = READ_PORT_UCHAR(PortAddr); }
             if ((int)tmp___0 == (int)cr) {
               OkToLook = 1;
             } else {
@@ -6022,8 +5939,7 @@ PDEVICE_RELATIONS PptPnpBuildRemovalRelations(PDEVICE_EXTENSION Extension) {
       /*   ExAcquireFastMutex(& Extension->ExtensionFastMutex); */ /* INLINED */
     }
     if ((unsigned int)listHead->Flink == (unsigned int)listHead) {
-      {
-      }
+      {}
       goto targetExit;
     } else {
     }
@@ -6065,8 +5981,7 @@ PDEVICE_RELATIONS PptPnpBuildRemovalRelations(PDEVICE_EXTENSION Extension) {
           count += 1UL;
         }
         if (!firstListEntry) {
-          {
-          }
+          {}
           firstListEntry = thisListEntry;
         } else {
         }
@@ -6082,8 +5997,7 @@ PDEVICE_RELATIONS PptPnpBuildRemovalRelations(PDEVICE_EXTENSION Extension) {
       relations = tmp;
     }
     if (!relations) {
-      {
-      }
+      {}
       goto targetExit;
     } else {
     }
@@ -6293,15 +6207,13 @@ BOOLEAN PptIsPci(PDEVICE_EXTENSION Extension, PIRP Irp) {
     ResourceList =
         irpStack->Parameters.StartDevice.AllocatedResourcesTranslated;
     if ((unsigned int)ResourceList == (unsigned int)((void *)0)) {
-      {
-      }
+      {}
       return (0);
     } else {
     }
     FullResourceDescriptor = &ResourceList->List[0];
     if (FullResourceDescriptor) {
-      {
-      }
+      {}
       PartialResourceList = &FullResourceDescriptor->PartialResourceList;
       i = 0;
       {
@@ -6325,8 +6237,7 @@ BOOLEAN PptIsPci(PDEVICE_EXTENSION Extension, PIRP Irp) {
                 {}
                 portResourceDescriptorCount += 1UL;
                 if (rangeLength > 8UL) {
-                  {
-                  }
+                  {}
                   largePortRangeFound = 1;
                 } else {
                 }
@@ -6399,8 +6310,7 @@ NTSTATUS PptPnpAddDevice(PDRIVER_OBJECT pDriverObject,
           PptBuildDeviceObject(pDriverObject, pPhysicalDeviceObject);
     }
     if ((unsigned int)((void *)0) == (unsigned int)pDeviceObject) {
-      {
-      }
+      {}
       return (-1073741823L);
     } else {
     }
@@ -6452,9 +6362,7 @@ NTSTATUS PptDispatchPnp(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                      .CurrentStackLocation;
       minorFunction = irpStack->MinorFunction;
       if ((int)minorFunction > 24) {
-        {
-          status = PptPnpUnhandledIrp(DeviceObject, Irp);
-        }
+        { status = PptPnpUnhandledIrp(DeviceObject, Irp); }
       } else {
         if (__BLAST_NONDET == 0) {
           goto switch_214_0;
@@ -6614,9 +6522,7 @@ NTSTATUS PptPnpStartDevice(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
       status = PptDetectChipFilter(extension);
     }
     if (!(status >= 0L)) {
-      {
-        PptDetectPortType(extension);
-      }
+      { PptDetectPortType(extension); }
     } else {
     }
     { status = PptWmiInitWmi(DeviceObject); }
@@ -6678,17 +6584,14 @@ NTSTATUS PptPnpStartScanCmResourceList(PDEVICE_EXTENSION Extension, PIRP Irp,
     ResourceList =
         irpStack->Parameters.StartDevice.AllocatedResourcesTranslated;
     if ((unsigned int)ResourceList == (unsigned int)((void *)0)) {
-      {
-      }
+      {}
       status = -1073741670L;
       goto targetExit;
     } else {
     }
     if ((int)((KUSER_SHARED_DATA *const)4292804608U)->AlternativeArchitecture !=
         1) {
-      {
-        tmp = PptIsPci(Extension, Irp);
-      }
+      { tmp = PptIsPci(Extension, Irp); }
       if (1 == (int)tmp) {
         {} {
           status = PptPnpStartScanPciCardCmResourceList(
@@ -6738,8 +6641,7 @@ NTSTATUS PptPnpStartScanCmResourceList(PDEVICE_EXTENSION Extension, PIRP Irp,
                               .__annonCompField1.LowPart == 0UL) {
                         if (Extension->PortInfo.OriginalController
                                 .__annonCompField1.HighPart == 0L) {
-                          {
-                          }
+                          {}
                           Extension->PortInfo.OriginalController =
                               PartialResourceDescriptor->u.Port.Start;
                           Extension->PortInfo.SpanOfController =
@@ -6750,9 +6652,7 @@ NTSTATUS PptPnpStartScanCmResourceList(PDEVICE_EXTENSION Extension, PIRP Irp,
                           Extension->AddressSpace =
                               PartialResourceDescriptor->Flags;
                           if (Extension->PortInfo.SpanOfController == 4096UL) {
-                            {
-                              tmp___0 = PptIsNecR98Machine();
-                            }
+                            { tmp___0 = PptIsNecR98Machine(); }
                             if (tmp___0) {
                               Extension->PortInfo.SpanOfController = 8;
                             } else {
@@ -6778,8 +6678,7 @@ NTSTATUS PptPnpStartScanCmResourceList(PDEVICE_EXTENSION Extension, PIRP Irp,
                                         .__annonCompField1.HighPart <
                                     Extension->PortInfo.OriginalController
                                         .__annonCompField1.HighPart) {
-                                  {
-                                  }
+                                  {}
                                   Extension->PnpInfo.OriginalEcpController =
                                       Extension->PortInfo.OriginalController;
                                   Extension->PnpInfo.SpanOfEcpController =
@@ -6800,9 +6699,7 @@ NTSTATUS PptPnpStartScanCmResourceList(PDEVICE_EXTENSION Extension, PIRP Irp,
                                       PartialResourceDescriptor->Flags;
                                   if (Extension->PortInfo.SpanOfController ==
                                       4096UL) {
-                                    {
-                                      tmp___1 = PptIsNecR98Machine();
-                                    }
+                                    { tmp___1 = PptIsNecR98Machine(); }
                                     if (tmp___1) {
                                       Extension->PortInfo.SpanOfController = 8;
                                     } else {
@@ -7055,8 +6952,7 @@ BOOLEAN PptPnpFilterExistsNonIrqResourceList(
             }
             {}
             if ((int)curDesc->Type == 2) {
-              {
-              }
+              {}
               foundIrq = 1;
               goto while_243_break;
             } else {
@@ -7067,8 +6963,7 @@ BOOLEAN PptPnpFilterExistsNonIrqResourceList(
         while_243_break: /* CIL Label */;
         }
         if ((int)foundIrq == 0) {
-          {
-          }
+          {}
           return (1);
         } else {
         }
@@ -7112,8 +7007,7 @@ void PptPnpFilterRemoveIrqResourceLists(
         }
         {} {} { tmp___0 = PptPnpListContainsIrqResourceDescriptor(curList); }
         if (tmp___0) {
-          {
-          }
+          {}
           nextList = (struct _IO_RESOURCE_LIST *)(curList->Descriptors +
                                                   curList->Count);
           bytesToMove =
@@ -7259,15 +7153,13 @@ NTSTATUS PptPnpQueryDeviceRelations(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                 switch_261_3: /* CIL Label */;
                   {} { PptDumpRemovalRelationsList(extension); }
                   if (Irp->IoStatus.Information) {
-                    {
-                    }
+                    {}
                   } else {
                     {
                       removalRelations = PptPnpBuildRemovalRelations(extension);
                     }
                     if (removalRelations) {
-                      {
-                      }
+                      {}
                       Irp->IoStatus.__annonCompField4.Status = 0L;
                       myStatus = 0L;
                       Irp->IoStatus.Information =
@@ -7535,14 +7427,10 @@ NTSTATUS PptPnpBounceAndCatchPnpIrp(PDEVICE_EXTENSION Extension, PIRP Irp) {
       nextIrpSp->Control = 0;
     }
     if (s != NP) {
-      {
-        errorFn();
-      }
+      { errorFn(); }
     } else {
       if (compRegistered != 0) {
-        {
-          errorFn();
-        }
+        { errorFn(); }
       } else {
         compRegistered = 1;
         compFptr = &PptSynchCompletionRoutine;
@@ -7805,9 +7693,7 @@ NTSTATUS PptDispatchPower(PDEVICE_OBJECT pDeviceObject, PIRP pIrp) {
                       hookit = 1;
                       if ((int)((KUSER_SHARED_DATA *const)4292804608U)
                               ->AlternativeArchitecture == 1) {
-                        {
-                          InitNEC_98(Extension);
-                        }
+                        { InitNEC_98(Extension); }
                       } else {
                       }
                     } else {
@@ -7868,14 +7754,10 @@ NTSTATUS PptDispatchPower(PDEVICE_OBJECT pDeviceObject, PIRP pIrp) {
     } else {
       if (hookit) {
         if (s != NP) {
-          {
-            errorFn();
-          }
+          { errorFn(); }
         } else {
           if (compRegistered != 0) {
-            {
-              errorFn();
-            }
+            { errorFn(); }
           } else {
             compRegistered = 1;
             compFptr = &PptPowerComplete;
@@ -8034,22 +7916,17 @@ NTSTATUS PptTrySelectLegacyZip(PVOID Context, PVOID TrySelectCommand) {
     if (Status >= 0L) {
       if (Status != 259L) {
         if (Command->CommandFlags & 32UL) {
-          {
-            PptLegacyZipSetDiskMode(Controller, (unsigned char)207);
-          }
+          { PptLegacyZipSetDiskMode(Controller, (unsigned char)207); }
         } else {
           { PptLegacyZipSetDiskMode(Controller, (unsigned char)143); }
         }
         { tmp = PptLegacyZipCheckDevice(Controller); }
         if (tmp) {
-          {
-          }
+          {}
           if (!Extension->CheckedForGenericEpp) {
             if (Extension->PnpInfo.HardwareCapabilities & 1UL) {
               if (!Extension->NationalChipFound) {
-                {
-                  PptDetectEppPort(Extension);
-                }
+                { PptDetectEppPort(Extension); }
               } else {
               }
             } else {
@@ -8085,9 +7962,7 @@ NTSTATUS PptDeselectLegacyZip(PVOID Context, PVOID DeselectCommand) {
       PptLegacyZipClockPrtModeByte(Controller, (unsigned char)15);
     }
     if (!(Command->CommandFlags & 2UL)) {
-      {
-        PptFreePort(Extension);
-      }
+      { PptFreePort(Extension); }
     } else {
     }
     return (0L);
@@ -8214,8 +8089,7 @@ NTSTATUS PptRegSetDeviceParameterDword(PDEVICE_OBJECT Pdo, PWSTR ParameterName,
   {
     { status = IoOpenDeviceRegistryKey(Pdo, 1, 131078L, &hKey); }
     if (!(status >= 0L)) {
-      {
-      }
+      {}
       return (status);
     } else {
     }
@@ -8225,8 +8099,7 @@ NTSTATUS PptRegSetDeviceParameterDword(PDEVICE_OBJECT Pdo, PWSTR ParameterName,
           ZwSetValueKey(hKey, &valueName, 0, 4, ParameterValue, sizeof(ULONG));
     }
     if (!(status >= 0L)) {
-      {
-      }
+      {}
     } else {
     }
     { ZwClose(hKey); }
@@ -8288,9 +8161,7 @@ NTSTATUS PptAcquireRemoveLockOrFailIrp(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
       status = tmp;
     }
     if (!(status >= 0L)) {
-      {
-        PptFailRequest(Irp, status);
-      }
+      { PptFailRequest(Irp, status); }
     } else {
     }
     return (status);
@@ -8350,8 +8221,7 @@ PWSTR PptGetPortNameFromPhysicalDeviceObject(
           IoOpenDeviceRegistryKey(PhysicalDeviceObject, 1, 2031616L, &hKey);
     }
     if (!(status >= 0L)) {
-      {
-      }
+      {}
       return ((void *)0);
     } else {
     }
@@ -8891,8 +8761,7 @@ NTSTATUS PptBuildParallelPortDeviceName(ULONG Number,
       status = RtlIntegerToUnicodeString(Number, 10, &uniPortNumberString);
     }
     if (!(status >= 0L)) {
-      {
-      }
+      {}
       return (status);
     } else {
     }
@@ -8906,8 +8775,7 @@ NTSTATUS PptBuildParallelPortDeviceName(ULONG Number,
       DeviceName->Buffer = tmp;
     }
     if ((unsigned int)((void *)0) == (unsigned int)DeviceName->Buffer) {
-      {
-      }
+      {}
       return (-1073741670L);
     } else {
     }
@@ -9000,8 +8868,7 @@ NTSTATUS PptGetPortNumberFromLptName(PWSTR PortName, PULONG PortNumber) {
 
   {
     if (__BLAST_NONDET) {
-      {
-      }
+      {}
       return (-1073741823L);
     } else {
     }
@@ -9010,14 +8877,12 @@ NTSTATUS PptGetPortNumberFromLptName(PWSTR PortName, PULONG PortNumber) {
       status = RtlUnicodeStringToInteger(&str, 10, PortNumber);
     }
     if (!(status >= 0L)) {
-      {
-      }
+      {}
       return (-1073741823L);
     } else {
     }
     if (*PortNumber == 0UL) {
-      {
-      }
+      {}
       return (-1073741823L);
     } else {
     }
@@ -9045,8 +8910,7 @@ PDEVICE_OBJECT PptBuildDeviceObject(PDRIVER_OBJECT DriverObject,
       portName = PptGetPortNameFromPhysicalDeviceObject(PhysicalDeviceObject);
     }
     if ((unsigned int)((void *)0) == (unsigned int)portName) {
-      {
-      }
+      {}
       goto targetExit;
     } else {
     }
@@ -9070,8 +8934,7 @@ PDEVICE_OBJECT PptBuildDeviceObject(PDRIVER_OBJECT DriverObject,
                               &uniNameString, 22, 256, 0, &deviceObject);
     }
     if (-1073741771L == status) {
-      {
-      }
+      {}
       portNumber = 7;
       {
         while (1) {
@@ -9509,9 +9372,7 @@ int main(void) {
         }
       }
       if (we_should_unload) {
-        {
-          PptUnload(&d);
-        }
+        { PptUnload(&d); }
       } else {
       }
     } else {
@@ -9541,9 +9402,7 @@ int main(void) {
             if (s != SKIP2) {
               if (s != IPC) {
                 if (s != DC) {
-                  {
-                    errorFn();
-                  }
+                  { errorFn(); }
                 } else {
                   goto _L___0;
                 }
@@ -9554,21 +9413,15 @@ int main(void) {
             _L___0: /* CIL Label */
               if (pended == 1) {
                 if (status != 259L) {
-                  {
-                    errorFn();
-                  }
+                  { errorFn(); }
                 } else {
                 }
               } else {
                 if (s == DC) {
-                  {
-                    errorFn();
-                  }
+                  { errorFn(); }
                 } else {
                   if (status != (NTSTATUS)lowerDriverReturn) {
-                    {
-                      errorFn();
-                    }
+                    { errorFn(); }
                   } else {
                   }
                 }
@@ -10012,9 +9865,7 @@ NTSTATUS IofCallDriver(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
         }
       }
       if ((long)compRetStatus == -1073741802L) {
-        {
-          stubMoreProcessingRequired();
-        }
+        { stubMoreProcessingRequired(); }
       } else {
       }
     } else {
@@ -10168,9 +10019,7 @@ NTSTATUS KeWaitForSingleObject(PVOID Object, KWAIT_REASON WaitReason,
         customIrp = 0;
       } else {
         if (s == MPR3) {
-          {
-            errorFn();
-          }
+          { errorFn(); }
         } else {
         }
       }
@@ -10316,9 +10165,7 @@ NTSTATUS PoCallDriver(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
         }
       }
       if ((long)compRetStatus == -1073741802L) {
-        {
-          stubMoreProcessingRequired();
-        }
+        { stubMoreProcessingRequired(); }
       } else {
       }
     } else {
diff --git a/test/c/ntdrivers/parport_true.i.cil.c b/test/c/ntdrivers/parport_true.i.cil.c
index 36921913e..7b3d33a73 100644
--- a/test/c/ntdrivers/parport_true.i.cil.c
+++ b/test/c/ntdrivers/parport_true.i.cil.c
@@ -2617,9 +2617,7 @@ void PptLogError(PDRIVER_OBJECT DriverObject, PDEVICE_OBJECT DeviceObject,
     ErrorLogEntry->FinalStatus = FinalStatus;
     ErrorLogEntry->DumpDataSize = DumpToAllocate;
     if (DumpToAllocate) {
-      {
-        memcpy(ErrorLogEntry->DumpData, &P1, sizeof(PHYSICAL_ADDRESS));
-      }
+      { memcpy(ErrorLogEntry->DumpData, &P1, sizeof(PHYSICAL_ADDRESS)); }
       if ((unsigned int)DumpToAllocate > sizeof(PHYSICAL_ADDRESS)) {
         {
           memcpy((UCHAR *)(ErrorLogEntry->DumpData) + sizeof(PHYSICAL_ADDRESS),
@@ -2672,8 +2670,7 @@ NTSTATUS DriverEntry(PDRIVER_OBJECT DriverObject,
           ExAllocatePoolWithTag(1, pRegistryPath->MaximumLength, 1349673296UL);
     }
     if ((unsigned int)((void *)0) == (unsigned int)Buffer) {
-      {
-      }
+      {}
       return (-1073741670L);
     } else {
       {
@@ -2721,9 +2718,7 @@ void PptUnload(PDRIVER_OBJECT DriverObject) {
         }
         Extension = CurrentDevice->DeviceExtension;
         if (Extension->InterruptRefCount) {
-          {
-            PptDisconnectInterrupt(Extension);
-          }
+          { PptDisconnectInterrupt(Extension); }
         } else {
         }
         {
@@ -2860,8 +2855,7 @@ PptAddPptRemovalRelation(PDEVICE_EXTENSION Extension,
     }
     {}
     if (!node) {
-      {
-      }
+      {}
       return (-1073741670L);
     } else {
     }
@@ -2957,19 +2951,16 @@ PptRemovePptRemovalRelation(PDEVICE_EXTENSION Extension,
                        (unsigned long)(&((REMOVAL_RELATIONS_LIST_ENTRY *)0)
                                             ->ListEntry));
         if ((unsigned int)node->DeviceObject == (unsigned int)callerDevObj) {
-          {
-          }
+          {}
           found = 1;
           done = 1;
         } else {
           if ((unsigned int)firstListEntry == (unsigned int)thisListEntry) {
-            {
-            }
+            {}
             done = 1;
           } else {
             if (!firstListEntry) {
-              {
-              }
+              {}
               firstListEntry = thisListEntry;
             } else {
             }
@@ -3126,8 +3117,7 @@ NTSTATUS PptDispatchInternalDeviceControl(PDEVICE_OBJECT DeviceObject,
     }
     { Status = PptAcquireRemoveLockOrFailIrp(DeviceObject, Irp); }
     if (!(Status >= 0L)) {
-      {
-      }
+      {}
       return (Status);
     } else {
     }
@@ -3206,8 +3196,7 @@ NTSTATUS PptDispatchInternalDeviceControl(PDEVICE_OBJECT DeviceObject,
                                               .InputBufferLength <
                                           (ULONG)sizeof(
                                               PARPORT_REMOVAL_RELATIONS)) {
-                                        {
-                                        }
+                                        {}
                                         Status = -1073741789L;
                                       } else {
                                         {
@@ -3240,8 +3229,7 @@ NTSTATUS PptDispatchInternalDeviceControl(PDEVICE_OBJECT DeviceObject,
                                               .InputBufferLength <
                                           (ULONG)sizeof(
                                               PARPORT_REMOVAL_RELATIONS)) {
-                                        {
-                                        }
+                                        {}
                                         Status = -1073741789L;
                                       } else {
                                         {
@@ -3415,8 +3403,7 @@ NTSTATUS PptDispatchInternalDeviceControl(PDEVICE_OBJECT DeviceObject,
                                       EnableConnectInterruptIoctl = 0;
                                       {}
                                       if (0UL == EnableConnectInterruptIoctl) {
-                                        {
-                                        }
+                                        {}
                                         Status = -1073741823L;
                                         goto targetExit;
                                       } else {
@@ -3578,9 +3565,7 @@ NTSTATUS PptDispatchInternalDeviceControl(PDEVICE_OBJECT DeviceObject,
                                           }
                                         }
                                         if (DisconnectInterrupt) {
-                                          {
-                                            PptDisconnectInterrupt(Extension);
-                                          }
+                                          { PptDisconnectInterrupt(Extension); }
                                         } else {
                                         }
                                       }
@@ -3631,8 +3616,7 @@ NTSTATUS PptDispatchInternalDeviceControl(PDEVICE_OBJECT DeviceObject,
                                               .InputBufferLength <
                                           (ULONG)sizeof(
                                               PARALLEL_1284_COMMAND)) {
-                                        {
-                                        }
+                                        {}
                                         Status = -1073741789L;
                                       } else {
                                         if (Irp->Cancel) {
@@ -3700,8 +3684,7 @@ NTSTATUS PptDispatchInternalDeviceControl(PDEVICE_OBJECT DeviceObject,
                                               .InputBufferLength <
                                           (ULONG)sizeof(
                                               PARALLEL_1284_COMMAND)) {
-                                        {
-                                        }
+                                        {}
                                         Status = -1073741789L;
                                       } else {
                                         {
@@ -3882,8 +3865,7 @@ NTSTATUS PptDispatchCreate(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
     }
     { status = PptAcquireRemoveLockOrFailIrp(DeviceObject, Irp); }
     if (!(status >= 0L)) {
-      {
-      }
+      {}
       return (status);
     } else {
     }
@@ -3933,13 +3915,9 @@ NTSTATUS PptDispatchClose(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
     { /*   ExAcquireFastMutex(& extension->OpenCloseMutex); */ /* INLINED */
     }
     if (extension->OpenCloseRefCount > 0L) {
-      {
-        tmp = InterlockedDecrement(&extension->OpenCloseRefCount);
-      }
+      { tmp = InterlockedDecrement(&extension->OpenCloseRefCount); }
       if (tmp < 0L) {
-        {
-          InterlockedIncrement(&extension->OpenCloseRefCount);
-        }
+        { InterlockedIncrement(&extension->OpenCloseRefCount); }
       } else {
       }
       {
@@ -4050,15 +4028,11 @@ NTSTATUS PptTrySelectDevice(PVOID Context, PVOID TrySelectCommand) {
     success = 0;
     {}
     if (Command->CommandFlags & 4UL) {
-      {
-        tmp = PptTrySelectLegacyZip(Context, TrySelectCommand);
-      }
+      { tmp = PptTrySelectLegacyZip(Context, TrySelectCommand); }
       return (tmp);
     } else {
       if ((int)Command->ID == 5) {
-        {
-          tmp = PptTrySelectLegacyZip(Context, TrySelectCommand);
-        }
+        { tmp = PptTrySelectLegacyZip(Context, TrySelectCommand); }
         return (tmp);
       } else {
       }
@@ -4066,8 +4040,7 @@ NTSTATUS PptTrySelectDevice(PVOID Context, PVOID TrySelectCommand) {
     DeviceID = Command->ID;
     if (!(Command->CommandFlags & 1UL)) {
       if ((ULONG)DeviceID > Extension->PnpInfo.Ieee1284_3DeviceCount) {
-        {
-        }
+        {}
         Status = -1073741811L;
       } else {
         goto _L___1;
@@ -4100,8 +4073,7 @@ NTSTATUS PptTrySelectDevice(PVOID Context, PVOID TrySelectCommand) {
             while_79_break: /* CIL Label */;
             }
             if (success) {
-              {
-              }
+              {}
               Status = 0L;
             } else {
               {}
@@ -4163,8 +4135,7 @@ NTSTATUS PptTrySelectDevice(PVOID Context, PVOID TrySelectCommand) {
               while_85_break: /* CIL Label */;
               }
               if (success) {
-                {
-                }
+                {}
                 Status = 0L;
               } else {
                 {}
@@ -4200,15 +4171,11 @@ NTSTATUS PptDeselectDevice(PVOID Context, PVOID DeselectCommand) {
     success = 0;
     {}
     if (Command->CommandFlags & 4UL) {
-      {
-        tmp = PptDeselectLegacyZip(Context, DeselectCommand);
-      }
+      { tmp = PptDeselectLegacyZip(Context, DeselectCommand); }
       return (tmp);
     } else {
       if ((int)Command->ID == 5) {
-        {
-          tmp = PptDeselectLegacyZip(Context, DeselectCommand);
-        }
+        { tmp = PptDeselectLegacyZip(Context, DeselectCommand); }
         return (tmp);
       } else {
       }
@@ -4216,8 +4183,7 @@ NTSTATUS PptDeselectDevice(PVOID Context, PVOID DeselectCommand) {
     DeviceID = Command->ID;
     if (!(Command->CommandFlags & 1UL)) {
       if ((ULONG)DeviceID > Extension->PnpInfo.Ieee1284_3DeviceCount) {
-        {
-        }
+        {}
         Status = -1073741811L;
       } else {
         goto _L___0;
@@ -4248,12 +4214,9 @@ NTSTATUS PptDeselectDevice(PVOID Context, PVOID DeselectCommand) {
           while_91_break: /* CIL Label */;
           }
           if (success) {
-            {
-            }
+            {}
             if (!(Command->CommandFlags & 2UL)) {
-              {
-                PptFreePort(Extension);
-              }
+              { PptFreePort(Extension); }
             } else {
             }
             Status = 0L;
@@ -4268,9 +4231,7 @@ NTSTATUS PptDeselectDevice(PVOID Context, PVOID DeselectCommand) {
       _L : /* CIL Label */
       {}
         if (!(Command->CommandFlags & 2UL)) {
-          {
-            PptFreePort(Extension);
-          }
+          { PptFreePort(Extension); }
         } else {
         }
         Status = 0L;
@@ -4327,9 +4288,7 @@ ULONG Ppt1284_3AssignAddress(PDEVICE_EXTENSION DeviceExtension) {
           status = READ_PORT_UCHAR(CurrentStatus);
         }
         if (((int)status & 48) == 48) {
-          {
-            KeStallExecutionProcessor(Delay);
-          }
+          { KeStallExecutionProcessor(Delay); }
           {
             while (1) {
             while_95_continue: /* CIL Label */;
@@ -4389,9 +4348,7 @@ ULONG Ppt1284_3AssignAddress(PDEVICE_EXTENSION DeviceExtension) {
                 } else {
                 }
                 if (1 == (int)bStlNon1284_3Found) {
-                  {
-                    tmp___1 = PptCheckIfStlProductId(DeviceExtension, idx);
-                  }
+                  { tmp___1 = PptCheckIfStlProductId(DeviceExtension, idx); }
                   if (1 == (int)tmp___1) {
                     bStlNon1284_3Valid = 1;
                     goto __Cont;
@@ -4812,8 +4769,7 @@ BOOLEAN PptSend1284_3Command(PDEVICE_EXTENSION DeviceExtension, UCHAR Command) {
                   } else {
                   }
                   if (!success) {
-                    {
-                    }
+                    {}
                   } else {
                   }
                   goto switch_99_break;
@@ -4827,8 +4783,7 @@ BOOLEAN PptSend1284_3Command(PDEVICE_EXTENSION DeviceExtension, UCHAR Command) {
                   } else {
                   }
                   if (!success) {
-                    {
-                    }
+                    {}
                   } else {
                   }
                   goto switch_99_break;
@@ -5016,9 +4971,7 @@ NTSTATUS PptDetectPortCapabilities(PDEVICE_EXTENSION Extension) {
           if (!Extension->NationalChipFound) {
             {} {} { PptDetectEppPortIfDot3DevicePresent(Extension); }
             if (!Extension->CheckedForGenericEpp) {
-              {
-                PptDetectEppPortIfUserRequested(Extension);
-              }
+              { PptDetectEppPortIfUserRequested(Extension); }
             } else {
             }
           } else {
@@ -5037,8 +4990,7 @@ NTSTATUS PptDetectPortCapabilities(PDEVICE_EXTENSION Extension) {
     }
     {} { PptDetectBytePort(Extension); }
     if (Extension->PnpInfo.HardwareCapabilities & 11UL) {
-      {
-      }
+      {}
       return (0L);
     } else {
     }
@@ -5059,8 +5011,7 @@ void PptDetectEcpPort(PDEVICE_EXTENSION Extension) {
     wPortDCR = Controller + 2;
     if ((unsigned int)((PUCHAR)0) ==
         (unsigned int)Extension->PnpInfo.EcpController) {
-      {
-      }
+      {}
       return;
     } else {
     }
@@ -5151,8 +5102,7 @@ void PptDetectEppPortIfDot3DevicePresent(PDEVICE_EXTENSION Extension) {
     Forward = (unsigned char)6;
     daisyChainDevicePresent = 0;
     if (0UL == Extension->PnpInfo.Ieee1284_3DeviceCount) {
-      {
-      }
+      {}
       return;
     } else {
     }
@@ -5163,8 +5113,7 @@ void PptDetectEppPortIfDot3DevicePresent(PDEVICE_EXTENSION Extension) {
       status = PptTrySelectDevice(Extension, &Command);
     }
     if (!(status >= 0L)) {
-      {
-      }
+      {}
       return;
     } else {
     }
@@ -5176,8 +5125,7 @@ void PptDetectEppPortIfDot3DevicePresent(PDEVICE_EXTENSION Extension) {
       status = PptDeselectDevice(Extension, &Command);
     }
     if (!(status >= 0L)) {
-      {
-      }
+      {}
     } else {
       {}
     }
@@ -5190,9 +5138,7 @@ void PptDetectEppPortIfUserRequested(PDEVICE_EXTENSION Extension) {
   {
     RequestEppTest = 0;
     if (RequestEppTest) {
-      {
-        PptDetectEppPort(Extension);
-      }
+      { PptDetectEppPort(Extension); }
     } else {
     }
     return;
@@ -5237,8 +5183,7 @@ void PptDetectEppPort(PDEVICE_EXTENSION Extension) {
       Extension->CheckedForGenericEpp = 1;
     }
     if (Extension->PnpInfo.HardwareCapabilities & 2UL) {
-      {
-      }
+      {}
     } else {
       {}
     }
@@ -5252,8 +5197,7 @@ void PptDetectBytePort(PDEVICE_EXTENSION Extension) {
     Status = 0L;
     {} { Status = PptSetByteMode(Extension, 52); }
     if (Status >= 0L) {
-      {
-      }
+      {}
       Extension->PnpInfo.HardwareCapabilities |= 8UL;
     } else {
       {}
@@ -5329,9 +5273,7 @@ void PptDetermineFifoDepth(PDEVICE_EXTENSION Extension) {
           }
           { testData = READ_PORT_UCHAR(wPortDFIFO); }
           if ((int)testData != ((int)readFifoDepth & 255)) {
-            {
-              WRITE_PORT_UCHAR(wPortECR, ecrLast);
-            }
+            { WRITE_PORT_UCHAR(wPortECR, ecrLast); }
             {}
             return;
           } else {
@@ -5387,8 +5329,7 @@ NTSTATUS PptSetChipMode(PDEVICE_EXTENSION Extension, UCHAR ChipMode) {
     EcrMode = (unsigned char)((int)ChipMode & -32);
     {}
     if (Extension->PnpInfo.CurrentMode != 0UL) {
-      {
-      }
+      {}
       Status = -1073741436L;
       goto ExitSetChipModeNoChange;
     } else {
@@ -5402,8 +5343,7 @@ NTSTATUS PptSetChipMode(PDEVICE_EXTENSION Extension, UCHAR ChipMode) {
       {}
       if ((int)EcrMode == 96) {
         if ((Extension->PnpInfo.HardwareCapabilities & 1UL) ^ 1UL) {
-          {
-          }
+          {}
           return (-1073741810L);
         } else {
         }
@@ -5413,8 +5353,7 @@ NTSTATUS PptSetChipMode(PDEVICE_EXTENSION Extension, UCHAR ChipMode) {
       }
       if ((int)EcrMode == 128) {
         if ((Extension->PnpInfo.HardwareCapabilities & 2UL) ^ 2UL) {
-          {
-          }
+          {}
           return (-1073741810L);
         } else {
         }
@@ -5424,8 +5363,7 @@ NTSTATUS PptSetChipMode(PDEVICE_EXTENSION Extension, UCHAR ChipMode) {
       }
       if ((int)EcrMode == 32) {
         if ((Extension->PnpInfo.HardwareCapabilities & 8UL) ^ 8UL) {
-          {
-          }
+          {}
           return (-1073741810L);
         } else {
         }
@@ -5436,8 +5374,7 @@ NTSTATUS PptSetChipMode(PDEVICE_EXTENSION Extension, UCHAR ChipMode) {
     }
   ExitSetChipModeWithChanges:
     if (Status >= 0L) {
-      {
-      }
+      {}
       Extension->PnpInfo.CurrentMode = EcrMode;
     } else {
       {}
@@ -5455,8 +5392,7 @@ NTSTATUS PptClearChipMode(PDEVICE_EXTENSION Extension, UCHAR ChipMode) {
     EcrMode = (int)ChipMode & -32;
     {}
     if (EcrMode != Extension->PnpInfo.CurrentMode) {
-      {
-      }
+      {}
       Status = -1073741436L;
       goto ExitClearChipModeNoChange;
     } else {
@@ -5469,31 +5405,24 @@ NTSTATUS PptClearChipMode(PDEVICE_EXTENSION Extension, UCHAR ChipMode) {
     } else {
       {}
       if (EcrMode == 96UL) {
-        {
-          Status = PptEcrClearMode(Extension);
-        }
+        { Status = PptEcrClearMode(Extension); }
         goto ExitClearChipModeWithChanges;
       } else {
       }
       if (EcrMode == 128UL) {
-        {
-          Status = PptEcrClearMode(Extension);
-        }
+        { Status = PptEcrClearMode(Extension); }
         goto ExitClearChipModeWithChanges;
       } else {
       }
       if (EcrMode == 32UL) {
-        {
-          Status = PptClearByteMode(Extension);
-        }
+        { Status = PptClearByteMode(Extension); }
         goto ExitClearChipModeWithChanges;
       } else {
       }
     }
   ExitClearChipModeWithChanges:
     if (Status >= 0L) {
-      {
-      }
+      {}
       Extension->PnpInfo.CurrentMode = 0;
     } else {
     }
@@ -5526,9 +5455,7 @@ NTSTATUS PptSetByteMode(PDEVICE_EXTENSION Extension, UCHAR ChipMode) {
 
   {
     if (Extension->PnpInfo.HardwareCapabilities & 1UL) {
-      {
-        Status = PptEcrSetMode(Extension, ChipMode);
-      }
+      { Status = PptEcrSetMode(Extension, ChipMode); }
     } else {
     }
     { Status = PptCheckByteMode(Extension); }
@@ -5541,9 +5468,7 @@ NTSTATUS PptClearByteMode(PDEVICE_EXTENSION Extension) {
   {
     Status = 0L;
     if (Extension->PnpInfo.HardwareCapabilities & 1UL) {
-      {
-        Status = PptEcrClearMode(Extension);
-      }
+      { Status = PptEcrClearMode(Extension); }
     } else {
     }
     return (Status);
@@ -5637,8 +5562,7 @@ NTSTATUS PptFindNatChip(PDEVICE_EXTENSION Extension) {
     NationalChecked = 0;
     NationalChipFound = 0;
     if ((int)Extension->NationalChecked == 1) {
-      {
-      }
+      {}
       return (0L);
     } else {
     }
@@ -5661,8 +5585,7 @@ NTSTATUS PptFindNatChip(PDEVICE_EXTENSION Extension) {
       Resources = (struct _CM_RESOURCE_LIST *)tmp;
     }
     if ((unsigned int)Resources == (unsigned int)((void *)0)) {
-      {
-      }
+      {}
       return (-1073741823L);
     } else {
     }
@@ -5684,14 +5607,12 @@ NTSTATUS PptFindNatChip(PDEVICE_EXTENSION Extension) {
       /*   ExFreePool(Resources); */ /* INLINED */
     }
     if (!(Status >= 0L)) {
-      {
-      }
+      {}
       return (Status);
     } else {
     }
     if (Conflict) {
-      {
-      }
+      {}
       return (-1073741823L);
     } else {
     }
@@ -5713,9 +5634,7 @@ NTSTATUS PptFindNatChip(PDEVICE_EXTENSION Extension) {
           tmp___1 = READ_PORT_UCHAR(PortAddr);
         }
         if ((int)tmp___1 == 136) {
-          {
-            tmp___2 = READ_PORT_UCHAR(PortAddr);
-          }
+          { tmp___2 = READ_PORT_UCHAR(PortAddr); }
           if ((int)tmp___2 < 32) {
             OkToLook = 1;
           } else {
@@ -5728,9 +5647,7 @@ NTSTATUS PptFindNatChip(PDEVICE_EXTENSION Extension) {
           cr = READ_PORT_UCHAR(PortAddr);
         }
           if ((int)cr != 255) {
-            {
-              tmp___0 = READ_PORT_UCHAR(PortAddr);
-            }
+            { tmp___0 = READ_PORT_UCHAR(PortAddr); }
             if ((int)tmp___0 == (int)cr) {
               OkToLook = 1;
             } else {
@@ -6022,8 +5939,7 @@ PDEVICE_RELATIONS PptPnpBuildRemovalRelations(PDEVICE_EXTENSION Extension) {
       /*   ExAcquireFastMutex(& Extension->ExtensionFastMutex); */ /* INLINED */
     }
     if ((unsigned int)listHead->Flink == (unsigned int)listHead) {
-      {
-      }
+      {}
       goto targetExit;
     } else {
     }
@@ -6065,8 +5981,7 @@ PDEVICE_RELATIONS PptPnpBuildRemovalRelations(PDEVICE_EXTENSION Extension) {
           count += 1UL;
         }
         if (!firstListEntry) {
-          {
-          }
+          {}
           firstListEntry = thisListEntry;
         } else {
         }
@@ -6082,8 +5997,7 @@ PDEVICE_RELATIONS PptPnpBuildRemovalRelations(PDEVICE_EXTENSION Extension) {
       relations = tmp;
     }
     if (!relations) {
-      {
-      }
+      {}
       goto targetExit;
     } else {
     }
@@ -6293,15 +6207,13 @@ BOOLEAN PptIsPci(PDEVICE_EXTENSION Extension, PIRP Irp) {
     ResourceList =
         irpStack->Parameters.StartDevice.AllocatedResourcesTranslated;
     if ((unsigned int)ResourceList == (unsigned int)((void *)0)) {
-      {
-      }
+      {}
       return (0);
     } else {
     }
     FullResourceDescriptor = &ResourceList->List[0];
     if (FullResourceDescriptor) {
-      {
-      }
+      {}
       PartialResourceList = &FullResourceDescriptor->PartialResourceList;
       i = 0;
       {
@@ -6325,8 +6237,7 @@ BOOLEAN PptIsPci(PDEVICE_EXTENSION Extension, PIRP Irp) {
                 {}
                 portResourceDescriptorCount += 1UL;
                 if (rangeLength > 8UL) {
-                  {
-                  }
+                  {}
                   largePortRangeFound = 1;
                 } else {
                 }
@@ -6399,8 +6310,7 @@ NTSTATUS PptPnpAddDevice(PDRIVER_OBJECT pDriverObject,
           PptBuildDeviceObject(pDriverObject, pPhysicalDeviceObject);
     }
     if ((unsigned int)((void *)0) == (unsigned int)pDeviceObject) {
-      {
-      }
+      {}
       return (-1073741823L);
     } else {
     }
@@ -6452,9 +6362,7 @@ NTSTATUS PptDispatchPnp(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                      .CurrentStackLocation;
       minorFunction = irpStack->MinorFunction;
       if ((int)minorFunction > 24) {
-        {
-          status = PptPnpUnhandledIrp(DeviceObject, Irp);
-        }
+        { status = PptPnpUnhandledIrp(DeviceObject, Irp); }
       } else {
         if (__BLAST_NONDET == 0) {
           goto switch_214_0;
@@ -6614,9 +6522,7 @@ NTSTATUS PptPnpStartDevice(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
       status = PptDetectChipFilter(extension);
     }
     if (!(status >= 0L)) {
-      {
-        PptDetectPortType(extension);
-      }
+      { PptDetectPortType(extension); }
     } else {
     }
     { status = PptWmiInitWmi(DeviceObject); }
@@ -6678,17 +6584,14 @@ NTSTATUS PptPnpStartScanCmResourceList(PDEVICE_EXTENSION Extension, PIRP Irp,
     ResourceList =
         irpStack->Parameters.StartDevice.AllocatedResourcesTranslated;
     if ((unsigned int)ResourceList == (unsigned int)((void *)0)) {
-      {
-      }
+      {}
       status = -1073741670L;
       goto targetExit;
     } else {
     }
     if ((int)((KUSER_SHARED_DATA *const)4292804608U)->AlternativeArchitecture !=
         1) {
-      {
-        tmp = PptIsPci(Extension, Irp);
-      }
+      { tmp = PptIsPci(Extension, Irp); }
       if (1 == (int)tmp) {
         {} {
           status = PptPnpStartScanPciCardCmResourceList(
@@ -6738,8 +6641,7 @@ NTSTATUS PptPnpStartScanCmResourceList(PDEVICE_EXTENSION Extension, PIRP Irp,
                               .__annonCompField1.LowPart == 0UL) {
                         if (Extension->PortInfo.OriginalController
                                 .__annonCompField1.HighPart == 0L) {
-                          {
-                          }
+                          {}
                           Extension->PortInfo.OriginalController =
                               PartialResourceDescriptor->u.Port.Start;
                           Extension->PortInfo.SpanOfController =
@@ -6750,9 +6652,7 @@ NTSTATUS PptPnpStartScanCmResourceList(PDEVICE_EXTENSION Extension, PIRP Irp,
                           Extension->AddressSpace =
                               PartialResourceDescriptor->Flags;
                           if (Extension->PortInfo.SpanOfController == 4096UL) {
-                            {
-                              tmp___0 = PptIsNecR98Machine();
-                            }
+                            { tmp___0 = PptIsNecR98Machine(); }
                             if (tmp___0) {
                               Extension->PortInfo.SpanOfController = 8;
                             } else {
@@ -6778,8 +6678,7 @@ NTSTATUS PptPnpStartScanCmResourceList(PDEVICE_EXTENSION Extension, PIRP Irp,
                                         .__annonCompField1.HighPart <
                                     Extension->PortInfo.OriginalController
                                         .__annonCompField1.HighPart) {
-                                  {
-                                  }
+                                  {}
                                   Extension->PnpInfo.OriginalEcpController =
                                       Extension->PortInfo.OriginalController;
                                   Extension->PnpInfo.SpanOfEcpController =
@@ -6800,9 +6699,7 @@ NTSTATUS PptPnpStartScanCmResourceList(PDEVICE_EXTENSION Extension, PIRP Irp,
                                       PartialResourceDescriptor->Flags;
                                   if (Extension->PortInfo.SpanOfController ==
                                       4096UL) {
-                                    {
-                                      tmp___1 = PptIsNecR98Machine();
-                                    }
+                                    { tmp___1 = PptIsNecR98Machine(); }
                                     if (tmp___1) {
                                       Extension->PortInfo.SpanOfController = 8;
                                     } else {
@@ -7055,8 +6952,7 @@ BOOLEAN PptPnpFilterExistsNonIrqResourceList(
             }
             {}
             if ((int)curDesc->Type == 2) {
-              {
-              }
+              {}
               foundIrq = 1;
               goto while_243_break;
             } else {
@@ -7067,8 +6963,7 @@ BOOLEAN PptPnpFilterExistsNonIrqResourceList(
         while_243_break: /* CIL Label */;
         }
         if ((int)foundIrq == 0) {
-          {
-          }
+          {}
           return (1);
         } else {
         }
@@ -7112,8 +7007,7 @@ void PptPnpFilterRemoveIrqResourceLists(
         }
         {} {} { tmp___0 = PptPnpListContainsIrqResourceDescriptor(curList); }
         if (tmp___0) {
-          {
-          }
+          {}
           nextList = (struct _IO_RESOURCE_LIST *)(curList->Descriptors +
                                                   curList->Count);
           bytesToMove =
@@ -7259,15 +7153,13 @@ NTSTATUS PptPnpQueryDeviceRelations(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
                 switch_261_3: /* CIL Label */;
                   {} { PptDumpRemovalRelationsList(extension); }
                   if (Irp->IoStatus.Information) {
-                    {
-                    }
+                    {}
                   } else {
                     {
                       removalRelations = PptPnpBuildRemovalRelations(extension);
                     }
                     if (removalRelations) {
-                      {
-                      }
+                      {}
                       Irp->IoStatus.__annonCompField4.Status = 0L;
                       myStatus = 0L;
                       Irp->IoStatus.Information =
@@ -7535,14 +7427,10 @@ NTSTATUS PptPnpBounceAndCatchPnpIrp(PDEVICE_EXTENSION Extension, PIRP Irp) {
       nextIrpSp->Control = 0;
     }
     if (s != NP) {
-      {
-        errorFn();
-      }
+      { errorFn(); }
     } else {
       if (compRegistered != 0) {
-        {
-          errorFn();
-        }
+        { errorFn(); }
       } else {
         compRegistered = 1;
         compFptr = &PptSynchCompletionRoutine;
@@ -7805,9 +7693,7 @@ NTSTATUS PptDispatchPower(PDEVICE_OBJECT pDeviceObject, PIRP pIrp) {
                       hookit = 1;
                       if ((int)((KUSER_SHARED_DATA *const)4292804608U)
                               ->AlternativeArchitecture == 1) {
-                        {
-                          InitNEC_98(Extension);
-                        }
+                        { InitNEC_98(Extension); }
                       } else {
                       }
                     } else {
@@ -7868,14 +7754,10 @@ NTSTATUS PptDispatchPower(PDEVICE_OBJECT pDeviceObject, PIRP pIrp) {
     } else {
       if (hookit) {
         if (s != NP) {
-          {
-            errorFn();
-          }
+          { errorFn(); }
         } else {
           if (compRegistered != 0) {
-            {
-              errorFn();
-            }
+            { errorFn(); }
           } else {
             compRegistered = 1;
             compFptr = &PptPowerComplete;
@@ -8034,22 +7916,17 @@ NTSTATUS PptTrySelectLegacyZip(PVOID Context, PVOID TrySelectCommand) {
     if (Status >= 0L) {
       if (Status != 259L) {
         if (Command->CommandFlags & 32UL) {
-          {
-            PptLegacyZipSetDiskMode(Controller, (unsigned char)207);
-          }
+          { PptLegacyZipSetDiskMode(Controller, (unsigned char)207); }
         } else {
           { PptLegacyZipSetDiskMode(Controller, (unsigned char)143); }
         }
         { tmp = PptLegacyZipCheckDevice(Controller); }
         if (tmp) {
-          {
-          }
+          {}
           if (!Extension->CheckedForGenericEpp) {
             if (Extension->PnpInfo.HardwareCapabilities & 1UL) {
               if (!Extension->NationalChipFound) {
-                {
-                  PptDetectEppPort(Extension);
-                }
+                { PptDetectEppPort(Extension); }
               } else {
               }
             } else {
@@ -8085,9 +7962,7 @@ NTSTATUS PptDeselectLegacyZip(PVOID Context, PVOID DeselectCommand) {
       PptLegacyZipClockPrtModeByte(Controller, (unsigned char)15);
     }
     if (!(Command->CommandFlags & 2UL)) {
-      {
-        PptFreePort(Extension);
-      }
+      { PptFreePort(Extension); }
     } else {
     }
     return (0L);
@@ -8214,8 +8089,7 @@ NTSTATUS PptRegSetDeviceParameterDword(PDEVICE_OBJECT Pdo, PWSTR ParameterName,
   {
     { status = IoOpenDeviceRegistryKey(Pdo, 1, 131078L, &hKey); }
     if (!(status >= 0L)) {
-      {
-      }
+      {}
       return (status);
     } else {
     }
@@ -8225,8 +8099,7 @@ NTSTATUS PptRegSetDeviceParameterDword(PDEVICE_OBJECT Pdo, PWSTR ParameterName,
           ZwSetValueKey(hKey, &valueName, 0, 4, ParameterValue, sizeof(ULONG));
     }
     if (!(status >= 0L)) {
-      {
-      }
+      {}
     } else {
     }
     { ZwClose(hKey); }
@@ -8288,9 +8161,7 @@ NTSTATUS PptAcquireRemoveLockOrFailIrp(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
       status = tmp;
     }
     if (!(status >= 0L)) {
-      {
-        PptFailRequest(Irp, status);
-      }
+      { PptFailRequest(Irp, status); }
     } else {
     }
     return (status);
@@ -8350,8 +8221,7 @@ PWSTR PptGetPortNameFromPhysicalDeviceObject(
           IoOpenDeviceRegistryKey(PhysicalDeviceObject, 1, 2031616L, &hKey);
     }
     if (!(status >= 0L)) {
-      {
-      }
+      {}
       return ((void *)0);
     } else {
     }
@@ -8891,8 +8761,7 @@ NTSTATUS PptBuildParallelPortDeviceName(ULONG Number,
       status = RtlIntegerToUnicodeString(Number, 10, &uniPortNumberString);
     }
     if (!(status >= 0L)) {
-      {
-      }
+      {}
       return (status);
     } else {
     }
@@ -8906,8 +8775,7 @@ NTSTATUS PptBuildParallelPortDeviceName(ULONG Number,
       DeviceName->Buffer = tmp;
     }
     if ((unsigned int)((void *)0) == (unsigned int)DeviceName->Buffer) {
-      {
-      }
+      {}
       return (-1073741670L);
     } else {
     }
@@ -9000,8 +8868,7 @@ NTSTATUS PptGetPortNumberFromLptName(PWSTR PortName, PULONG PortNumber) {
 
   {
     if (__BLAST_NONDET) {
-      {
-      }
+      {}
       return (-1073741823L);
     } else {
     }
@@ -9010,14 +8877,12 @@ NTSTATUS PptGetPortNumberFromLptName(PWSTR PortName, PULONG PortNumber) {
       status = RtlUnicodeStringToInteger(&str, 10, PortNumber);
     }
     if (!(status >= 0L)) {
-      {
-      }
+      {}
       return (-1073741823L);
     } else {
     }
     if (*PortNumber == 0UL) {
-      {
-      }
+      {}
       return (-1073741823L);
     } else {
     }
@@ -9045,8 +8910,7 @@ PDEVICE_OBJECT PptBuildDeviceObject(PDRIVER_OBJECT DriverObject,
       portName = PptGetPortNameFromPhysicalDeviceObject(PhysicalDeviceObject);
     }
     if ((unsigned int)((void *)0) == (unsigned int)portName) {
-      {
-      }
+      {}
       goto targetExit;
     } else {
     }
@@ -9070,8 +8934,7 @@ PDEVICE_OBJECT PptBuildDeviceObject(PDRIVER_OBJECT DriverObject,
                               &uniNameString, 22, 256, 0, &deviceObject);
     }
     if (-1073741771L == status) {
-      {
-      }
+      {}
       portNumber = 7;
       {
         while (1) {
@@ -9509,9 +9372,7 @@ int main(void) {
         }
       }
       if (we_should_unload) {
-        {
-          PptUnload(&d);
-        }
+        { PptUnload(&d); }
       } else {
       }
     } else {
@@ -9541,9 +9402,7 @@ int main(void) {
             if (s != SKIP2) {
               if (s != IPC) {
                 if (s != DC) {
-                  {
-                    errorFn();
-                  }
+                  { errorFn(); }
                 } else {
                   goto _L___0;
                 }
@@ -9554,24 +9413,18 @@ int main(void) {
             _L___0: /* CIL Label */
               if (pended == 1) {
                 if (status != 259L) {
-                  {
-                    errorFn();
-                  }
+                  { errorFn(); }
                 } else {
                 }
               } else {
                 if (s == DC) {
                   if (status == 259L) {
-                    {
-                      errorFn();
-                    }
+                    { errorFn(); }
                   } else {
                   }
                 } else {
                   if (status != (NTSTATUS)lowerDriverReturn) {
-                    {
-                      errorFn();
-                    }
+                    { errorFn(); }
                   } else {
                   }
                 }
@@ -10015,9 +9868,7 @@ NTSTATUS IofCallDriver(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
         }
       }
       if ((long)compRetStatus == -1073741802L) {
-        {
-          stubMoreProcessingRequired();
-        }
+        { stubMoreProcessingRequired(); }
       } else {
       }
     } else {
@@ -10171,9 +10022,7 @@ NTSTATUS KeWaitForSingleObject(PVOID Object, KWAIT_REASON WaitReason,
         customIrp = 0;
       } else {
         if (s == MPR3) {
-          {
-            errorFn();
-          }
+          { errorFn(); }
         } else {
         }
       }
@@ -10319,9 +10168,7 @@ NTSTATUS PoCallDriver(PDEVICE_OBJECT DeviceObject, PIRP Irp) {
         }
       }
       if ((long)compRetStatus == -1073741802L) {
-        {
-          stubMoreProcessingRequired();
-        }
+        { stubMoreProcessingRequired(); }
       } else {
       }
     } else {
diff --git a/test/llvm/llvm-expect.ll b/test/llvm/llvm-expect.ll
new file mode 100644
index 000000000..0fd72f359
--- /dev/null
+++ b/test/llvm/llvm-expect.ll
@@ -0,0 +1,19 @@
+; @expect verified
+
+; This file tests that the semantics of the llvm.expect intrinsic is properly
+; modeled.
+; ModuleID = '/home/vagrant/rust-smack/b-Y00Q2K.bc'
+source_filename = "llvm-link"
+target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128"
+target triple = "x86_64-unknown-linux-gnu"
+
+; Function Attrs: nounwind uwtable
+define i32 @main() {
+  %1 = add nsw i32 0, 1
+  %2 = call i32 @llvm.expect.i32(i32 %1, i32 1)
+  call void @__VERIFIER_assert(i32 %2)
+  ret i32 0
+}
+
+declare i32 @llvm.expect.i32(i32, i32)
+declare void @__VERIFIER_assert(i32)
\ No newline at end of file
diff --git a/test/llvm/llvm-expect_fail.ll b/test/llvm/llvm-expect_fail.ll
new file mode 100644
index 000000000..7423638ff
--- /dev/null
+++ b/test/llvm/llvm-expect_fail.ll
@@ -0,0 +1,19 @@
+; @expect error
+
+; This file tests that the semantics of the llvm.expect intrinsic is properly
+; modeled.
+; ModuleID = '/home/vagrant/rust-smack/b-Y00Q2K.bc'
+source_filename = "llvm-link"
+target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128"
+target triple = "x86_64-unknown-linux-gnu"
+
+; Function Attrs: nounwind uwtable
+define i32 @main() {
+  %1 = add nsw i32 0, 1
+  %2 = call i32 @llvm.expect.i32(i32 0, i32 1)
+  call void @__VERIFIER_assert(i32 %2)
+  ret i32 0
+}
+
+declare i32 @llvm.expect.i32(i32, i32)
+declare void @__VERIFIER_assert(i32)
\ No newline at end of file
diff --git a/test/regtest.py b/test/regtest.py
index 3f6667806..98ca376ae 100755
--- a/test/regtest.py
+++ b/test/regtest.py
@@ -19,8 +19,10 @@
 APPEND_FIELDS = ['flags', 'checkbpl', 'checkout']
 
 LANGUAGES = {'c': {'*.c'},
+             'cargo': {'Cargo.toml'},
              'cplusplus': {'*.cpp'},
-             'rust': {'*.rs'}}
+             'rust': {'*.rs'},
+             'llvm-ir': {"*.ll"}}
 
 
 def bold(text):
diff --git a/test/rust/cargo/cargo-test/Cargo.toml b/test/rust/cargo/num-crate-test-fail/Cargo.toml
similarity index 94%
rename from test/rust/cargo/cargo-test/Cargo.toml
rename to test/rust/cargo/num-crate-test-fail/Cargo.toml
index 9e5aa6ccf..961bb86ea 100644
--- a/test/rust/cargo/cargo-test/Cargo.toml
+++ b/test/rust/cargo/num-crate-test-fail/Cargo.toml
@@ -4,6 +4,8 @@ version = "0.1.0"
 authors = ["smackers"]
 edition = "2018"
 
+# @expect error
+
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
diff --git a/test/rust/cargo/num-crate-test-fail/src/main.rs b/test/rust/cargo/num-crate-test-fail/src/main.rs
new file mode 100644
index 000000000..deea3bd20
--- /dev/null
+++ b/test/rust/cargo/num-crate-test-fail/src/main.rs
@@ -0,0 +1,13 @@
+extern crate num_traits;
+#[macro_use]
+extern crate smack;
+use smack::*;
+
+fn main() {
+    let a: u32 = 5.verifier_nondet();
+    let b: u32 = 3.verifier_nondet();
+    let c: u32 = 8.verifier_nondet();
+    verifier_assume!(a <= c);
+    let d = num_traits::clamp(b, a, c);
+    verifier_assert!(a > d || d > c);
+}
diff --git a/test/rust/cargo/num-crate-test/Cargo.toml b/test/rust/cargo/num-crate-test/Cargo.toml
new file mode 100644
index 000000000..6a837ac98
--- /dev/null
+++ b/test/rust/cargo/num-crate-test/Cargo.toml
@@ -0,0 +1,13 @@
+[package]
+name = "cargo-test"
+version = "0.1.0"
+authors = ["smackers"]
+edition = "2018"
+
+# @expect verified
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+num-traits = "0.2.12"
+smack = { path = "/usr/local/share/smack/lib" }
diff --git a/test/rust/cargo/cargo-test/src/main.rs b/test/rust/cargo/num-crate-test/src/main.rs
similarity index 100%
rename from test/rust/cargo/cargo-test/src/main.rs
rename to test/rust/cargo/num-crate-test/src/main.rs
diff --git a/test/rust/cargo/simple-static-lib-fail/Cargo.toml b/test/rust/cargo/simple-static-lib-fail/Cargo.toml
new file mode 100644
index 000000000..b264930c9
--- /dev/null
+++ b/test/rust/cargo/simple-static-lib-fail/Cargo.toml
@@ -0,0 +1,18 @@
+[package]
+name = "simple-static-lib"
+version = "0.1.0"
+authors = ["Shaobo He <polarishehn@gmail.com>"]
+edition = "2018"
+
+# @expect error
+# @flag --entry-point=helloworld
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[lib]
+name = "toylib"
+crate-type = ["staticlib"]
+
+
+[dependencies]
+smack = { path = "/usr/local/share/smack/lib" }
diff --git a/test/rust/cargo/simple-static-lib-fail/src/lib.rs b/test/rust/cargo/simple-static-lib-fail/src/lib.rs
new file mode 100644
index 000000000..c930b37d1
--- /dev/null
+++ b/test/rust/cargo/simple-static-lib-fail/src/lib.rs
@@ -0,0 +1,18 @@
+#![crate_name = "toylib"]
+#![crate_type = "staticlib"]
+#[macro_use]
+extern crate smack;
+use smack::*;
+
+#[cfg(test)]
+mod tests {
+    #[test]
+    fn it_works() {
+        assert_eq!(2 + 2, 4);
+    }
+}
+
+#[no_mangle]
+pub extern "C" fn helloworld() {
+    verifier_assert!(1 + 1 != 2);
+}
diff --git a/test/rust/cargo/simple-static-lib/Cargo.toml b/test/rust/cargo/simple-static-lib/Cargo.toml
new file mode 100644
index 000000000..8db37ecdb
--- /dev/null
+++ b/test/rust/cargo/simple-static-lib/Cargo.toml
@@ -0,0 +1,18 @@
+[package]
+name = "simple-static-lib"
+version = "0.1.0"
+authors = ["Shaobo He <polarishehn@gmail.com>"]
+edition = "2018"
+
+# @expect verified
+# @flag --entry-point=helloworld
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[lib]
+name = "toylib"
+crate-type = ["staticlib"]
+
+
+[dependencies]
+smack = { path = "/usr/local/share/smack/lib" }
diff --git a/test/rust/cargo/simple-static-lib/src/lib.rs b/test/rust/cargo/simple-static-lib/src/lib.rs
new file mode 100644
index 000000000..a4eb25fbd
--- /dev/null
+++ b/test/rust/cargo/simple-static-lib/src/lib.rs
@@ -0,0 +1,18 @@
+#![crate_name = "toylib"]
+#![crate_type = "staticlib"]
+#[macro_use]
+extern crate smack;
+use smack::*;
+
+#[cfg(test)]
+mod tests {
+    #[test]
+    fn it_works() {
+        assert_eq!(2 + 2, 4);
+    }
+}
+
+#[no_mangle]
+pub extern "C" fn helloworld() {
+    verifier_assert!(1 + 1 == 2);
+}
diff --git a/test/rust/box/box_basic.rs b/test/rust/failing/box_basic.rs
similarity index 57%
rename from test/rust/box/box_basic.rs
rename to test/rust/failing/box_basic.rs
index 6811ff6b7..db8824783 100644
--- a/test/rust/box/box_basic.rs
+++ b/test/rust/failing/box_basic.rs
@@ -1,3 +1,5 @@
+// fail reason: potential incompleteness of the solver
+// https://github.com/smackers/smack/commit/195bd52ff351bd289a47f565ad3b0e2f14d25dcd
 #[macro_use]
 extern crate smack;
 use smack::*;
diff --git a/test/rust/box/box_basic_fail.rs b/test/rust/failing/box_basic_fail.rs
similarity index 56%
rename from test/rust/box/box_basic_fail.rs
rename to test/rust/failing/box_basic_fail.rs
index b64fc709f..af0979d3b 100644
--- a/test/rust/box/box_basic_fail.rs
+++ b/test/rust/failing/box_basic_fail.rs
@@ -1,3 +1,5 @@
+// fail reason: potential incompleteness of the solver
+// https://github.com/smackers/smack/commit/195bd52ff351bd289a47f565ad3b0e2f14d25dcd
 #[macro_use]
 extern crate smack;
 use smack::*;
diff --git a/test/rust/memory-safety/buffer-overflow_fail.rs b/test/rust/memory-safety/buffer-overflow_fail.rs
new file mode 100644
index 000000000..cfaf3b8b1
--- /dev/null
+++ b/test/rust/memory-safety/buffer-overflow_fail.rs
@@ -0,0 +1,25 @@
+// @flag --check=memory-safety --unroll=2
+// @expect errro
+
+
+fn sum_to(slice: &[u8], to: usize) -> u64 {
+    // This function bypasses rust bounds checking. to must be less than or
+    // equal to the length of the slice.
+    
+    // if slice.len() < to { panic!(); }
+    let slice_ptr = slice.as_ptr();
+    let mut sum = 0;
+    // Bypass bounds checking
+    unsafe {
+	for idx in 0..to {
+	    sum += *slice_ptr.add(idx) as u64;
+	}
+    }
+    sum
+}
+
+
+fn main() {
+    let x = [1];
+    sum_to(&x, 2);
+}
diff --git a/test/rust/memory-safety/double-free_fail.rs b/test/rust/memory-safety/double-free_fail.rs
new file mode 100644
index 000000000..4a0944b6a
--- /dev/null
+++ b/test/rust/memory-safety/double-free_fail.rs
@@ -0,0 +1,13 @@
+use std::alloc::{alloc, Layout, System};
+use std::ptr;
+
+struct S {
+    data: &i32,
+}
+
+fn main() {
+    let layout = Layout::new::<i32>();
+    let x = S { data: alloc(layout) as *const i32 };
+    let y = unsafe { ptr::read(x) };
+    
+}
diff --git a/test/rust/memory-safety/double_free.rs b/test/rust/memory-safety/double_free.rs
new file mode 100644
index 000000000..1122a31e9
--- /dev/null
+++ b/test/rust/memory-safety/double_free.rs
@@ -0,0 +1,12 @@
+use std::alloc::{alloc, dealloc, Layout};
+
+// @expect verified
+
+fn main() {
+    let layout = Layout::new::<u32>();
+    unsafe {
+	let x = alloc(layout);
+	dealloc(x, layout);
+	//dealloc(x, layout);
+    }
+}
diff --git a/test/rust/memory-safety/double_free_fail.rs b/test/rust/memory-safety/double_free_fail.rs
new file mode 100644
index 000000000..6a68ffbb2
--- /dev/null
+++ b/test/rust/memory-safety/double_free_fail.rs
@@ -0,0 +1,12 @@
+use std::alloc::{alloc, dealloc, Layout};
+
+// @expect error
+
+fn main() {
+    let layout = Layout::new::<u32>();
+    unsafe {
+	let x = alloc(layout);
+	dealloc(x, layout);
+	dealloc(x, layout);
+    }
+}
diff --git a/test/rust/memory-safety/invalid-free_fail.rs b/test/rust/memory-safety/invalid-free_fail.rs
new file mode 100644
index 000000000..19750a63c
--- /dev/null
+++ b/test/rust/memory-safety/invalid-free_fail.rs
@@ -0,0 +1,21 @@
+use std::alloc::{alloc, Layout, System};
+use std::ptr;
+
+pub struct File {
+    buf: Box<u8>,
+}
+
+
+pub unsafe fn fdopen() -> * mut File {
+    let layout = Layout::new::<File>();
+    let f = alloc(layout) as * mut File;
+    // Rust will run drop on *f when it is assigned to, causing an invalid
+    // free on the member buf.
+    *f = File{buf: Box::new(0)};
+    //ptr::write(f, File{buf: vec!{0u8; 100}});
+    f
+}
+
+fn main() {
+    let x = unsafe { fdopen() };
+}
diff --git a/test/rust/memory-safety/use-after-free_fail.rs b/test/rust/memory-safety/use-after-free_fail.rs
new file mode 100644
index 000000000..4902fc99e
--- /dev/null
+++ b/test/rust/memory-safety/use-after-free_fail.rs
@@ -0,0 +1,24 @@
+use std::ptr;
+
+// Simplified from Qin et al. fig. 7
+
+unsafe fn run(data: *const u8) -> bool {
+    if data.is_null() { false }
+    else { *data == 0 }
+}
+
+fn sign(data: Option<&[u8]>) -> bool {
+    let p = match data {
+	Some(d) => Box::new(d).as_ptr(),
+	None => ptr::null_mut(),
+    }; // Lifetime of temporary Box ends
+    unsafe {
+	run(p)
+    }
+}
+
+
+fn main() {
+    let data = [0u8; 2];
+    sign(Some(&data));
+}
diff --git a/tools/llvm2bpl/llvm2bpl.cpp b/tools/llvm2bpl/llvm2bpl.cpp
index a0ec23d28..4d018896b 100644
--- a/tools/llvm2bpl/llvm2bpl.cpp
+++ b/tools/llvm2bpl/llvm2bpl.cpp
@@ -25,6 +25,7 @@
 #include "llvm/Target/TargetMachine.h"
 
 #include "seadsa/InitializePasses.hh"
+#include "seadsa/support/Debug.h"
 #include "seadsa/support/RemovePtrToInt.hh"
 #include "smack/AddTiming.h"
 #include "smack/BplFilePrinter.h"
@@ -101,7 +102,7 @@ static TargetMachine *GetTargetMachine(Triple TheTriple, StringRef CPUStr,
                                        const TargetOptions &Options) {
   std::string Error;
 
-  StringRef MArch;
+  const std::string MArch;
 
   const Target *TheTarget =
       TargetRegistry::lookupTarget(MArch, TheTriple, Error);
@@ -144,6 +145,10 @@ int main(int argc, char **argv) {
   if (L.empty())
     module.get()->setDataLayout(DefaultDataLayout);
 
+  if (smack::SmackOptions::WarningLevel ==
+      smack::SmackWarnings::WarningLevel::Info)
+    seadsa::SeaDsaEnableLog("dsa-warn");
+
   ///////////////////////////////
   // initialise and run passes //
   ///////////////////////////////
@@ -162,10 +167,10 @@ int main(int argc, char **argv) {
 
   if (!Modular) {
     auto PreserveKeyGlobals = [=](const llvm::GlobalValue &GV) {
-      std::string name = GV.getName();
+      auto name = GV.getName();
       return smack::SmackOptions::isEntryPoint(name) ||
              smack::Naming::isSmackName(name) ||
-             name.find("__VERIFIER_assume") != std::string::npos;
+             name.find("__VERIFIER_assume") != llvm::StringRef::npos;
     };
     pass_manager.add(llvm::createInternalizePass(PreserveKeyGlobals));
     pass_manager.add(llvm::createGlobalDCEPass());