diff --git a/.github/workflows/cmake-multi-platform.yml b/.github/workflows/cmake-multi-platform.yml
index 84cc52a..9e4f9ed 100644
--- a/.github/workflows/cmake-multi-platform.yml
+++ b/.github/workflows/cmake-multi-platform.yml
@@ -82,3 +82,4 @@ jobs:
       # Execute tests defined by the CMake configuration. Note that --build-config is needed because the default Windows generator is a multi-config generator (Visual Studio generator).
       # See https://cmake.org/cmake/help/latest/manual/ctest.1.html for more detail
       run: ctest --build-config ${{ matrix.build_type }}
+      if: ${{ matrix.os == 'ubuntu-latest' && matrix.c_compiler == 'gcc' }}
diff --git a/.gitmodules b/.gitmodules
index 92f9005..e6b05b0 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -4,3 +4,7 @@
 [submodule "extern/tinyxml2"]
 	path = extern/tinyxml2
 	url = https://github.com/leethomason/tinyxml2.git
+[submodule "extern/BAST"]
+	path = extern/BAST
+	url = ../BAST
+	branch = main
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 84ec47e..5d68f94 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -21,6 +21,7 @@ endif()
 if(PROJECT_IS_TOP_LEVEL)
   set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} ${CMAKE_SOURCE_DIR}/cmake/modules)
   add_subdirectory(extern/tinyxml2)
+  add_subdirectory(extern/BAST)
   add_subdirectory(extern/POGLIB)
 endif(PROJECT_IS_TOP_LEVEL)
 
@@ -29,4 +30,4 @@ add_subdirectory(src)
 if(PROJECT_IS_TOP_LEVEL)
   include (CTest)
   add_subdirectory(test)
-endif()
\ No newline at end of file
+endif(PROJECT_IS_TOP_LEVEL)
diff --git a/README.md b/README.md
index 5e713fa..091f87d 100644
--- a/README.md
+++ b/README.md
@@ -2,6 +2,10 @@
 
 [![License](https://img.shields.io/badge/license-GPLv3-blue.svg)](https://www.gnu.org/licenses/gpl-3.0.en.html)
 
+
+![Code format](https://github.com/CLEARSY/b2smtlib/actions/workflows/clang-format-check.yml/badge.svg)
+![Build & Test](https://github.com/CLEARSY/b2smtlib/actions/workflows/cmake-multi-platform.yml/badge.svg)
+
 `POG2WhyML` is a translator from pog to WhyML, the language of the [Why3](https://why3.org) platform for deductive program verification.
 
 ## Getting the sources
diff --git a/extern/BAST b/extern/BAST
new file mode 160000
index 0000000..ef0a47a
--- /dev/null
+++ b/extern/BAST
@@ -0,0 +1 @@
+Subproject commit ef0a47a30c836b430b76d6ac5b1204b158323e22