Import test suite from charon

27 files changed, 4148 insertions, 56 deletions

diff --git a/Makefile b/Makefile
index dc38e56a..73f711a7 100644
--- a/Makefile
+++ b/Makefile
@@ -13,35 +13,31 @@ all: build-tests-verify nix
 # Variables customizable by the user
 ####################################
 
-# Set this variable to any value to call Charon to regenerate the .llbc source
-# files before running the tests
-REGEN_LLBC ?=
-
-# The path to Charon
-CHARON_HOME ?= ./charon
-
-# The path to the Aeneas executable to run the tests - we need the ability to
-# change this path for the Nix package.
-AENEAS_EXE ?= bin/aeneas
-
-# The path to our test runner.
-TEST_RUNNER_EXE ?= bin/test_runner
+# Paths to the executables we need for tests. They are overriden in CI.
+AENEAS_EXE ?= $(PWD)/bin/aeneas
+TEST_RUNNER_EXE ?= $(PWD)/bin/test_runner
+CHARON_EXE ?= $(PWD)/charon/bin/charon
 
 # The user can specify additional translation options for Aeneas.
-# By default we activate the (expensive) sanity checks.
+# In CI we activate the (expensive) sanity checks.
 OPTIONS ?=
+CHARON_OPTIONS ?=
+
+# The directory thta contains the rust source files for tests.
+INPUTS_DIR ?= tests/src
+# The directory where to look for the .llbc files.
+LLBC_DIR ?= $(PWD)/tests/llbc
 
-# The rules use (and update) the following variables
-#
-# The Charon test directory where to look for the .llbc files
-CHARON_TEST_DIR ?= $(CHARON_HOME)/tests
-# The options with which to call Charon
-CHARON_OPTIONS =
+# In CI, we enforce formatting and we don't regenerate llbc files.
+IN_CI ?=
 
 ####################################
 # The rules
 ####################################
 
+# Never remove intermediate files
+.SECONDARY:
+
 # Build the compiler, after formatting the code
 .PHONY: build
 build: format build-dev
@@ -104,14 +100,51 @@ check-charon:
 setup-charon:
 	@./scripts/check-charon-install.sh --force
 
+ifdef IN_CI
+# In CI, error if formatting is not done.
+format: RUSTFMT_FLAGS := --check
+endif
+
+# Reformat the project files
+.PHONY: format
+format:
+	@# `|| `true` because the command returns an error if it changed anything, which we don't care about.
+	cd compiler && dune fmt || true
+	cd tests/test_runner && dune fmt || true
+	rustfmt $(RUSTFMT_FLAGS) $(INPUTS_DIR)/*.rs
+	cd $(INPUTS_DIR)/betree && cargo fmt $(RUSTFMT_FLAGS)
 
 .PHONY: clean
 clean: clean-generated
 	cd compiler && dune clean
+	cd $(INPUTS_DIR)/betree && $(MAKE) clean
+
+.PHONY: clean-generated
+clean-generated: clean-generated-aeneas clean-generated-llbc
+
+.PHONY: clean-generated-aeneas
+clean-generated-aeneas:
+	@# We can't put this line in `tests/Makefile` otherwise it will detect itself.
+	@# FIXME: generation of hol4 files is deactivated so we don't delete those.
+	@# `|| true` to avoid failing if there are no generated files present.
+	grep -lR 'THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS' tests | grep -v '^tests/hol4' | xargs rm || true
+
+.PHONY: clean-generated-llbc
+clean-generated-llbc:
+	rm -rf $(LLBC_DIR)
 
-# Test the project by translating test files to F*
+# =============================================================================
+# The tests.
+# =============================================================================
+
+# Test the project by translating test files to various backends.
 .PHONY: test
-test: build-dev test-all
+test: build-dev test-all betree-tests
+
+# This runs the rust tests of the betree crate.
+.PHONY: betree-tests
+betree-tests:
+	cd $(INPUTS_DIR)/betree && $(MAKE) test
 
 .PHONY: test-all
 test-all: \
@@ -129,46 +162,65 @@ test-all: \
 	test-polonius_list \
 	test-traits
 
-.PHONY: clean-generated
-clean-generated:
-	# We can't put this line in `tests/Makefile` otherwise it will detect itself.
-	# FIXME: generation of hol4 files is deactivated so we don't delete those.
-	grep -lR 'THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS' tests | grep -v '^tests/hol4' | xargs rm
-
 # Verify the F* files generated by the translation
 .PHONY: verify
 verify:
 	cd tests && $(MAKE) all
 
-# Reformat the project
-.PHONY: format
-format:
-	@# `|| `true` because the command returns an error if it changed anything, which we don't care about.
-	cd compiler && dune fmt || true
-	cd tests/test_runner && dune fmt || true
-
-# The commands to run Charon to generate the .llbc files
-ifeq (, $(REGEN_LLBC))
-else
-CHARON_CMD = cd $(CHARON_TEST_DIR) && $(MAKE) test-$*
+ifdef IN_CI
+# In CI we do extra sanity checks.
+test-%: OPTIONS += -checks
 endif
 
-# Generic rules to extract the LLBC from a rust file
-# We use the rules in Charon's Makefile to generate the .llbc files: the options
-# vary with the test files.
-.PHONY: gen-llbc-%
-gen-llbc-%:
-	$(CHARON_CMD)
-
 # Translate the given llbc file to available backends. The test runner decides
 # which backends to use and sets test-specific options.
 .PHONY: test-%
-test-%: FILE = $*
-test-%: gen-llbc-%
-	$(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) $(OPTIONS)
+test-%: TEST_NAME = $*
+test-%: $(LLBC_DIR)/%.llbc
+	$(TEST_RUNNER_EXE) $(AENEAS_EXE) $(LLBC_DIR) $(TEST_NAME) $(OPTIONS)
 	echo "# Test $* done"
 
-# Nix - TODO: add the lean tests
+#  List the `.rs` files in `$(INPUTS_DIR)/`
+INDIVIDUAL_RUST_SRCS = $(wildcard $(INPUTS_DIR)/*.rs)
+# We test all rust files except this one.
+INDIVIDUAL_RUST_SRCS := $(filter-out $(INPUTS_DIR)/hashmap_utils.rs, $(INDIVIDUAL_RUST_SRCS))
+# List the corresponding llbc files.
+INDIVIDUAL_LLBCS := $(subst $(INPUTS_DIR)/,$(LLBC_DIR)/,$(patsubst %.rs,%.llbc,$(INDIVIDUAL_RUST_SRCS)))
+
+.PHONY: generate-llbc
+# This depends on `llbc/<file>.llbc` for each `$(INPUTS_DIR)/<file>.rs` we care about, plus the whole-crate test.
+generate-llbc: $(INDIVIDUAL_LLBCS) $(LLBC_DIR)/betree_main.llbc
+
+$(LLBC_DIR)/hashmap_main.llbc: CHARON_OPTIONS += --opaque=hashmap_utils
+$(LLBC_DIR)/nested_borrows.llbc: CHARON_OPTIONS += --no-code-duplication
+$(LLBC_DIR)/no_nested_borrows.llbc: CHARON_OPTIONS += --no-code-duplication
+$(LLBC_DIR)/paper.llbc: CHARON_OPTIONS += --no-code-duplication
+$(LLBC_DIR)/constants.llbc: CHARON_OPTIONS += --no-code-duplication
+$(LLBC_DIR)/external.llbc: CHARON_OPTIONS += --no-code-duplication
+$(LLBC_DIR)/polonius_list.llbc: CHARON_OPTIONS += --polonius
+# Possible to add `--no-code-duplication` if we use the optimized MIR
+$(LLBC_DIR)/betree_main.llbc: CHARON_OPTIONS += --polonius --opaque=betree_utils --crate betree_main
+
+ifndef IN_CI
+$(LLBC_DIR)/%.llbc: check-charon
+
+$(LLBC_DIR)/%.llbc:
+	@# We do a `cd` dance to keep the exact same paths as before since that appears in the test outputs.
+	cd tests && $(CHARON_EXE) --no-cargo --input $(subst tests/,,$(INPUTS_DIR))/$*.rs --crate $* $(CHARON_OPTIONS) --dest $(LLBC_DIR)
+# Special rule for the whole-crate test.
+$(LLBC_DIR)/betree_main.llbc:
+	cd $(INPUTS_DIR)/betree && $(CHARON_EXE) $(CHARON_OPTIONS) --dest $(LLBC_DIR)
+else
+$(LLBC_DIR)/%.llbc:
+	@echo 'ERROR: llbc files should be built separately in CI'
+	@false
+endif
+
+
+# =============================================================================
+# Nix
+# =============================================================================
+# TODO: add the lean tests
 .PHONY: nix
 nix:
 	nix build && nix flake check
diff --git a/flake.nix b/flake.nix
index 7dd2b7c0..26689af0 100644
--- a/flake.nix
+++ b/flake.nix
@@ -80,6 +80,32 @@
           OCAMLPARAM = "_,warn-error=+A"; # Turn all warnings into errors.
         };
 
+        betree-llbc = charon.extractCrateWithCharon.${system} {
+          name = "betree";
+          src = ./tests/src/betree;
+          charonFlags = "--polonius --opaque=betree_utils --crate betree_main";
+          craneExtraArgs.checkPhaseCargoCommand = ''
+            cargo rustc -- --test -Zpolonius
+            ./target/debug/betree
+          '';
+        };
+        input-llbcs = pkgs.runCommand "input-llbcs"
+          {
+            src = ./tests/src;
+            makefile = ./Makefile;
+            buildInputs = [ charon.packages.${system}.rustToolchain charon.packages.${system}.charon ];
+          } ''
+          # Copy the betree output file
+          mkdir -p $out
+          cp ${betree-llbc}/llbc/betree_main.llbc $out
+
+          mkdir tests
+          cp -r $src tests/src
+          cp $makefile Makefile
+          # Generate the llbc files
+          CHARON_EXE="charon" INPUTS_DIR="tests/src" LLBC_DIR="$out" make generate-llbc
+        '';
+
         # Run the translation on various files.
         # Make sure we don't need to recompile the package whenever we make
         # unnecessary changes - we list the exact files and folders the package
@@ -95,9 +121,7 @@
               || pkgs.lib.hasPrefix (toString ./tests) path;
           };
           buildPhase = ''
-            # We need to provide the paths to the Charon tests derivations
-            export CHARON_TEST_DIR=${charon.checks.${system}.tests}
-
+            export LLBC_DIR=${input-llbcs}
             export AENEAS_EXE=${aeneas}/bin/aeneas
             export TEST_RUNNER_EXE=${test_runner}/bin/test_runner
 
@@ -106,8 +130,8 @@
 
             # Run the tests with extra sanity checks enabled
             # Remark: we could remove the file
-            make clean-generated
-            OPTIONS=-checks make test-all -j $NIX_BUILD_CORES
+            make clean-generated-aeneas
+            IN_CI=1 make test-all -j $NIX_BUILD_CORES
 
             # Check that there are no differences between the generated tests
             # and the original tests
@@ -124,6 +148,7 @@
           # something, otherwise Nix will consider the build has failed.
           installPhase = "touch $out";
         };
+
         # Replay the F* proofs.
         aeneas-verify-fstar = pkgs.stdenv.mkDerivation {
           name = "aeneas_verify_fstar";
diff --git a/tests/.gitignore b/tests/.gitignore
new file mode 100644
index 00000000..7eab4f57
--- /dev/null
+++ b/tests/.gitignore
@@ -0,0 +1,2 @@
+*.llbc
+target/
diff --git a/tests/Makefile b/tests/Makefile
index 8d40e8da..ff4baaba 100644
--- a/tests/Makefile
+++ b/tests/Makefile
@@ -1,4 +1,6 @@
+.PHONY: all
 all: test-fstar test-coq test-lean test-hol4
 
+.PHONY: test-%
 test-%:
 	cd $* && $(MAKE) all
diff --git a/tests/src/arrays.rs b/tests/src/arrays.rs
new file mode 100644
index 00000000..1f094541
--- /dev/null
+++ b/tests/src/arrays.rs
@@ -0,0 +1,328 @@
+//! Exercise the translation of arrays, with features supported by Eurydice
+
+pub enum AB {
+    A,
+    B,
+}
+
+pub fn incr(x: &mut u32) {
+    *x += 1;
+}
+
+// Nano-tests
+// ----------
+
+// The suffix `_` prevents name collisions in some backends
+pub fn array_to_shared_slice_<T>(s: &[T; 32]) -> &[T] {
+    s
+}
+
+// The suffix `_` prevents name collisions in some backends
+pub fn array_to_mut_slice_<T>(s: &mut [T; 32]) -> &mut [T] {
+    s
+}
+
+pub fn array_len<T>(s: [T; 32]) -> usize {
+    s.len()
+}
+
+pub fn shared_array_len<T>(s: &[T; 32]) -> usize {
+    s.len()
+}
+
+pub fn shared_slice_len<T>(s: &[T]) -> usize {
+    s.len()
+}
+
+pub fn index_array_shared<T>(s: &[T; 32], i: usize) -> &T {
+    &s[i]
+}
+
+// Remark: can't move out of an array
+// Also: can't move out of a slice.
+
+pub fn index_array_u32(s: [u32; 32], i: usize) -> u32 {
+    s[i]
+}
+
+pub fn index_array_copy(x: &[u32; 32]) -> u32 {
+    x[0]
+}
+
+pub fn index_mut_array<T>(s: &mut [T; 32], i: usize) -> &mut T {
+    &mut s[i]
+}
+
+pub fn index_slice<T>(s: &[T], i: usize) -> &T {
+    &s[i]
+}
+
+pub fn index_mut_slice<T>(s: &mut [T], i: usize) -> &mut T {
+    &mut s[i]
+}
+
+pub fn slice_subslice_shared_(x: &[u32], y: usize, z: usize) -> &[u32] {
+    &x[y..z]
+}
+
+pub fn slice_subslice_mut_(x: &mut [u32], y: usize, z: usize) -> &mut [u32] {
+    &mut x[y..z]
+}
+
+pub fn array_to_slice_shared_(x: &[u32; 32]) -> &[u32] {
+    x
+}
+
+pub fn array_to_slice_mut_(x: &mut [u32; 32]) -> &mut [u32] {
+    x
+}
+
+pub fn array_subslice_shared_(x: &[u32; 32], y: usize, z: usize) -> &[u32] {
+    &x[y..z]
+}
+
+pub fn array_subslice_mut_(x: &mut [u32; 32], y: usize, z: usize) -> &mut [u32] {
+    &mut x[y..z]
+}
+
+pub fn index_slice_0<T>(s: &[T]) -> &T {
+    &s[0]
+}
+
+pub fn index_array_0<T>(s: &[T; 32]) -> &T {
+    &s[0]
+}
+
+/*
+// Unsupported by Aeneas for now
+pub fn index_index_slice<'a, T>(s: &'a [&[T]], i: usize, j: usize) -> &'a T {
+    &s[i][j]
+}
+*/
+
+pub fn index_index_array(s: [[u32; 32]; 32], i: usize, j: usize) -> u32 {
+    s[i][j]
+}
+
+/*
+// Unsupported by Aeneas for now
+pub fn update_update_slice(s: &mut [&mut [u32]], i: usize, j: usize) {
+    s[i][j] = 0;
+}
+*/
+
+pub fn update_update_array(mut s: [[u32; 32]; 32], i: usize, j: usize) {
+    s[i][j] = 0;
+}
+
+pub fn array_local_deep_copy(x: &[u32; 32]) {
+    let _y = *x;
+}
+
+pub fn take_array(_: [u32; 2]) {}
+pub fn take_array_borrow(_: &[u32; 2]) {}
+pub fn take_slice(_: &[u32]) {}
+pub fn take_mut_slice(_: &mut [u32]) {}
+
+pub fn const_array() -> [u32; 2] {
+    [0, 0]
+}
+
+pub fn const_slice() {
+    let _: &[u32] = &[0, 0];
+}
+
+/*
+// This triggers a special case in the constant expressions
+pub fn const_string() {
+    let _ = "hello";
+}*/
+
+pub fn take_all() {
+    let mut x: [u32; 2] = [0, 0];
+    // x is deep copied (copy node appears in Charon, followed by a move)
+    take_array(x);
+    take_array(x);
+    // x passed by address, there is a reborrow here
+    take_array_borrow(&x);
+    // automatic cast from array to slice (spanning entire array)
+    take_slice(&x);
+    // note that both appear as SliceNew expressions, meaning the SliceNew UnOp is overloaded for
+    // mut and non-mut cases
+    take_mut_slice(&mut x);
+}
+
+pub fn index_array(x: [u32; 2]) -> u32 {
+    x[0]
+}
+pub fn index_array_borrow(x: &[u32; 2]) -> u32 {
+    x[0]
+}
+
+pub fn index_slice_u32_0(x: &[u32]) -> u32 {
+    x[0]
+}
+
+pub fn index_mut_slice_u32_0(x: &mut [u32]) -> u32 {
+    x[0]
+}
+
+pub fn index_all() -> u32 {
+    let mut x: [u32; 2] = [0, 0];
+    if true {
+        let _y: [u32; 2] = [0, 0];
+    } else {
+        let _z: [u32; 1] = [0];
+    }
+    index_array(x)
+        + index_array(x)
+        + index_array_borrow(&x)
+        + index_slice_u32_0(&x)
+        + index_mut_slice_u32_0(&mut x)
+}
+
+pub fn update_array(mut x: [u32; 2]) {
+    x[0] = 1
+}
+pub fn update_array_mut_borrow(x: &mut [u32; 2]) {
+    x[0] = 1
+}
+pub fn update_mut_slice(x: &mut [u32]) {
+    x[0] = 1
+}
+
+pub fn update_all() {
+    let mut x: [u32; 2] = [0, 0];
+    update_array(x);
+    update_array(x);
+    update_array_mut_borrow(&mut x);
+    update_mut_slice(&mut x);
+}
+
+// Nano-tests, with ranges
+// -----------------------
+
+pub fn range_all() {
+    let mut x: [u32; 4] = [0, 0, 0, 0];
+    // CONFIRM: there is no way to shrink [T;N] into [T;M] with M<N?
+    update_mut_slice(&mut x[1..3]);
+}
+
+// Nano-tests, with dereferences
+// -----------------------------
+
+pub fn deref_array_borrow(x: &[u32; 2]) -> u32 {
+    let x: [u32; 2] = *x;
+    x[0]
+}
+
+pub fn deref_array_mut_borrow(x: &mut [u32; 2]) -> u32 {
+    let x: [u32; 2] = *x;
+    x[0]
+}
+
+// Non-copiable arrays
+// -------------------
+
+pub fn take_array_t(_: [AB; 2]) {}
+
+pub fn non_copyable_array() {
+    let x: [AB; 2] = [AB::A, AB::B];
+    // x is moved (not deep copied!)
+    // TODO: determine whether the translation needs to be aware of that and pass by ref instead of by copy
+    take_array_t(x);
+
+    // this fails, naturally:
+    // take_array_t(x);
+}
+
+// Larger, random tests
+// --------------------
+
+pub fn sum(s: &[u32]) -> u32 {
+    let mut sum = 0;
+    let mut i = 0;
+    while i < s.len() {
+        sum += s[i];
+        i += 1;
+    }
+    sum
+}
+
+pub fn sum2(s: &[u32], s2: &[u32]) -> u32 {
+    let mut sum = 0;
+    assert!(s.len() == s2.len());
+    let mut i = 0;
+    while i < s.len() {
+        sum += s[i] + s2[i];
+        i += 1;
+    }
+    sum
+}
+
+pub fn f0() {
+    let s: &mut [u32] = &mut [1, 2];
+    s[0] = 1;
+}
+
+pub fn f1() {
+    let mut s: [u32; 2] = [1, 2];
+    s[0] = 1;
+}
+
+pub fn f2(_: u32) {}
+
+pub fn f3() -> u32 {
+    let a: [u32; 2] = [1, 2];
+    f2(a[0]);
+    let b = [0; 32];
+    sum2(&a, f4(&b, 16, 18))
+}
+
+pub fn f4(x: &[u32; 32], y: usize, z: usize) -> &[u32] {
+    &x[y..z]
+}
+
+pub const SZ: usize = 32;
+
+// There is something slightly annoying here: the SZ constant gets inlined
+pub fn f5(x: &[u32; SZ]) -> u32 {
+    x[0]
+}
+
+// To avoid lifetime shortening
+pub fn ite() {
+    let mut x: [u32; 2] = [0, 0];
+    if true {
+        let mut y: [u32; 2] = [0, 0];
+        index_mut_slice_u32_0(&mut x);
+        index_mut_slice_u32_0(&mut y);
+    }
+}
+
+pub fn zero_slice(a: &mut [u8]) {
+    let mut i: usize = 0;
+    let len = a.len();
+    while i < len {
+        a[i] = 0;
+        i += 1;
+    }
+}
+
+pub fn iter_mut_slice(a: &mut [u8]) {
+    let len = a.len();
+    let mut i = 0;
+    while i < len {
+        i += 1;
+    }
+}
+
+pub fn sum_mut_slice(a: &mut [u32]) -> u32 {
+    let mut i = 0;
+    let mut s = 0;
+    while i < a.len() {
+        s += a[i];
+        i += 1;
+    }
+    s
+}
diff --git a/tests/src/betree/Cargo.lock b/tests/src/betree/Cargo.lock
new file mode 100644
index 00000000..1bd274ad
--- /dev/null
+++ b/tests/src/betree/Cargo.lock
@@ -0,0 +1,299 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 3
+
+[[package]]
+name = "aho-corasick"
+version = "1.1.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8e60d3430d3a69478ad0993f19238d2df97c507009a52b3c10addcd7f6bcb916"
+dependencies = [
+ "memchr",
+]
+
+[[package]]
+name = "atty"
+version = "0.2.14"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d9b39be18770d11421cdb1b9947a45dd3f37e93092cbf377614828a319d5fee8"
+dependencies = [
+ "hermit-abi",
+ "libc",
+ "winapi",
+]
+
+[[package]]
+name = "betree"
+version = "0.1.0"
+dependencies = [
+ "env_logger",
+ "log",
+ "serde",
+ "serde_json",
+]
+
+[[package]]
+name = "env_logger"
+version = "0.8.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a19187fea3ac7e84da7dacf48de0c45d63c6a76f9490dae389aead16c243fce3"
+dependencies = [
+ "atty",
+ "humantime",
+ "log",
+ "regex",
+ "termcolor",
+]
+
+[[package]]
+name = "hermit-abi"
+version = "0.1.19"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "62b467343b94ba476dcb2500d242dadbb39557df889310ac77c5d99100aaac33"
+dependencies = [
+ "libc",
+]
+
+[[package]]
+name = "humantime"
+version = "2.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4"
+
+[[package]]
+name = "itoa"
+version = "1.0.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b"
+
+[[package]]
+name = "libc"
+version = "0.2.155"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "97b3888a4aecf77e811145cadf6eef5901f4782c53886191b2f693f24761847c"
+
+[[package]]
+name = "log"
+version = "0.4.21"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "90ed8c1e510134f979dbc4f070f87d4313098b704861a105fe34231c70a3901c"
+
+[[package]]
+name = "memchr"
+version = "2.7.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6c8640c5d730cb13ebd907d8d04b52f55ac9a2eec55b440c8892f40d56c76c1d"
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.83"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0b33eb56c327dec362a9e55b3ad14f9d2f0904fb5a5b03b513ab5465399e9f43"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.36"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0fa76aaf39101c457836aec0ce2316dbdc3ab723cdda1c6bd4e6ad4208acaca7"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "regex"
+version = "1.10.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c117dbdfde9c8308975b6a18d71f3f385c89461f7b3fb054288ecf2a2058ba4c"
+dependencies = [
+ "aho-corasick",
+ "memchr",
+ "regex-automata",
+ "regex-syntax",
+]
+
+[[package]]
+name = "regex-automata"
+version = "0.4.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "86b83b8b9847f9bf95ef68afb0b8e6cdb80f498442f5179a29fad448fcc1eaea"
+dependencies = [
+ "aho-corasick",
+ "memchr",
+ "regex-syntax",
+]
+
+[[package]]
+name = "regex-syntax"
+version = "0.8.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "adad44e29e4c806119491a7f06f03de4d1af22c3a680dd47f1e6e179439d1f56"
+
+[[package]]
+name = "ryu"
+version = "1.0.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f3cb5ba0dc43242ce17de99c180e96db90b235b8a9fdc9543c96d2209116bd9f"
+
+[[package]]
+name = "serde"
+version = "1.0.202"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "226b61a0d411b2ba5ff6d7f73a476ac4f8bb900373459cd00fab8512828ba395"
+dependencies = [
+ "serde_derive",
+]
+
+[[package]]
+name = "serde_derive"
+version = "1.0.202"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6048858004bcff69094cd972ed40a32500f153bd3be9f716b2eed2e8217c4838"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "serde_json"
+version = "1.0.117"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "455182ea6142b14f93f4bc5320a2b31c1f266b66a4a5c858b013302a5d8cbfc3"
+dependencies = [
+ "itoa",
+ "ryu",
+ "serde",
+]
+
+[[package]]
+name = "syn"
+version = "2.0.65"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d2863d96a84c6439701d7a38f9de935ec562c8832cc55d1dde0f513b52fad106"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "termcolor"
+version = "1.4.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "06794f8f6c5c898b3275aebefa6b8a1cb24cd2c6c79397ab15774837a0bc5755"
+dependencies = [
+ "winapi-util",
+]
+
+[[package]]
+name = "unicode-ident"
+version = "1.0.12"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b"
+
+[[package]]
+name = "winapi"
+version = "0.3.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5c839a674fcd7a98952e593242ea400abe93992746761e38641405d28b00f419"
+dependencies = [
+ "winapi-i686-pc-windows-gnu",
+ "winapi-x86_64-pc-windows-gnu",
+]
+
+[[package]]
+name = "winapi-i686-pc-windows-gnu"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6"
+
+[[package]]
+name = "winapi-util"
+version = "0.1.8"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4d4cc384e1e73b93bafa6fb4f1df8c41695c8a91cf9c4c64358067d15a7b6c6b"
+dependencies = [
+ "windows-sys",
+]
+
+[[package]]
+name = "winapi-x86_64-pc-windows-gnu"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f"
+
+[[package]]
+name = "windows-sys"
+version = "0.52.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d"
+dependencies = [
+ "windows-targets",
+]
+
+[[package]]
+name = "windows-targets"
+version = "0.52.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6f0713a46559409d202e70e28227288446bf7841d3211583a4b53e3f6d96e7eb"
+dependencies = [
+ "windows_aarch64_gnullvm",
+ "windows_aarch64_msvc",
+ "windows_i686_gnu",
+ "windows_i686_gnullvm",
+ "windows_i686_msvc",
+ "windows_x86_64_gnu",
+ "windows_x86_64_gnullvm",
+ "windows_x86_64_msvc",
+]
+
+[[package]]
+name = "windows_aarch64_gnullvm"
+version = "0.52.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7088eed71e8b8dda258ecc8bac5fb1153c5cffaf2578fc8ff5d61e23578d3263"
+
+[[package]]
+name = "windows_aarch64_msvc"
+version = "0.52.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9985fd1504e250c615ca5f281c3f7a6da76213ebd5ccc9561496568a2752afb6"
+
+[[package]]
+name = "windows_i686_gnu"
+version = "0.52.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "88ba073cf16d5372720ec942a8ccbf61626074c6d4dd2e745299726ce8b89670"
+
+[[package]]
+name = "windows_i686_gnullvm"
+version = "0.52.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "87f4261229030a858f36b459e748ae97545d6f1ec60e5e0d6a3d32e0dc232ee9"
+
+[[package]]
+name = "windows_i686_msvc"
+version = "0.52.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "db3c2bf3d13d5b658be73463284eaf12830ac9a26a90c717b7f771dfe97487bf"
+
+[[package]]
+name = "windows_x86_64_gnu"
+version = "0.52.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4e4246f76bdeff09eb48875a0fd3e2af6aada79d409d33011886d3e1581517d9"
+
+[[package]]
+name = "windows_x86_64_gnullvm"
+version = "0.52.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "852298e482cd67c356ddd9570386e2862b5673c85bd5f88df9ab6802b334c596"
+
+[[package]]
+name = "windows_x86_64_msvc"
+version = "0.52.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bec47e5bfd1bff0eeaf6d8b485cc1074891a197ab4225d504cb7a1ab88b02bf0"
diff --git a/tests/src/betree/Cargo.toml b/tests/src/betree/Cargo.toml
new file mode 100644
index 00000000..c05c7d93
--- /dev/null
+++ b/tests/src/betree/Cargo.toml
@@ -0,0 +1,13 @@
+[package]
+name = "betree"
+version = "0.1.0"
+authors = ["Son Ho <hosonmarc@gmail.com>"]
+edition = "2018"
+
+[dependencies]
+serde_json = "1.0.91"
+serde = { version = "1.0.152", features = ["derive"] }
+log = "0.4.17"
+env_logger = "0.8.4"
+
+# TODO: If we turn this package into a library, building the tests fails.
diff --git a/tests/src/betree/Makefile b/tests/src/betree/Makefile
new file mode 100644
index 00000000..7b41e56d
--- /dev/null
+++ b/tests/src/betree/Makefile
@@ -0,0 +1,11 @@
+.PHONY: all
+all: tests
+
+.PHONY: test
+test:
+	cargo rustc -- --test -Zpolonius
+	cd target/debug/ && ./betree
+
+.PHONY: clean
+clean:
+	cargo clean
diff --git a/tests/src/betree/README.md b/tests/src/betree/README.md
new file mode 100644
index 00000000..a71fe884
--- /dev/null
+++ b/tests/src/betree/README.md
@@ -0,0 +1 @@
+This project contains tests which require the Polonius borrow checker.
diff --git a/tests/src/betree/rust-toolchain b/tests/src/betree/rust-toolchain
new file mode 100644
index 00000000..9460b1a8
--- /dev/null
+++ b/tests/src/betree/rust-toolchain
@@ -0,0 +1,3 @@
+[toolchain]
+channel = "nightly-2023-06-02"
+components = [ "rustc-dev", "llvm-tools-preview" ]
diff --git a/tests/src/betree/src/betree.rs b/tests/src/betree/src/betree.rs
new file mode 100644
index 00000000..12f2847d
--- /dev/null
+++ b/tests/src/betree/src/betree.rs
@@ -0,0 +1,1084 @@
+//! The following module implements a minimal betree.
+//! We don't have loops for now, so we will need to update the code to remove
+//! the recursive functions at some point.
+//! We drew a lot of inspiration from the C++ [Be-Tree](https://github.com/oscarlab/Be-Tree).
+//! implementation.
+#![allow(dead_code)]
+
+use crate::betree_utils as utils;
+
+pub type NodeId = u64;
+pub type Key = u64;
+pub type Value = u64;
+
+type Map<K, V> = List<(K, V)>;
+
+/// We use linked lists for the maps from keys to messages/bindings
+pub(crate) enum List<T> {
+    Cons(T, Box<List<T>>),
+    Nil,
+}
+
+/// Every node has a unique identifier (the betree has a counter).
+/// Whenever we need to read/update the content of a node, we read/update
+/// the whole content from disk at once.
+///
+/// In order to make things simple, the content of each node is saved in
+/// a single file, identified by the node index. Also, we use json.
+///
+/// We don't reason about the content of the load/store node functions
+/// (which are assumed), while the purpose of this example is to illustrate the
+/// proof experience we have with Aeneas: we are not looking for performance here.
+///
+/// Rk.: in the future, we will directly use the functions from betree_utils
+/// and setup the translation to consider this module as assumed (i.e., no
+/// wrappers)
+fn load_internal_node(id: NodeId) -> InternalContent {
+    utils::load_internal_node(id)
+}
+
+/// See [load_internal_node].
+fn store_internal_node(id: NodeId, content: InternalContent) {
+    utils::store_internal_node(id, content)
+}
+
+/// See [load_internal_node].
+fn load_leaf_node(id: NodeId) -> LeafContent {
+    utils::load_leaf_node(id)
+}
+
+/// See [load_internal_node].
+fn store_leaf_node(id: NodeId, content: LeafContent) {
+    utils::store_leaf_node(id, content)
+}
+
+fn fresh_node_id(counter: &mut NodeId) -> NodeId {
+    let id = *counter;
+    *counter += 1;
+    id
+}
+
+/// We use this type to encode closures.
+/// See [Message::Upsert] and [upsert_update]
+pub enum UpsertFunState {
+    Add(u64),
+    Sub(u64),
+}
+
+/// A message - note that all those messages have to be linked to a key
+pub(crate) enum Message {
+    /// Insert a binding from value to key
+    Insert(Value),
+    /// Delete a binding from value to key
+    Delete,
+    /// [Upsert] is "query then update" (query a value, then update the binding
+    /// by using the result of the query). This is pretty expensive if we
+    /// actually *do* query, *then* update: queries are expensive, because
+    /// we potentially have to explore the tree in depth (and every time we
+    /// lookup a node, we have an expensive I/O operation).
+    /// Instead, we insert this [Upsert] message in the tree, which progressively
+    /// gets propagated to the children untils it gets applied (when we find an
+    /// [Insert], or when we reach a leaf).
+    ///
+    /// In practice, [Upsert] should store a closure. For now we don't have
+    /// support for function pointers and closures, so [Upsert] doesn't store
+    /// a closure and always applies the same update function. Note that the
+    /// [Value] stored in [Upsert] acts as a closure's state.
+    ///
+    /// The interest of this example is to split the proof in two:
+    /// 1. a very simple refinement proof (which is made simple by the fact that
+    ///    Aeneas takes care of the memory management proof obligations through
+    ///    the translation)
+    /// 2. a more complex functional proof.
+    /// We write a very general model of the b-epsilon tree, prove that it is
+    /// refined by the translated code in 1., then prove the general functional
+    /// correctness case once and for all in 2.
+    /// The idea is that once we add support for closures, we should be able to
+    /// update the Rust code, and all we would need to do on the proof side is
+    /// to update the refinement proof in 1., which should hopefully be
+    /// straightforward.
+    ///
+    /// Also note that if we don't have [Upsert], there is no point in using
+    /// b-epsilon trees, which have the particularity of storing messages:
+    /// b-trees and their variants work very well (and don't use messages).
+    ///
+    /// Note there is something interesting about the proofs we do for [Upsert].
+    /// When we use [Insert] or [Delete], we remove the upserts which are pending
+    /// for the key, because there is no point in applying them (there would be
+    /// if we wanted to leverage the fact that the update functions we apply may
+    /// be stateful).
+    /// The consequence is that we don't observe potentially failing executions of
+    /// the update functions. At the opposite, the specification of [Upsert] is
+    /// "greedy": we see [Upsert] as query then update. This means that the
+    /// implementation refines the specification only if we make sure that the
+    /// update function used for the upsert doesn't fail on the input we give it
+    /// (all this can be seen in the specification we prove about the be-tree).
+    Upsert(UpsertFunState),
+}
+
+/// Internal node content.
+///
+/// An internal node contains a map from keys to pending messages
+///
+/// Invariants:
+/// - the pairs (key, message) are sorted so that the keys are in increasing order
+/// - for a given key, there can be:
+///   - no message
+///   - one insert or delete message
+///   - a list of upsert messages. In that case, the upsert message are sorted
+///     from the *first* to the *last* added in the betree.
+pub(crate) type InternalContent = Map<Key, Message>;
+
+/// Leaf node content.
+///
+/// A leaf node contains a map from keys to values.
+/// We store the bindings in order of increasing key.
+pub(crate) type LeafContent = Map<Key, Value>;
+
+/// Internal node. See [Node].
+///
+/// An internal node contains a stack of messages (stored on disk and thus
+/// absent from the node itself), and two children.
+///
+/// When transmitting messages to the children: the messages/bindings for the
+/// keys < pivot are given to the left child, and those for the keys >= pivot
+/// are given to the right child.
+///
+/// Note that in Be-Tree the internal nodes have lists of children, which
+/// allows to do even smarter things: if an internal node has too many
+/// messages, then:
+/// - either it can transmit big batches of those messages to some of its
+///   children, in which case it does
+/// - or it can't, in which case it splits, because otherwise we have too
+///   many unefficient updates to perform (the aim really is to amortize
+///   the cost of I/O, which is achieved by minimizing the number of
+///   accesses to node contents)
+struct Internal {
+    id: NodeId,
+    pivot: Key,
+    left: Box<Node>,
+    right: Box<Node>,
+}
+
+/// Leaf node. See [Node]
+///
+/// A leaf node contains bindings (stored on disk, and thus absent from the
+/// node itself).
+struct Leaf {
+    id: NodeId,
+    /// The number of bindings in the node
+    size: u64,
+}
+
+/// A node in the BeTree.
+///
+/// The node's content is stored on disk (and hence absent from the node itself).
+///
+/// Note that we don't have clean/dirty nodes: all node contents are immediately
+/// written on disk upon being updated.
+enum Node {
+    /// An internal node (with children).
+    Internal(Internal),
+    /// A leaf node.
+    Leaf(Leaf),
+}
+
+/// The parameters of a BeTree, which control when to flush or split.
+struct Params {
+    /// The minimum number of messages we flush to the children.
+    /// We wait to reach 2 * min_flush_size before flushing to children.
+    /// If one of the children doesn't receive a number of
+    /// messages >= min_flush_size, we keep those messages in the parent
+    /// node. Of course, at least one of the two children will receive
+    /// flushed messages: this gives us that an internal node has at most
+    /// 2 * min_flush_size pending messages - 1.
+    min_flush_size: u64,
+    /// The maximum number of bindings we can store in a leaf node (if we
+    /// reach this number, we split).
+    split_size: u64,
+}
+
+struct NodeIdCounter {
+    next_node_id: NodeId,
+}
+
+impl NodeIdCounter {
+    fn new() -> Self {
+        NodeIdCounter { next_node_id: 0 }
+    }
+
+    fn fresh_id(&mut self) -> NodeId {
+        let id = self.next_node_id;
+        self.next_node_id += 1;
+        id
+    }
+}
+
+/// The BeTree itself
+pub struct BeTree {
+    /// The parameters of the BeTree
+    params: Params,
+    /// Every node has a unique id: we keep a counter to generate fresh ids
+    node_id_cnt: NodeIdCounter,
+    /// The root of the tree
+    root: Node,
+}
+
+/// The update function used for [Upsert].
+/// Will be removed once we have closures (or at least function pointers).
+/// This function just computes a saturated sum.
+/// Also note that it takes an option as input, for the previous value:
+/// we draw inspiration from the C++ Be-Tree implemenation, where
+/// in case the binding is not present, the closure stored in upsert is
+/// given a default value.
+pub fn upsert_update(prev: Option<Value>, st: UpsertFunState) -> Value {
+    // We just compute the sum, until it saturates
+    match prev {
+        Option::None => {
+            match st {
+                UpsertFunState::Add(v) => {
+                    // We consider the default value is 0, so we return 0 + v
+                    // (or we could fail - it doesn't really matter)
+                    v
+                }
+                UpsertFunState::Sub(_) => {
+                    // Same logic as for [sub], but this time we saturate at 0
+                    0
+                }
+            }
+        }
+        Option::Some(prev) => {
+            match st {
+                UpsertFunState::Add(v) => {
+                    // Note that Aeneas is a bit conservative about the max_usize
+                    let margin = u64::MAX - prev;
+                    // Check if we saturate
+                    if margin >= v {
+                        prev + v
+                    } else {
+                        u64::MAX
+                    }
+                }
+                UpsertFunState::Sub(v) => {
+                    // Check if we saturate
+                    if prev >= v {
+                        prev - v
+                    } else {
+                        0
+                    }
+                }
+            }
+        }
+    }
+}
+
+impl<T> List<T> {
+    fn len(&self) -> u64 {
+        match self {
+            List::Nil => 0,
+            List::Cons(_, tl) => 1 + tl.len(),
+        }
+    }
+
+    /// Split a list at a given length
+    fn split_at(self, n: u64) -> (List<T>, List<T>) {
+        if n == 0 {
+            (List::Nil, self)
+        } else {
+            match self {
+                List::Nil => unreachable!(),
+                List::Cons(hd, tl) => {
+                    let (ls0, ls1) = tl.split_at(n - 1);
+                    (List::Cons(hd, Box::new(ls0)), ls1)
+                }
+            }
+        }
+    }
+
+    /// Push an element at the front of the list.
+    fn push_front(&mut self, x: T) {
+        // Move under borrows: annoying...
+        let tl = std::mem::replace(self, List::Nil);
+        *self = List::Cons(x, Box::new(tl));
+    }
+
+    /// Pop the element at the front of the list
+    fn pop_front(&mut self) -> T {
+        // Move under borrows: annoying...
+        let ls = std::mem::replace(self, List::Nil);
+        match ls {
+            List::Nil => panic!(),
+            List::Cons(x, tl) => {
+                *self = *tl;
+                x
+            }
+        }
+    }
+
+    fn hd(&self) -> &T {
+        match self {
+            List::Nil => panic!(),
+            List::Cons(hd, _) => hd,
+        }
+    }
+}
+
+impl<T> Map<Key, T> {
+    fn head_has_key(&self, key: Key) -> bool {
+        match self {
+            List::Nil => false,
+            List::Cons(hd, _) => hd.0 == key,
+        }
+    }
+
+    /// Partition the map between two maps:
+    /// - a first map where the keys < pivot
+    /// - a second map where the keys >= pivot
+    /// Note that the bindings in the map are supposed to be sorted in
+    /// order of increasing keys.
+    fn partition_at_pivot(self, pivot: Key) -> (Map<Key, T>, Map<Key, T>) {
+        match self {
+            List::Nil => (List::Nil, List::Nil),
+            List::Cons(hd, tl) => {
+                if hd.0 >= pivot {
+                    (List::Nil, List::Cons(hd, tl))
+                } else {
+                    let (ls0, ls1) = tl.partition_at_pivot(pivot);
+                    (List::Cons(hd, Box::new(ls0)), ls1)
+                }
+            }
+        }
+    }
+}
+
+impl Leaf {
+    /// Split a leaf into an internal node with two children.
+    ///
+    /// The leaf should have exactly 2 * split_size elements.
+    /// Also, we use the fact that the keys are sorted in increasing order.
+    fn split(
+        &self,
+        content: Map<Key, Value>,
+        params: &Params,
+        node_id_cnt: &mut NodeIdCounter,
+    ) -> Internal {
+        // Split the content
+        let (content0, content1) = content.split_at(params.split_size);
+        // Get the pivot
+        let pivot = content1.hd().0;
+        // Create the two nodes
+        let id0 = node_id_cnt.fresh_id();
+        let id1 = node_id_cnt.fresh_id();
+        let left = Leaf {
+            id: id0,
+            size: params.split_size,
+        };
+        let right = Leaf {
+            id: id1,
+            size: params.split_size,
+        };
+        // Store the content
+        store_leaf_node(id0, content0);
+        store_leaf_node(id1, content1);
+        // Return
+        Internal {
+            id: self.id,
+            pivot,
+            left: Box::new(Node::Leaf(left)),
+            right: Box::new(Node::Leaf(right)),
+        }
+    }
+}
+
+impl Internal {
+    /// Small utility: lookup a value in the children nodes.
+    fn lookup_in_children(&mut self, key: Key) -> Option<Value> {
+        if key < self.pivot {
+            self.left.lookup(key)
+        } else {
+            self.right.lookup(key)
+        }
+    }
+
+    /// Flush the messages in an internal node to its children.
+    /// Note that when flushing, we send messages to a child only if there
+    /// are more than min_flush_size messages to send. Also, we flush only
+    /// if the number of messages in the current node is >= 2* num_flush_size.
+    ///
+    /// The function returns the messages we couldn't flush to the children
+    /// nodes.
+    fn flush<'a>(
+        &'a mut self,
+        params: &Params,
+        node_id_cnt: &'a mut NodeIdCounter,
+        content: Map<Key, Message>,
+    ) -> Map<Key, Message> {
+        // Partition the messages
+        let (msgs_left, msgs_right) = content.partition_at_pivot(self.pivot);
+        // Check if we need to flush to the left child
+        let len_left = msgs_left.len();
+        if len_left >= params.min_flush_size {
+            // Flush to the left
+            self.left.apply_messages(params, node_id_cnt, msgs_left);
+            // Check if we need to flush to the right
+            let len_right = msgs_right.len();
+            if len_right >= params.min_flush_size {
+                self.right.apply_messages(params, node_id_cnt, msgs_right);
+                // No messages remain in the current node
+                List::Nil
+            } else {
+                // We keep the messages which belong to the right node
+                msgs_right
+            }
+        } else {
+            // Don't flush to the left: we necessarily flush to the right
+            self.right.apply_messages(params, node_id_cnt, msgs_right);
+            // We keep the messages which belong to the left node
+            msgs_left
+        }
+    }
+}
+
+impl Node {
+    /// Apply a list of message to ourselves: leaf node case
+    fn apply_messages_to_leaf<'a>(
+        bindings: &'a mut Map<Key, Value>,
+        new_msgs: List<(Key, Message)>,
+    ) {
+        match new_msgs {
+            List::Nil => (),
+            List::Cons(new_msg, new_msgs_tl) => {
+                Node::apply_to_leaf(bindings, new_msg.0, new_msg.1);
+                Node::apply_messages_to_leaf(bindings, *new_msgs_tl);
+            }
+        }
+    }
+
+    /// Apply a message to ourselves: leaf node case
+    ///
+    /// This simply updates the bindings.
+    fn apply_to_leaf<'a>(bindings: &'a mut Map<Key, Value>, key: Key, new_msg: Message) {
+        // Retrieve a mutable borrow to the position of the binding, if there is
+        // one, or to the end of the list
+        let bindings = Node::lookup_mut_in_bindings(key, bindings);
+        // Check if we point to a binding which has the key we are looking for
+        if bindings.head_has_key(key) {
+            // We need to pop the binding, and may need to reuse the
+            // previous value (for an upsert)
+            let hd = bindings.pop_front();
+            // Match over the message
+            match new_msg {
+                Message::Insert(v) => {
+                    bindings.push_front((key, v));
+                }
+                Message::Delete => {
+                    // Nothing to do: we popped the binding
+                    ()
+                }
+                Message::Upsert(s) => {
+                    let v = upsert_update(Option::Some(hd.1), s);
+                    bindings.push_front((key, v));
+                }
+            }
+        } else {
+            // Key not found: simply insert
+            match new_msg {
+                Message::Insert(v) => {
+                    bindings.push_front((key, v));
+                }
+                Message::Delete => {
+                    // Nothing to do
+                    ()
+                }
+                Message::Upsert(s) => {
+                    let v = upsert_update(Option::None, s);
+                    bindings.push_front((key, v));
+                }
+            }
+        }
+    }
+
+    /// Apply a list of message to ourselves: internal node case
+    fn apply_messages_to_internal<'a>(
+        msgs: &'a mut Map<Key, Message>,
+        new_msgs: List<(Key, Message)>,
+    ) {
+        match new_msgs {
+            List::Nil => (),
+            List::Cons(new_msg, new_msgs_tl) => {
+                Node::apply_to_internal(msgs, new_msg.0, new_msg.1);
+                Node::apply_messages_to_internal(msgs, *new_msgs_tl);
+            }
+        }
+    }
+
+    /// Apply a message to ourselves: internal node case
+    ///
+    /// This basically inserts a message in a messages stack. However,
+    /// we may need to filter previous messages: for insert, if we insert an
+    /// [Insert] in a stack which contains an [Insert] or a [Delete] for the
+    /// same key, we replace this old message with the new one.
+    fn apply_to_internal<'a>(msgs: &'a mut Map<Key, Message>, key: Key, new_msg: Message) {
+        // Lookup the first message for [key] (if there is no message for [key],
+        // we get a mutable borrow to the position in the list where we need
+        // to insert the new message).
+        let msgs = Node::lookup_first_message_for_key(key, msgs);
+        // What we do is not the same, depending on whether there is already
+        // a message or not.
+        if msgs.head_has_key(key) {
+            // We need to check the current message
+            match new_msg {
+                Message::Insert(_) | Message::Delete => {
+                    // If [Insert] or [Delete]: filter the current
+                    // messages, and insert the new one
+                    Node::filter_messages_for_key(key, msgs);
+                    msgs.push_front((key, new_msg));
+                }
+                Message::Upsert(s) => {
+                    // If [Update]: we need to take into account the
+                    // previous messages.
+                    match msgs.hd().1 {
+                        Message::Insert(prev) => {
+                            // There should be exactly one [Insert]:
+                            // pop it, compute the result of the [Upsert]
+                            // and insert this result
+                            let v = upsert_update(Option::Some(prev), s);
+                            let _ = msgs.pop_front();
+                            msgs.push_front((key, Message::Insert(v)));
+                        }
+                        Message::Delete => {
+                            // There should be exactly one [Delete]
+                            // message : pop it, compute the result of
+                            // the [Upsert], and insert this result
+                            let _ = msgs.pop_front();
+                            let v = upsert_update(Option::None, s);
+                            msgs.push_front((key, Message::Insert(v)));
+                        }
+                        Message::Upsert(_) => {
+                            // There may be several msgs upserts:
+                            // we need to insert the new message at
+                            // the end of the list of upserts (so
+                            // that later we can apply them all in
+                            // proper order).
+                            let msgs = Node::lookup_first_message_after_key(key, msgs);
+                            msgs.push_front((key, Message::Upsert(s)));
+                        }
+                    }
+                }
+            }
+        } else {
+            // No pending message for [key]: simply add the new message
+            msgs.push_front((key, new_msg))
+        }
+    }
+
+    /// Apply a message to ourselves
+    fn apply<'a>(
+        &'a mut self,
+        params: &Params,
+        node_id_cnt: &'a mut NodeIdCounter,
+        key: Key,
+        new_msg: Message,
+    ) {
+        let msgs = List::Cons((key, new_msg), Box::new(List::Nil));
+        self.apply_messages(params, node_id_cnt, msgs);
+    }
+
+    /// Apply a list of messages to ourselves
+    fn apply_messages<'a>(
+        &'a mut self,
+        params: &Params,
+        node_id_cnt: &'a mut NodeIdCounter,
+        msgs: List<(Key, Message)>,
+    ) {
+        match self {
+            Node::Leaf(node) => {
+                // Load the content from disk
+                let mut content = load_leaf_node(node.id);
+                // Insert
+                Node::apply_messages_to_leaf(&mut content, msgs);
+                // Check if we need to split - in the future, we might want to
+                // do something smarter to compute the number of messages
+                let len = content.len();
+                if len >= 2 * params.split_size {
+                    // Split
+                    let new_node = node.split(content, params, node_id_cnt);
+                    // Store the content to disk
+                    store_leaf_node(node.id, List::Nil);
+                    // Update the node
+                    *self = Node::Internal(new_node);
+                } else {
+                    // Update the size if necessary
+                    node.size = len;
+                    // Store the content to disk
+                    store_leaf_node(node.id, content);
+                }
+            }
+            Node::Internal(node) => {
+                // Load the content from disk
+                let mut content = load_internal_node(node.id);
+                // Insert
+                Node::apply_messages_to_internal(&mut content, msgs);
+                // Check if we need to flush - in the future, we might want to
+                // do something smarter to compute the number of messages
+                let num_msgs = content.len();
+                if num_msgs >= params.min_flush_size {
+                    content = node.flush(params, node_id_cnt, content);
+                }
+                // Store the content to disk
+                store_internal_node(node.id, content)
+            }
+        }
+    }
+
+    /// Lookup a value in a list of bindings.
+    /// Note that the values should be stored in order of increasing key.
+    fn lookup_in_bindings(key: Key, bindings: &Map<Key, Value>) -> Option<Value> {
+        match bindings {
+            List::Nil => Option::None,
+            List::Cons(hd, tl) => {
+                if hd.0 == key {
+                    Option::Some(hd.1)
+                } else if hd.0 > key {
+                    Option::None
+                } else {
+                    Node::lookup_in_bindings(key, tl)
+                }
+            }
+        }
+    }
+
+    /// Lookup a value in a list of bindings, and return a borrow to the position
+    /// where the value is (or should be inserted, if the key is not in the bindings).
+    fn lookup_mut_in_bindings<'a>(
+        key: Key,
+        bindings: &'a mut Map<Key, Value>,
+    ) -> &'a mut Map<Key, Value> {
+        match bindings {
+            List::Nil => bindings,
+            List::Cons(hd, tl) => {
+                // This requires Polonius
+                if hd.0 >= key {
+                    bindings
+                } else {
+                    Node::lookup_mut_in_bindings(key, tl)
+                }
+            }
+        }
+    }
+
+    /// Filter all the messages which concern [key].
+    ///
+    /// Note that the stack of messages must start with a message for [key]:
+    /// we stop filtering at the first message which is not about [key].
+    fn filter_messages_for_key<'a>(key: Key, msgs: &'a mut Map<Key, Message>) {
+        match msgs {
+            List::Nil => (),
+            List::Cons((k, _), _) => {
+                if *k == key {
+                    msgs.pop_front();
+                    Node::filter_messages_for_key(key, msgs);
+                } else {
+                    // Stop
+                    ()
+                }
+            }
+        }
+    }
+
+    fn lookup_first_message_after_key<'a>(
+        key: Key,
+        msgs: &'a mut Map<Key, Message>,
+    ) -> &'a mut Map<Key, Message> {
+        match msgs {
+            List::Nil => msgs,
+            List::Cons((k, _), next_msgs) => {
+                if *k == key {
+                    Node::lookup_first_message_after_key(key, next_msgs)
+                } else {
+                    msgs
+                }
+            }
+        }
+    }
+
+    /// Returns the value bound to a key.
+    /// Note that while looking for the binding, we might reorganize the
+    /// internals of the betree to apply or flush messages: hence the mutable
+    /// borrow.
+    fn lookup<'a>(&'a mut self, key: Key) -> Option<Value> {
+        match self {
+            Node::Leaf(node) => {
+                // Load the node content
+                let bindings = load_leaf_node(node.id);
+                // Just lookup the binding in the map
+                Node::lookup_in_bindings(key, &bindings)
+            }
+            Node::Internal(node) => {
+                // Load the node content
+                let mut msgs = load_internal_node(node.id);
+                // Look for the first message pending for the key.
+                // Note that we maintain the following invariants:
+                // - if there are > 1 messages, they must be upsert messages only
+                // - the upsert messages are sorted from the *first* added to the
+                //   *last* added to the betree.
+                // Also note that if there are upsert messages, we have to apply
+                // them immediately.
+                //
+                // Rk.: [lookup_first_message_for_key] below returns a borrow to
+                // the portion of the list we will update (if we have upserts,
+                // we will apply the messages, filter them while doing so,
+                // insert an [Insert] message, etc.). Should be interesting
+                // to see how the proof experience with the backward functions
+                // is at this for this piece of code. Note that this was inpired
+                // by Be-Tree.
+                // Also, can't wait to see how all this will work with loops.
+                let pending = Node::lookup_first_message_for_key(key, &mut msgs);
+                match pending {
+                    List::Nil => {
+                        // Nothing: dive into the children
+                        node.lookup_in_children(key)
+                    }
+                    List::Cons((k, msg), _) => {
+                        // Check if the borrow which points inside the messages
+                        // stack points to a message for [key]
+                        if *k != key {
+                            // Note the same key: dive into the children
+                            node.lookup_in_children(key)
+                        } else {
+                            // Same key: match over the message for this key
+                            match msg {
+                                Message::Insert(v) => Some(*v),
+                                Message::Delete => None,
+                                Message::Upsert(_) => {
+                                    // There are pending upserts: we have no choice but to
+                                    // apply them.
+                                    //
+                                    // Rk.: rather than calling [lookup], we could actually
+                                    // go down the tree accumulating upserts. On the other
+                                    // hand, the key is now "hotter", so it is not a bad
+                                    // idea to keep it as close to the root as possible.
+                                    // Note that what we do is what Be-Tree does.
+                                    //
+                                    // First, lookup the value from the children.
+                                    let v = node.lookup_in_children(key);
+                                    // Apply the pending updates, and replace them with
+                                    // an [Insert] containing the updated value.
+                                    //
+                                    // Rk.: Be-Tree doesn't seem to store the newly computed
+                                    // value, which I don't understand.
+                                    let v = Node::apply_upserts(pending, v, key);
+                                    // Update the node content
+                                    store_internal_node(node.id, msgs);
+                                    // Return the value
+                                    Option::Some(v)
+                                }
+                            }
+                        }
+                    }
+                }
+            }
+        }
+    }
+
+    /// Return a mutable borrow to the first message whose key is <= than [key].
+    /// If the key is [key], then it is the first message about [key].
+    /// Otherwise, it gives us a mutable borrow to the place where we need
+    /// to insert new messages (note that the borrow may point to the end
+    /// of the list).
+    fn lookup_first_message_for_key<'a>(
+        key: Key,
+        msgs: &'a mut Map<Key, Message>,
+    ) -> &'a mut Map<Key, Message> {
+        match msgs {
+            List::Nil => msgs,
+            List::Cons(x, next_msgs) => {
+                // Rk.: we need Polonius here
+                // We wouldn't need Polonius if directly called the proper
+                // function to make the modifications here (because we wouldn't
+                // need to return anything). However, it would not be very
+                // idiomatic, especially with regards to the fact that we will
+                // rewrite everything with loops at some point.
+                if x.0 >= key {
+                    msgs
+                } else {
+                    Node::lookup_first_message_for_key(key, next_msgs)
+                }
+            }
+        }
+    }
+
+    /// Apply the upserts from the current messages stack to a looked up value.
+    ///
+    /// The input mutable borrow must point to the first upsert message in the
+    /// messages stack of the current node. We remove the messages from the stack
+    /// while applying them.
+    /// Note that if there are no more upserts to apply, then the value must be
+    /// `Some`. Also note that we use the invariant that in the message stack,
+    /// upsert messages are sorted from the first to the last to apply.
+    fn apply_upserts(msgs: &mut Map<Key, Message>, prev: Option<Value>, key: Key) -> Value {
+        if msgs.head_has_key(key) {
+            // Pop the front message.
+            // Note that it *must* be an upsert.
+            let msg = msgs.pop_front();
+            match msg.1 {
+                Message::Upsert(s) => {
+                    // Apply the update
+                    let v = upsert_update(prev, s);
+                    let prev = Option::Some(v);
+                    // Continue
+                    Node::apply_upserts(msgs, prev, key)
+                }
+                _ => {
+                    // Unreachable: we can only have [Upsert] messages
+                    // for the key
+                    unreachable!();
+                }
+            }
+        } else {
+            // We applied all the upsert messages: simply put an [Insert]
+            // message and return the value.
+            let v = prev.unwrap();
+            msgs.push_front((key, Message::Insert(v)));
+            return v;
+        }
+    }
+}
+
+impl BeTree {
+    pub fn new(min_flush_size: u64, split_size: u64) -> Self {
+        let mut node_id_cnt = NodeIdCounter::new();
+        let id = node_id_cnt.fresh_id();
+        let root = Node::Leaf(Leaf { id, size: 0 });
+        store_leaf_node(id, List::Nil);
+        let params = Params {
+            min_flush_size,
+            split_size,
+        };
+        BeTree {
+            params,
+            node_id_cnt,
+            root,
+        }
+    }
+
+    /// Apply a message to the tree.
+    ///
+    /// This is an auxiliary function.
+    fn apply(&mut self, key: Key, msg: Message) {
+        self.root
+            .apply(&self.params, &mut self.node_id_cnt, key, msg)
+    }
+
+    /// Insert a binding from [key] to [value]
+    pub fn insert(&mut self, key: Key, value: Value) {
+        let msg = Message::Insert(value);
+        self.apply(key, msg);
+    }
+
+    /// Delete the bindings for [key]
+    pub fn delete(&mut self, key: Key) {
+        let msg = Message::Delete;
+        self.apply(key, msg);
+    }
+
+    /// Apply a query-update
+    pub fn upsert(&mut self, key: Key, upd: UpsertFunState) {
+        let msg = Message::Upsert(upd);
+        self.apply(key, msg);
+    }
+
+    /// Returns the value bound to a key.
+    /// Note that while looking for the binding, we might reorganize the
+    /// internals of the betree to apply or flush messages: hence the mutable
+    /// borrow.
+    pub fn lookup<'a>(&'a mut self, key: Key) -> Option<Value> {
+        self.root.lookup(key)
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use crate::betree::*;
+    use std::collections::HashMap;
+    use std::fmt::{Display, Error, Formatter};
+    use std::vec::Vec;
+
+    struct Maps {
+        betree: BeTree,
+        refmap: HashMap<Key, Value>,
+    }
+
+    impl Maps {
+        fn insert(&mut self, k: Key, v: Value) {
+            log::trace!("insert: {} -> {}", k, v);
+            self.betree.insert(k, v);
+            self.refmap.insert(k, v);
+        }
+
+        fn delete(&mut self, k: Key) {
+            log::trace!("delete: {}", k);
+            self.betree.delete(k);
+            self.refmap.remove(&k);
+        }
+
+        /// This function doesn't return a value: it simply checks that the
+        /// b-epsilon tree and the reference map have the same bindings.
+        fn lookup(&mut self, k: Key) {
+            let v0 = self.betree.lookup(k);
+            let v1 = self.refmap.get(&k).map(|x| *x);
+            log::trace!("lookup {k}: betree: {:?}, ref: {:?}", v0, v1);
+            assert!(v0 == v1);
+        }
+
+        /// Only testing the addition (the choice of the update function doesn't
+        /// make much difference)
+        fn upsert(&mut self, k: Key, v: Value) {
+            log::trace!("upsert: {} -> add({})", k, v);
+            self.betree.upsert(k, UpsertFunState::Add(v));
+            let prev = self.refmap.get(&k).map(|x| *x);
+            let nv = upsert_update(prev, UpsertFunState::Add(v));
+            self.refmap.insert(k, nv);
+        }
+
+        /// Check that all the bindings in the betree give the same result as the
+        /// reference.
+        ///
+        /// Rk.: looking up actually updates the b-epsilon tree.
+        fn check_equal(&mut self) {
+            let keys: Vec<Key> = self.refmap.keys().map(|k| *k).collect();
+            for k in keys {
+                self.lookup(k);
+            }
+        }
+    }
+
+    impl Display for Map<Key, Value> {
+        fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
+            match self {
+                List::Nil => write!(f, ""),
+                List::Cons(hd, tl) => {
+                    write!(f, "{} -> {}, ", hd.0, hd.1).unwrap();
+                    tl.fmt(f)
+                }
+            }
+        }
+    }
+
+    impl Display for UpsertFunState {
+        fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
+            match self {
+                UpsertFunState::Add(v) => write!(f, "add({})", v),
+                UpsertFunState::Sub(v) => write!(f, "sub({})", v),
+            }
+        }
+    }
+
+    impl Display for Message {
+        fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
+            match self {
+                Message::Insert(v) => write!(f, "insert({})", v),
+                Message::Delete => write!(f, "delete"),
+                Message::Upsert(v) => write!(f, "upsert({})", v),
+            }
+        }
+    }
+
+    impl Display for Map<Key, Message> {
+        fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
+            match self {
+                List::Nil => write!(f, ""),
+                List::Cons(hd, tl) => {
+                    write!(f, "{} -> {}, ", hd.0, hd.1).unwrap();
+                    tl.fmt(f)
+                }
+            }
+        }
+    }
+
+    impl Node {
+        fn fmt(&self, indent: &String, f: &mut Formatter<'_>) -> Result<(), Error> {
+            match self {
+                Node::Leaf(node) => {
+                    let content = load_leaf_node(node.id);
+                    write!(f, "{}{}: [{}]", indent, node.id, content)
+                }
+                Node::Internal(node) => {
+                    let content = load_internal_node(node.id);
+                    let indent1 = format!("{}  ", indent).to_string();
+                    write!(
+                        f,
+                        "{}{{\n{}{},\n{}[{}],",
+                        indent, indent, node.id, indent, &content
+                    )
+                    .unwrap();
+                    write!(f, "\n{}", indent1).unwrap();
+                    node.left.fmt(&indent1, f).unwrap();
+                    write!(f, "\n{}", indent1).unwrap();
+                    node.right.fmt(&indent1, f).unwrap();
+                    write!(f, "\n{}}}", indent)
+                }
+            }
+        }
+    }
+
+    impl Display for BeTree {
+        fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
+            self.root.fmt(&"".to_string(), f)
+        }
+    }
+
+    #[test]
+    fn test1() {
+        // Initialize the logger
+        env_logger::init();
+
+        let mut m = Maps {
+            betree: BeTree::new(5, 5),
+            refmap: HashMap::new(),
+        };
+        let num_keys = 100;
+
+        // Insert bindings
+        for k in 0..num_keys {
+            let v = 2 * k + 1;
+            m.insert(k, v);
+            log::trace!("\n{}", &m.betree);
+        }
+
+        // Make various queries
+        for kb in 0..(10 * num_keys) {
+            let k = kb % num_keys;
+            match k % 4 {
+                0 => {
+                    let v = 3 * k + 2;
+                    m.insert(k, v);
+                }
+                1 => {
+                    m.delete(k);
+                }
+                2 => {
+                    let v = kb % 7;
+                    m.upsert(k, v);
+                }
+                3 => {
+                    m.lookup(k);
+                }
+                _ => {
+                    unreachable!();
+                }
+            }
+            log::trace!("\n{}", &m.betree);
+        }
+
+        // Check that the b-epsilon tree didn't diverge (we check twice,
+        // because looking up performs updates that we also want to test)
+        m.check_equal();
+        m.check_equal();
+    }
+    fn range_insert(tree: &mut BeTree, start: Key, end: Key) {
+        for k in start..end {
+            tree.insert(k, 2 * k + 1);
+        }
+    }
+}
diff --git a/tests/src/betree/src/betree_utils.rs b/tests/src/betree/src/betree_utils.rs
new file mode 100644
index 00000000..fd269f4d
--- /dev/null
+++ b/tests/src/betree/src/betree_utils.rs
@@ -0,0 +1,155 @@
+//! The following module implements utilities for [betree.rs].
+//! Those utilities are only used for serialization/deserialization (we don't
+//! reason about them).
+//!
+//! The issue is that we can't derive serialization/deserialization
+//! implementations directly in betree.rs, otherwise we can't translate.
+//! We could have hacked in Aeneas to skip those implementations, but I'd
+//! rather put a little bit of engineering time into this file, while thinking
+//! about a cleaner way of doing this in general. The following file is not
+//! difficult to write and maintain anyway.
+#![allow(dead_code)]
+
+use crate::betree::{
+    InternalContent, Key, LeafContent, List, Message, NodeId, UpsertFunState, Value,
+};
+use serde::{Deserialize, Serialize};
+use std::fs::File;
+use std::vec::Vec;
+
+/// Note that I tried using Serde's facilities to define serialization/
+/// deserialization functions for external types, but it proved cumbersome
+/// for the betree case.
+#[derive(Serialize, Deserialize)]
+pub enum UpsertFunStateSerde {
+    Add(u64),
+    Sub(u64),
+}
+
+impl UpsertFunStateSerde {
+    fn to_state(self) -> UpsertFunState {
+        match self {
+            UpsertFunStateSerde::Add(v) => UpsertFunState::Add(v),
+            UpsertFunStateSerde::Sub(v) => UpsertFunState::Sub(v),
+        }
+    }
+
+    fn from_state(msg: UpsertFunState) -> Self {
+        match msg {
+            UpsertFunState::Add(v) => UpsertFunStateSerde::Add(v),
+            UpsertFunState::Sub(v) => UpsertFunStateSerde::Sub(v),
+        }
+    }
+}
+
+/// Same remark as for [UpsertFunStateSerde]
+#[derive(Serialize, Deserialize)]
+enum MessageSerde {
+    Insert(Value),
+    Delete,
+    Upsert(UpsertFunStateSerde),
+}
+
+impl MessageSerde {
+    fn to_msg(self) -> Message {
+        match self {
+            MessageSerde::Insert(v) => Message::Insert(v),
+            MessageSerde::Delete => Message::Delete,
+            MessageSerde::Upsert(v) => Message::Upsert(v.to_state()),
+        }
+    }
+
+    fn from_msg(msg: Message) -> Self {
+        match msg {
+            Message::Insert(v) => MessageSerde::Insert(v),
+            Message::Delete => MessageSerde::Delete,
+            Message::Upsert(v) => MessageSerde::Upsert(UpsertFunStateSerde::from_state(v)),
+        }
+    }
+}
+
+// For some reason, I don't manage to make that in an impl...
+pub(crate) fn list_from_vec<T>(mut v: Vec<T>) -> List<T> {
+    // We need to reverse
+    v.reverse();
+    let mut l = List::Nil;
+    for x in v.into_iter() {
+        l = List::Cons(x, Box::new(l));
+    }
+    l
+}
+
+// For some reason, I don't manage to make that in an impl...
+pub(crate) fn list_to_vec<T>(mut l: List<T>) -> Vec<T> {
+    let mut v = Vec::new();
+    loop {
+        match l {
+            List::Nil => break,
+            List::Cons(hd, tl) => {
+                v.push(hd);
+                l = *tl;
+            }
+        }
+    }
+    v
+}
+
+/// See the equivalent function in betree.rs
+pub(crate) fn load_internal_node(id: NodeId) -> InternalContent {
+    // Open the file
+    std::fs::create_dir_all("tmp").unwrap();
+    let filename = format!("tmp/node{}", id).to_string();
+    // Read
+    let f = File::open(filename).unwrap();
+    // Serde makes things easy
+    let c: Vec<(Key, MessageSerde)> = serde_json::from_reader(&f).unwrap();
+    let c: Vec<(Key, Message)> = c
+        .into_iter()
+        .map(|(key, msg)| (key, msg.to_msg()))
+        .collect();
+    // Convert
+    list_from_vec(c)
+}
+
+/// See the equivalent function in betree.rs
+pub(crate) fn store_internal_node(id: NodeId, content: InternalContent) {
+    // Open the file
+    std::fs::create_dir_all("tmp").unwrap();
+    let filename = format!("tmp/node{}", id).to_string();
+    // Write
+    let f = File::create(filename).unwrap();
+    // Convert
+    let v: Vec<(Key, Message)> = list_to_vec(content);
+    let v: Vec<(Key, MessageSerde)> = v
+        .into_iter()
+        .map(|(k, msg)| (k, MessageSerde::from_msg(msg)))
+        .collect();
+    // Serde makes things easy
+    serde_json::to_writer(&f, &v).unwrap();
+}
+
+/// See the equivalent function in betree.rs
+pub(crate) fn load_leaf_node(id: NodeId) -> LeafContent {
+    // Open the file
+    std::fs::create_dir_all("tmp").unwrap();
+    let filename = format!("tmp/node{}", id).to_string();
+    // Read
+    let f = File::open(filename).unwrap();
+    // Serde makes things easy
+    let c: Vec<(Key, Value)> = serde_json::from_reader(&f).unwrap();
+    // Convert
+    list_from_vec(c)
+}
+
+/// See the equivalent function in betree.rs
+pub(crate) fn store_leaf_node(id: NodeId, content: LeafContent) {
+    // Open the file
+    std::fs::create_dir_all("tmp").unwrap();
+    let filename = format!("tmp/node{}", id).to_string();
+    // Write
+    let f = File::create(filename).unwrap();
+    // Convert
+    let v: Vec<(Key, Value)> = list_to_vec(content);
+    // Serde makes things easy
+    serde_json::to_writer(&f, &v).unwrap();
+}
diff --git a/tests/src/betree/src/main.rs b/tests/src/betree/src/main.rs
new file mode 100644
index 00000000..64e9f7db
--- /dev/null
+++ b/tests/src/betree/src/main.rs
@@ -0,0 +1,4 @@
+mod betree;
+mod betree_utils;
+
+fn main() {}
diff --git a/tests/src/bitwise.rs b/tests/src/bitwise.rs
new file mode 100644
index 00000000..9f48cb04
--- /dev/null
+++ b/tests/src/bitwise.rs
@@ -0,0 +1,27 @@
+//! Exercise the bitwise operations
+
+pub fn shift_u32(a: u32) -> u32 {
+    let i: usize = 16;
+    let mut t = a >> i;
+    t <<= i;
+    t
+}
+
+pub fn shift_i32(a: i32) -> i32 {
+    let i: isize = 16;
+    let mut t = a >> i;
+    t <<= i;
+    t
+}
+
+pub fn xor_u32(a: u32, b: u32) -> u32 {
+    a ^ b
+}
+
+pub fn or_u32(a: u32, b: u32) -> u32 {
+    a | b
+}
+
+pub fn and_u32(a: u32, b: u32) -> u32 {
+    a & b
+}
diff --git a/tests/src/constants.rs b/tests/src/constants.rs
new file mode 100644
index 00000000..83904eed
--- /dev/null
+++ b/tests/src/constants.rs
@@ -0,0 +1,96 @@
+//! Tests with constants
+
+// Integers
+
+pub const X0: u32 = 0;
+
+pub const X1: u32 = u32::MAX;
+
+#[allow(clippy::let_and_return)]
+pub const X2: u32 = {
+    let x = 3;
+    x
+};
+
+pub const X3: u32 = incr(32);
+
+pub const fn incr(n: u32) -> u32 {
+    n + 1
+}
+
+// Pairs
+
+pub const fn mk_pair0(x: u32, y: u32) -> (u32, u32) {
+    (x, y)
+}
+
+pub const fn mk_pair1(x: u32, y: u32) -> Pair<u32, u32> {
+    Pair { x, y }
+}
+
+pub const P0: (u32, u32) = mk_pair0(0, 1);
+pub const P1: Pair<u32, u32> = mk_pair1(0, 1);
+pub const P2: (u32, u32) = (0, 1);
+pub const P3: Pair<u32, u32> = Pair { x: 0, y: 1 };
+
+pub struct Pair<T1, T2> {
+    pub x: T1,
+    pub y: T2,
+}
+
+pub const Y: Wrap<i32> = Wrap::new(2);
+
+pub const fn unwrap_y() -> i32 {
+    Y.value
+}
+
+pub const YVAL: i32 = unwrap_y();
+
+pub struct Wrap<T> {
+    value: T,
+}
+
+impl<T> Wrap<T> {
+    pub const fn new(value: T) -> Wrap<T> {
+        Wrap { value }
+    }
+}
+
+// Additions
+
+pub const fn get_z1() -> i32 {
+    const Z1: i32 = 3;
+    Z1
+}
+
+pub const fn add(a: i32, b: i32) -> i32 {
+    a + b
+}
+
+pub const fn get_z2() -> i32 {
+    add(Q1, add(get_z1(), Q3))
+}
+
+pub const Q1: i32 = 5;
+pub const Q2: i32 = Q1;
+pub const Q3: i32 = add(Q2, 3);
+
+// Static
+
+pub static S1: u32 = 6;
+pub static S2: u32 = incr(S1);
+pub static S3: Pair<u32, u32> = P3;
+pub static S4: Pair<u32, u32> = mk_pair1(7, 8);
+
+// Constants with generics
+pub struct V<const N: usize, T> {
+    pub x: [T; N],
+}
+
+impl<const N: usize, T> V<N, T> {
+    pub const LEN: usize = N;
+}
+
+pub fn use_v<const N: usize, T>() -> usize {
+    V::<N, T>::LEN
+}
diff --git a/tests/src/demo.rs b/tests/src/demo.rs
new file mode 100644
index 00000000..bc74cc8b
--- /dev/null
+++ b/tests/src/demo.rs
@@ -0,0 +1,111 @@
+#![allow(clippy::needless_lifetimes)]
+
+/* Simple functions */
+
+pub fn choose<'a, T>(b: bool, x: &'a mut T, y: &'a mut T) -> &'a mut T {
+    if b {
+        x
+    } else {
+        y
+    }
+}
+
+pub fn mul2_add1(x: u32) -> u32 {
+    (x + x) + 1
+}
+
+pub fn use_mul2_add1(x: u32, y: u32) -> u32 {
+    mul2_add1(x) + y
+}
+
+pub fn incr<'a>(x: &'a mut u32) {
+    *x += 1;
+}
+
+pub fn use_incr() {
+    let mut x = 0;
+    incr(&mut x);
+    incr(&mut x);
+    incr(&mut x);
+}
+
+/* Recursion, loops */
+
+pub enum CList<T> {
+    CCons(T, Box<CList<T>>),
+    CNil,
+}
+
+pub fn list_nth<'a, T>(l: &'a CList<T>, i: u32) -> &'a T {
+    match l {
+        CList::CCons(x, tl) => {
+            if i == 0 {
+                x
+            } else {
+                list_nth(tl, i - 1)
+            }
+        }
+        CList::CNil => {
+            panic!()
+        }
+    }
+}
+
+pub fn list_nth_mut<'a, T>(l: &'a mut CList<T>, i: u32) -> &'a mut T {
+    match l {
+        CList::CCons(x, tl) => {
+            if i == 0 {
+                x
+            } else {
+                list_nth_mut(tl, i - 1)
+            }
+        }
+        CList::CNil => {
+            panic!()
+        }
+    }
+}
+
+pub fn list_nth_mut1<'a, T>(mut l: &'a mut CList<T>, mut i: u32) -> &'a mut T {
+    while let CList::CCons(x, tl) = l {
+        if i == 0 {
+            return x;
+        }
+        i -= 1;
+        l = tl;
+    }
+    panic!()
+}
+
+pub fn i32_id(i: i32) -> i32 {
+    if i == 0 {
+        0
+    } else {
+        i32_id(i - 1) + 1
+    }
+}
+
+pub fn list_tail<'a, T>(l: &'a mut CList<T>) -> &'a mut CList<T> {
+    match l {
+        CList::CCons(_, tl) => list_tail(tl),
+        CList::CNil => l,
+    }
+}
+
+/* Traits */
+
+pub trait Counter {
+    fn incr(&mut self) -> usize;
+}
+
+impl Counter for usize {
+    fn incr(&mut self) -> usize {
+        let x = *self;
+        *self += 1;
+        x
+    }
+}
+
+pub fn use_counter<'a, T: Counter>(cnt: &'a mut T) -> usize {
+    cnt.incr()
+}
diff --git a/tests/src/external.rs b/tests/src/external.rs
new file mode 100644
index 00000000..521749d6
--- /dev/null
+++ b/tests/src/external.rs
@@ -0,0 +1,11 @@
+//! This module uses external types and functions
+
+use std::cell::Cell;
+
+pub fn use_get(rc: &Cell<u32>) -> u32 {
+    rc.get()
+}
+
+pub fn incr(rc: &mut Cell<u32>) {
+    *rc.get_mut() += 1;
+}
diff --git a/tests/src/hashmap.rs b/tests/src/hashmap.rs
new file mode 100644
index 00000000..58d22acd
--- /dev/null
+++ b/tests/src/hashmap.rs
@@ -0,0 +1,352 @@
+//! A hashmap implementation.
+//!
+//! Current limitations:
+//! - all the recursive functions should be rewritten with loops, once
+//!   we have support for this.
+//! - we will need function pointers/closures if we want to make the map
+//!   generic in the key type (having function pointers allows to mimic traits)
+//! - for the "get" functions: we don't support borrows inside of enumerations
+//!   for now, so we can't return a type like `Option<&T>`. The real restriction
+//!   we currently have on borrows is that we forbid *nested* borrows in function
+//!   signatures, like in `&'a mut &'b mut T` (and the real problem comes from
+//!   nested *lifetimes*, not nested borrows). Getting the borrows inside of
+//!   enumerations mostly requires to pour some implementation time in it.
+
+use std::vec::Vec;
+pub type Key = usize; // TODO: make this generic
+pub type Hash = usize;
+
+pub enum List<T> {
+    Cons(Key, T, Box<List<T>>),
+    Nil,
+}
+
+/// A hash function for the keys.
+/// Rk.: we use shared references because we anticipate on the generic
+/// hash map version.
+pub fn hash_key(k: &Key) -> Hash {
+    // Do nothing for now, we might want to implement something smarter
+    // in the future, or to call an external function (which will be
+    // abstract): we don't need to reason about the hash function.
+    *k
+}
+
+/// A hash map from [u64] to values
+pub struct HashMap<T> {
+    /// The current number of entries in the table
+    num_entries: usize,
+    /// The max load factor, expressed as a fraction
+    max_load_factor: (usize, usize),
+    /// The max load factor applied to the current table length:
+    /// gives the threshold at which to resize the table.
+    max_load: usize,
+    /// The table itself
+    slots: Vec<List<T>>,
+}
+
+impl<T> HashMap<T> {
+    /// Allocate a vector of slots of a given size.
+    /// We would need a loop, but can't use loops for now...
+    fn allocate_slots(mut slots: Vec<List<T>>, mut n: usize) -> Vec<List<T>> {
+        while n > 0 {
+            slots.push(List::Nil);
+            n -= 1;
+        }
+        slots
+    }
+
+    /// Create a new table, with a given capacity
+    fn new_with_capacity(
+        capacity: usize,
+        max_load_dividend: usize,
+        max_load_divisor: usize,
+    ) -> Self {
+        // TODO: better to use `Vec::with_capacity(capacity)` instead
+        // of `Vec::new()`
+        let slots = HashMap::allocate_slots(Vec::new(), capacity);
+        HashMap {
+            num_entries: 0,
+            max_load_factor: (max_load_dividend, max_load_divisor),
+            max_load: (capacity * max_load_dividend) / max_load_divisor,
+            slots,
+        }
+    }
+
+    pub fn new() -> Self {
+        // For now we create a table with 32 slots and a max load factor of 4/5
+        HashMap::new_with_capacity(32, 4, 5)
+    }
+
+    pub fn clear(&mut self) {
+        self.num_entries = 0;
+        let slots = &mut self.slots;
+        let mut i = 0;
+        while i < slots.len() {
+            slots[i] = List::Nil;
+            i += 1;
+        }
+    }
+
+    pub fn len(&self) -> usize {
+        self.num_entries
+    }
+
+    /// Insert in a list.
+    /// Return `true` if we inserted an element, `false` if we simply updated
+    /// a value.
+    fn insert_in_list(key: Key, value: T, mut ls: &mut List<T>) -> bool {
+        loop {
+            match ls {
+                List::Nil => {
+                    *ls = List::Cons(key, value, Box::new(List::Nil));
+                    return true;
+                }
+                List::Cons(ckey, cvalue, tl) => {
+                    if *ckey == key {
+                        *cvalue = value;
+                        return false;
+                    } else {
+                        ls = tl;
+                    }
+                }
+            }
+        }
+    }
+
+    /// Auxiliary function to insert in the hashmap without triggering a resize
+    fn insert_no_resize(&mut self, key: Key, value: T) {
+        let hash = hash_key(&key);
+        let hash_mod = hash % self.slots.len();
+        // We may want to use slots[...] instead of get_mut...
+        let inserted = HashMap::insert_in_list(key, value, &mut self.slots[hash_mod]);
+        if inserted {
+            self.num_entries += 1;
+        }
+    }
+
+    /// Insertion function.
+    /// May trigger a resize of the hash table.
+    pub fn insert(&mut self, key: Key, value: T) {
+        // Insert
+        self.insert_no_resize(key, value);
+        // Resize if necessary
+        if self.len() > self.max_load {
+            self.try_resize()
+        }
+    }
+
+    /// The resize function, called if we need to resize the table after
+    /// an insertion.
+    fn try_resize(&mut self) {
+        // Check that we can resize: we need to check that there are no overflows.
+        // Note that we are conservative about the usize::MAX.
+        // Also note that `as usize` is a trait, but we apply it to a constant
+        // here, which gets compiled by the MIR interpreter (so we don't see
+        // the conversion, actually).
+        // Rk.: this is a hit heavy...
+        let max_usize = u32::MAX as usize;
+        let capacity = self.slots.len();
+        // Checking that there won't be overflows by using the fact that, if m > 0:
+        // n * m <= p <==> n <= p / m
+        let n1 = max_usize / 2;
+        if capacity <= n1 / self.max_load_factor.0 {
+            // Create a new table with a higher capacity
+            let mut ntable = HashMap::new_with_capacity(
+                capacity * 2,
+                self.max_load_factor.0,
+                self.max_load_factor.1,
+            );
+
+            // Move the elements to the new table
+            HashMap::move_elements(&mut ntable, &mut self.slots, 0);
+
+            // Replace the current table with the new table
+            self.slots = ntable.slots;
+            self.max_load = ntable.max_load;
+        }
+    }
+
+    /// Auxiliary function called by [try_resize] to move all the elements
+    /// from the table to a new table
+    fn move_elements<'a>(ntable: &'a mut HashMap<T>, slots: &'a mut Vec<List<T>>, mut i: usize) {
+        while i < slots.len() {
+            // Move the elements out of the slot i
+            let ls = std::mem::replace(&mut slots[i], List::Nil);
+            // Move all those elements to the new table
+            HashMap::move_elements_from_list(ntable, ls);
+            // Do the same for slot i+1
+            i += 1;
+        }
+    }
+
+    /// Auxiliary function.
+    fn move_elements_from_list(ntable: &mut HashMap<T>, mut ls: List<T>) {
+        // As long as there are elements in the list, move them
+        loop {
+            match ls {
+                List::Nil => return, // We're done
+                List::Cons(k, v, tl) => {
+                    // Insert the element in the new table
+                    ntable.insert_no_resize(k, v);
+                    // Move the elements out of the tail
+                    ls = *tl;
+                }
+            }
+        }
+    }
+
+    /// Returns `true` if the map contains a value for the specified key.
+    pub fn contains_key(&self, key: &Key) -> bool {
+        let hash = hash_key(key);
+        let hash_mod = hash % self.slots.len();
+        HashMap::contains_key_in_list(key, &self.slots[hash_mod])
+    }
+
+    /// Returns `true` if the list contains a value for the specified key.
+    pub fn contains_key_in_list(key: &Key, mut ls: &List<T>) -> bool {
+        loop {
+            match ls {
+                List::Nil => return false,
+                List::Cons(ckey, _, tl) => {
+                    if *ckey == *key {
+                        return true;
+                    } else {
+                        ls = tl;
+                    }
+                }
+            }
+        }
+    }
+
+    /// We don't support borrows inside of enumerations for now, so we
+    /// can't return an option...
+    /// TODO: add support for that
+    fn get_in_list<'a, 'k>(key: &'k Key, mut ls: &'a List<T>) -> &'a T {
+        loop {
+            match ls {
+                List::Nil => panic!(),
+                List::Cons(ckey, cvalue, tl) => {
+                    if *ckey == *key {
+                        return cvalue;
+                    } else {
+                        ls = tl;
+                    }
+                }
+            }
+        }
+    }
+
+    pub fn get<'a, 'k>(&'a self, key: &'k Key) -> &'a T {
+        let hash = hash_key(key);
+        let hash_mod = hash % self.slots.len();
+        HashMap::get_in_list(key, &self.slots[hash_mod])
+    }
+
+    pub fn get_mut_in_list<'a, 'k>(mut ls: &'a mut List<T>, key: &'k Key) -> &'a mut T {
+        while let List::Cons(ckey, cvalue, tl) = ls {
+            if *ckey == *key {
+                return cvalue;
+            } else {
+                ls = tl;
+            }
+        }
+        panic!()
+    }
+
+    /// Same remark as for [get].
+    pub fn get_mut<'a, 'k>(&'a mut self, key: &'k Key) -> &'a mut T {
+        let hash = hash_key(key);
+        let hash_mod = hash % self.slots.len();
+        HashMap::get_mut_in_list(&mut self.slots[hash_mod], key)
+    }
+
+    /// Remove an element from the list.
+    /// Return the removed element.
+    fn remove_from_list(key: &Key, mut ls: &mut List<T>) -> Option<T> {
+        loop {
+            match ls {
+                List::Nil => return None,
+                // We have to use a guard and split the Cons case into two
+                // branches, otherwise the borrow checker is not happy.
+                List::Cons(ckey, _, _) if *ckey == *key => {
+                    // We have to move under borrows, so we need to use
+                    // [std::mem::replace] in several steps.
+                    // Retrieve the tail
+                    let mv_ls = std::mem::replace(ls, List::Nil);
+                    match mv_ls {
+                        List::Nil => unreachable!(),
+                        List::Cons(_, cvalue, tl) => {
+                            // Make the list equal to its tail
+                            *ls = *tl;
+                            // Return the dropped value
+                            return Some(cvalue);
+                        }
+                    }
+                }
+                List::Cons(_, _, tl) => {
+                    ls = tl;
+                }
+            }
+        }
+    }
+
+    /// Same remark as for [get].
+    pub fn remove(&mut self, key: &Key) -> Option<T> {
+        let hash = hash_key(key);
+        let hash_mod = hash % self.slots.len();
+
+        let x = HashMap::remove_from_list(key, &mut self.slots[hash_mod]);
+        match x {
+            Option::None => Option::None,
+            Option::Some(x) => {
+                self.num_entries -= 1;
+                Option::Some(x)
+            }
+        }
+    }
+}
+
+/// I currently can't retrieve functions marked with the attribute #[test],
+/// while I want to extract the unit tests and use the normalize on them,
+/// so I have to define the test functions somewhere and call them from
+/// a test function.
+/// TODO: find a way to do that.
+#[allow(dead_code)]
+fn test1() {
+    let mut hm: HashMap<u64> = HashMap::new();
+    hm.insert(0, 42);
+    hm.insert(128, 18);
+    hm.insert(1024, 138);
+    hm.insert(1056, 256);
+    // Rk.: `&128` introduces a ref constant value
+    // TODO: add support for this
+    // Rk.: this only happens if we query the MIR too late (for instance,
+    // the optimized MIR). It is not a problem if we query, say, the
+    // "built" MIR.
+    let k = 128;
+    assert!(*hm.get(&k) == 18);
+    let k = 1024;
+    let x = hm.get_mut(&k);
+    *x = 56;
+    assert!(*hm.get(&k) == 56);
+    let x = hm.remove(&k);
+    // If we write `x == Option::Some(56)` rust introduces
+    // a call to `core::cmp::PartialEq::eq`, which is a trait
+    // I don't support for now.
+    // Also, I haven't implemented support for `unwrap` yet...
+    match x {
+        Option::None => panic!(),
+        Option::Some(x) => assert!(x == 56),
+    };
+    let k = 0;
+    assert!(*hm.get(&k) == 42);
+    let k = 128;
+    assert!(*hm.get(&k) == 18);
+    let k = 1056;
+    assert!(*hm.get(&k) == 256);
+}
+
+#[test]
+fn tests() {
+    test1();
+}
diff --git a/tests/src/hashmap_main.rs b/tests/src/hashmap_main.rs
new file mode 100644
index 00000000..45dfa6e2
--- /dev/null
+++ b/tests/src/hashmap_main.rs
@@ -0,0 +1,16 @@
+mod hashmap;
+mod hashmap_utils;
+
+use crate::hashmap::*;
+use crate::hashmap_utils::*;
+
+pub fn insert_on_disk(key: Key, value: u64) {
+    // Deserialize
+    let mut hm = deserialize();
+    // Update
+    hm.insert(key, value);
+    // Serialize
+    serialize(hm);
+}
+
+pub fn main() {}
diff --git a/tests/src/hashmap_utils.rs b/tests/src/hashmap_utils.rs
new file mode 100644
index 00000000..cd7b481f
--- /dev/null
+++ b/tests/src/hashmap_utils.rs
@@ -0,0 +1,12 @@
+use crate::hashmap::*;
+
+/// Serialize a hash map - we don't have traits, so we fix the type of the
+/// values (this is not the interesting part anyway)
+pub(crate) fn serialize(_hm: HashMap<u64>) {
+    unimplemented!();
+}
+/// Deserialize a hash map - we don't have traits, so we fix the type of the
+/// values (this is not the interesting part anyway)
+pub(crate) fn deserialize() -> HashMap<u64> {
+    unimplemented!();
+}
diff --git a/tests/src/loops.rs b/tests/src/loops.rs
new file mode 100644
index 00000000..2f71d75b
--- /dev/null
+++ b/tests/src/loops.rs
@@ -0,0 +1,366 @@
+use std::vec::Vec;
+
+/// No borrows
+pub fn sum(max: u32) -> u32 {
+    let mut i = 0;
+    let mut s = 0;
+    while i < max {
+        s += i;
+        i += 1;
+    }
+
+    s *= 2;
+    s
+}
+
+/// Same as [sum], but we use borrows in order tocreate loans inside a loop
+/// iteration, and those borrows will have to be ended by the end of the
+/// iteration.
+pub fn sum_with_mut_borrows(max: u32) -> u32 {
+    let mut i = 0;
+    let mut s = 0;
+    while i < max {
+        let ms = &mut s;
+        *ms += i;
+        let mi = &mut i;
+        *mi += 1;
+    }
+
+    s *= 2;
+    s
+}
+
+/// Similar to [sum_with_mut_borrows].
+pub fn sum_with_shared_borrows(max: u32) -> u32 {
+    let mut i = 0;
+    let mut s = 0;
+    while i < max {
+        i += 1;
+        // We changed the order compared to [sum_with_mut_borrows]:
+        // we want to have a shared borrow surviving until the end
+        // of the iteration.
+        let mi = &i;
+        s += *mi;
+    }
+
+    s *= 2;
+    s
+}
+
+pub fn sum_array<const N: usize>(a: [u32; N]) -> u32 {
+    let mut i = 0;
+    let mut s = 0;
+    while i < N {
+        s += a[i];
+        i += 1;
+    }
+    s
+}
+
+/// This case is interesting, because the fixed point for the loop doesn't
+/// introduce new abstractions.
+pub fn clear(v: &mut Vec<u32>) {
+    let mut i = 0;
+    while i < v.len() {
+        v[i] = 0;
+        i += 1;
+    }
+}
+
+pub enum List<T> {
+    Cons(T, Box<List<T>>),
+    Nil,
+}
+
+/// The parameter `x` is a borrow on purpose
+pub fn list_mem(x: &u32, mut ls: &List<u32>) -> bool {
+    while let List::Cons(y, tl) = ls {
+        if *y == *x {
+            return true;
+        } else {
+            ls = tl;
+        }
+    }
+    false
+}
+
+/// Same as [list_nth_mut] but with a loop
+pub fn list_nth_mut_loop<T>(mut ls: &mut List<T>, mut i: u32) -> &mut T {
+    while let List::Cons(x, tl) = ls {
+        if i == 0 {
+            return x;
+        } else {
+            ls = tl;
+            i -= 1;
+        }
+    }
+    panic!()
+}
+
+/// Same as [list_nth_mut_loop] but with shared borrows
+pub fn list_nth_shared_loop<T>(mut ls: &List<T>, mut i: u32) -> &T {
+    while let List::Cons(x, tl) = ls {
+        if i == 0 {
+            return x;
+        } else {
+            ls = tl;
+            i -= 1;
+        }
+    }
+    panic!()
+}
+
+pub fn get_elem_mut(slots: &mut Vec<List<usize>>, x: usize) -> &mut usize {
+    let mut ls = &mut slots[0];
+    loop {
+        match ls {
+            List::Nil => panic!(),
+            List::Cons(y, tl) => {
+                if *y == x {
+                    return y;
+                } else {
+                    ls = tl;
+                }
+            }
+        }
+    }
+}
+
+pub fn get_elem_shared(slots: &Vec<List<usize>>, x: usize) -> &usize {
+    let mut ls = &slots[0];
+    loop {
+        match ls {
+            List::Nil => panic!(),
+            List::Cons(y, tl) => {
+                if *y == x {
+                    return y;
+                } else {
+                    ls = tl;
+                }
+            }
+        }
+    }
+}
+
+pub fn id_mut<T>(ls: &mut List<T>) -> &mut List<T> {
+    ls
+}
+
+pub fn id_shared<T>(ls: &List<T>) -> &List<T> {
+    ls
+}
+
+/// Small variation of [list_nth_mut_loop]
+pub fn list_nth_mut_loop_with_id<T>(ls: &mut List<T>, mut i: u32) -> &mut T {
+    let mut ls = id_mut(ls);
+    while let List::Cons(x, tl) = ls {
+        if i == 0 {
+            return x;
+        } else {
+            ls = tl;
+            i -= 1;
+        }
+    }
+    panic!()
+}
+
+/// Small variation of [list_nth_shared_loop]
+pub fn list_nth_shared_loop_with_id<T>(ls: &List<T>, mut i: u32) -> &T {
+    let mut ls = id_shared(ls);
+    while let List::Cons(x, tl) = ls {
+        if i == 0 {
+            return x;
+        } else {
+            ls = tl;
+            i -= 1;
+        }
+    }
+    panic!()
+}
+
+/// Same as [list_nth_mut] but on a pair of lists.
+///
+/// This test checks that we manage to decompose a loop into disjoint regions.
+pub fn list_nth_mut_loop_pair<'a, 'b, T>(
+    mut ls0: &'a mut List<T>,
+    mut ls1: &'b mut List<T>,
+    mut i: u32,
+) -> (&'a mut T, &'b mut T) {
+    loop {
+        match (ls0, ls1) {
+            (List::Nil, _) | (_, List::Nil) => {
+                panic!()
+            }
+            (List::Cons(x0, tl0), List::Cons(x1, tl1)) => {
+                if i == 0 {
+                    return (x0, x1);
+                } else {
+                    ls0 = tl0;
+                    ls1 = tl1;
+                    i -= 1;
+                }
+            }
+        }
+    }
+}
+
+/// Same as [list_nth_mut_loop_pair] but with shared borrows.
+pub fn list_nth_shared_loop_pair<'a, 'b, T>(
+    mut ls0: &'a List<T>,
+    mut ls1: &'b List<T>,
+    mut i: u32,
+) -> (&'a T, &'b T) {
+    loop {
+        match (ls0, ls1) {
+            (List::Nil, _) | (_, List::Nil) => {
+                panic!()
+            }
+            (List::Cons(x0, tl0), List::Cons(x1, tl1)) => {
+                if i == 0 {
+                    return (x0, x1);
+                } else {
+                    ls0 = tl0;
+                    ls1 = tl1;
+                    i -= 1;
+                }
+            }
+        }
+    }
+}
+
+/// Same as [list_nth_mut_loop_pair] but this time we force the two loop
+/// regions to be merged.
+pub fn list_nth_mut_loop_pair_merge<'a, T>(
+    mut ls0: &'a mut List<T>,
+    mut ls1: &'a mut List<T>,
+    mut i: u32,
+) -> (&'a mut T, &'a mut T) {
+    while let (List::Cons(x0, tl0), List::Cons(x1, tl1)) = (ls0, ls1) {
+        if i == 0 {
+            return (x0, x1);
+        } else {
+            ls0 = tl0;
+            ls1 = tl1;
+            i -= 1;
+        }
+    }
+    panic!()
+}
+
+/// Same as [list_nth_mut_loop_pair_merge] but with shared borrows.
+pub fn list_nth_shared_loop_pair_merge<'a, T>(
+    mut ls0: &'a List<T>,
+    mut ls1: &'a List<T>,
+    mut i: u32,
+) -> (&'a T, &'a T) {
+    while let (List::Cons(x0, tl0), List::Cons(x1, tl1)) = (ls0, ls1) {
+        if i == 0 {
+            return (x0, x1);
+        } else {
+            ls0 = tl0;
+            ls1 = tl1;
+            i -= 1;
+        }
+    }
+    panic!()
+}
+
+/// Mixing mutable and shared borrows.
+pub fn list_nth_mut_shared_loop_pair<'a, 'b, T>(
+    mut ls0: &'a mut List<T>,
+    mut ls1: &'b List<T>,
+    mut i: u32,
+) -> (&'a mut T, &'b T) {
+    while let (List::Cons(x0, tl0), List::Cons(x1, tl1)) = (ls0, ls1) {
+        if i == 0 {
+            return (x0, x1);
+        } else {
+            ls0 = tl0;
+            ls1 = tl1;
+            i -= 1;
+        }
+    }
+    panic!()
+}
+
+/// Same as [list_nth_mut_shared_loop_pair] but this time we force the two loop
+/// regions to be merged.
+pub fn list_nth_mut_shared_loop_pair_merge<'a, T>(
+    mut ls0: &'a mut List<T>,
+    mut ls1: &'a List<T>,
+    mut i: u32,
+) -> (&'a mut T, &'a T) {
+    while let (List::Cons(x0, tl0), List::Cons(x1, tl1)) = (ls0, ls1) {
+        if i == 0 {
+            return (x0, x1);
+        } else {
+            ls0 = tl0;
+            ls1 = tl1;
+            i -= 1;
+        }
+    }
+    panic!()
+}
+
+/// Same as [list_nth_mut_shared_loop_pair], but we switched the positions of
+/// the mutable and shared borrows.
+pub fn list_nth_shared_mut_loop_pair<'a, 'b, T>(
+    mut ls0: &'a List<T>,
+    mut ls1: &'b mut List<T>,
+    mut i: u32,
+) -> (&'a T, &'b mut T) {
+    while let (List::Cons(x0, tl0), List::Cons(x1, tl1)) = (ls0, ls1) {
+        if i == 0 {
+            return (x0, x1);
+        } else {
+            ls0 = tl0;
+            ls1 = tl1;
+            i -= 1;
+        }
+    }
+    panic!()
+}
+
+/// Same as [list_nth_mut_shared_loop_pair_merge], but we switch the positions of
+/// the mutable and shared borrows.
+pub fn list_nth_shared_mut_loop_pair_merge<'a, T>(
+    mut ls0: &'a List<T>,
+    mut ls1: &'a mut List<T>,
+    mut i: u32,
+) -> (&'a T, &'a mut T) {
+    while let (List::Cons(x0, tl0), List::Cons(x1, tl1)) = (ls0, ls1) {
+        if i == 0 {
+            return (x0, x1);
+        } else {
+            ls0 = tl0;
+            ls1 = tl1;
+            i -= 1;
+        }
+    }
+    panic!()
+}
+
+// We do not use the input borrow inside the loop
+#[allow(clippy::empty_loop)]
+pub fn ignore_input_mut_borrow(_a: &mut u32, mut i: u32) {
+    while i > 0 {
+        i -= 1;
+    }
+}
+
+// We do not use the input borrow inside the loop
+#[allow(clippy::empty_loop)]
+pub fn incr_ignore_input_mut_borrow(a: &mut u32, mut i: u32) {
+    *a += 1;
+    while i > 0 {
+        i -= 1;
+    }
+}
+
+// We do not use the input borrow inside the loop
+#[allow(clippy::empty_loop)]
+pub fn ignore_input_shared_borrow(_a: &mut u32, mut i: u32) {
+    while i > 0 {
+        i -= 1;
+    }
+}
diff --git a/tests/src/nested_borrows.rs b/tests/src/nested_borrows.rs
new file mode 100644
index 00000000..94db0cec
--- /dev/null
+++ b/tests/src/nested_borrows.rs
@@ -0,0 +1,181 @@
+//! This module contains functions with nested borrows in their signatures.
+
+pub fn id_mut_mut<'a, 'b, T>(x: &'a mut &'b mut T) -> &'a mut &'b mut T {
+    x
+}
+
+pub fn id_mut_pair<'a, T>(x: &'a mut (&'a mut T, u32)) -> &'a mut (&'a mut T, u32) {
+    x
+}
+
+pub fn id_mut_pair_test1() {
+    let mut x: u32 = 0;
+    let px = &mut x;
+    let mut p = (px, 1);
+    let pp0 = &mut p;
+    let pp1 = id_mut_pair(pp0);
+    let mut y = 2;
+    *pp1 = (&mut y, 3);
+}
+
+pub fn id_mut_mut_pair<'a, T>(
+    x: &'a mut &'a mut (&'a mut T, u32),
+) -> &'a mut &'a mut (&'a mut T, u32) {
+    x
+}
+
+pub fn id_mut_mut_mut_same<'a, T>(x: &'a mut &'a mut &'a mut u32) -> &'a mut &'a mut &'a mut u32 {
+    x
+}
+
+pub fn id_borrow1<'a, 'b, 'c>(_x: &'a mut &'b u32, _y: &'a &'a mut u32) {
+    ()
+}
+
+/// For symbolic execution: testing what happens with several abstractions.
+pub fn id_mut_mut_test1() {
+    let mut x = 0;
+    let mut px = &mut x;
+    let ppx = &mut px;
+    let ppy = id_mut_mut(ppx);
+    **ppy = 1;
+    // Ending one abstraction
+    assert!(*px == 1);
+    // Ending the other abstraction
+    assert!(x == 1);
+}
+
+/*
+/// For symbolic execution: testing what happens with several abstractions.
+/// This case is a bit trickier, because we modify the borrow graph through
+/// a value returned by a function call.
+/// TODO: not supported! We overwrite a borrow in a returned value.
+pub fn id_mut_mut_test2() {
+    let mut x = 0;
+    let mut px = &mut x;
+    let ppx = &mut px;
+    let ppy = id_mut_mut(ppx);
+    **ppy = 1;
+    // This time, we replace one of the borrows
+    let mut y = 2;
+    let py = &mut y;
+    *ppy = py;
+    // Ending one abstraction
+    assert!(*px == 2);
+    *px = 3;
+    // Ending the other abstraction
+    assert!(x == 1);
+    assert!(y == 3);
+}
+*/
+
+/*
+/// For symbolic execution: testing what happens with several abstractions.
+/// See what happens when chaining function calls.
+/// TODO: not supported! We overwrite a borrow in a returned value.
+pub fn id_mut_mut_test3() {
+    let mut x = 0;
+    let mut px = &mut x;
+    let ppx = &mut px;
+    let ppy = id_mut_mut(ppx); // &'a mut &'b mut i32
+    **ppy = 1;
+    let ppz = id_mut_mut(ppy); // &'c mut &'b mut i32
+    **ppz = 2;
+    // End 'a and 'c
+    assert!(*px == 2);
+    // End 'b (2 abstractions at once)
+    assert!(x == 2);
+}*/
+
+/*
+/// For symbolic execution: testing what happens with several abstractions.
+/// See what happens when chaining function calls.
+/// This one is slightly more complex than the previous one.
+pub fn id_mut_mut_test4() {
+    let mut x = 0;
+    let mut px = &mut x;
+    let ppx = &mut px;
+    let ppy = id_mut_mut(ppx); // &'a mut &'b mut i32
+    **ppy = 1;
+    let ppz = id_mut_mut(ppy); // &'c mut &'b mut i32
+    **ppz = 2;
+    // End 'c
+    assert!(**ppy == 2);
+    // End 'a
+    assert!(*px == 2);
+    // End 'b (2 abstractions at once)
+    assert!(x == 2);
+}
+*/
+
+fn id<'a, T>(x: &'a mut T) -> &'a mut T {
+    x
+}
+
+/// Checking projectors over symbolic values
+pub fn test_borrows1() {
+    let mut x = 3;
+    let y = id(&mut x);
+    let z = id(y);
+    // We do not write a statement which would expand `z` on purpose:
+    // we want to test that the handling of non-expanded symbolic values
+    // is correct
+    assert!(x == 3);
+}
+
+fn id_pair<'a, 'b, T>(x: &'a mut T, y: &'b mut T) -> (&'a mut T, &'b mut T) {
+    (x, y)
+}
+
+/// Similar to the previous one
+pub fn test_borrows2() {
+    let mut x = 3;
+    let mut y = 4;
+    let z = id_pair(&mut x, &mut y);
+    // We do not write a statement which would expand `z` on purpose:
+    // we want to test that the handling of non-expanded symbolic values
+    // is correct
+    assert!(x == 3);
+    assert!(y == 4);
+}
+
+/// input type: 'b must last longer than 'a
+/// output type: 'a must last longer than 'b
+/// So: 'a = 'b, and the function is legal.
+pub fn nested_mut_borrows1<'a, 'b>(x: &'a mut &'b mut u32) -> &'b mut &'a mut u32 {
+    x
+}
+
+pub fn nested_shared_borrows1<'a, 'b>(x: &'a &'b u32) -> &'a &'b u32 {
+    x
+}
+
+pub fn nested_borrows1<'a, 'b>(x: &'a mut &'b u32) -> &'a mut &'b u32 {
+    x
+}
+
+pub fn nested_borrows2<'a, 'b>(x: &'a &'b mut u32) -> &'a &'b mut u32 {
+    x
+}
+
+fn nested_borrows1_test1() {
+    let x = 0;
+    let mut px = &x;
+    let ppx = &mut px;
+    let ppy = nested_borrows1(ppx);
+    assert!(**ppy == 0);
+    assert!(x == 0);
+}
+
+fn nested_borrows1_test2<'a, 'b>(x: &'a mut &'b u32) -> &'a mut &'b u32 {
+    nested_borrows1(x)
+}
+
+fn nested_borrows2_test1() {
+    let mut x = 0;
+    let px = &mut x;
+    let ppx = &px;
+    let ppy = nested_borrows2(ppx);
+    assert!(**ppy == 0);
+    assert!(x == 0);
+}
diff --git a/tests/src/no_nested_borrows.rs b/tests/src/no_nested_borrows.rs
new file mode 100644
index 00000000..9a7604e6
--- /dev/null
+++ b/tests/src/no_nested_borrows.rs
@@ -0,0 +1,491 @@
+//! This module doesn't contain **functions which use nested borrows in their
+//! signatures**, and doesn't contain functions with loops.
+
+pub struct Pair<T1, T2> {
+    pub x: T1,
+    pub y: T2,
+}
+
+pub enum List<T> {
+    Cons(T, Box<List<T>>),
+    Nil,
+}
+
+/// Sometimes, enumerations with one variant are not treated
+/// the same way as the other variants (for example, downcasts
+/// are not always introduced).
+/// A downcast is the cast of an enum to a specific variant, like
+/// in the left value of:
+/// `((_0 as Right).0: T2) = move _1;`
+pub enum One<T1> {
+    One(T1),
+}
+
+/// Truely degenerate case
+/// Instantiations of this are encoded as constant values by rust.
+pub enum EmptyEnum {
+    Empty,
+}
+
+/// Enumeration (several variants with no parameters)
+/// Those are not encoded as constant values.
+pub enum Enum {
+    Variant1,
+    Variant2,
+}
+
+/// Degenerate struct
+/// Instanciations of this are encoded as constant values by rust.
+pub struct EmptyStruct {}
+
+pub enum Sum<T1, T2> {
+    Left(T1),
+    Right(T2),
+}
+
+pub fn cast_u32_to_i32(x: u32) -> i32 {
+    x as i32
+}
+
+pub fn cast_bool_to_i32(x: bool) -> i32 {
+    x as i32
+}
+
+#[allow(clippy::unnecessary_cast)]
+pub fn cast_bool_to_bool(x: bool) -> bool {
+    x as bool
+}
+
+#[allow(unused_variables)]
+pub fn test2() {
+    let x: u32 = 23;
+    let y: u32 = 44;
+    let z = x + y;
+    let p: Pair<u32, u32> = Pair { x, y: z };
+    let s: Sum<u32, bool> = Sum::Right(true);
+    let o: One<u64> = One::One(3);
+    let e0 = EmptyEnum::Empty;
+    let e1 = e0;
+    let enum0 = Enum::Variant1;
+}
+
+pub fn get_max(x: u32, y: u32) -> u32 {
+    if x >= y {
+        x
+    } else {
+        y
+    }
+}
+
+pub fn test3() {
+    let x = get_max(4, 3);
+    let y = get_max(10, 11);
+    let z = x + y;
+    assert!(z == 15);
+}
+
+pub fn test_neg1() {
+    let x: i32 = 3;
+    let y = -x;
+    assert!(y == -3);
+}
+
+/// Testing nested references.
+pub fn refs_test1() {
+    let mut x = 0;
+    let mut px = &mut x;
+    let ppx = &mut px;
+    **ppx = 1;
+    // The interesting thing happening here is that the borrow of x is inside
+    // the borrow of px: ending the borrow of x requires ending the borrow of
+    // px first.
+    assert!(x == 1);
+}
+
+pub fn refs_test2() {
+    let mut x = 0;
+    let mut y = 1;
+    let mut px = &mut x;
+    let py = &mut y;
+    let ppx = &mut px;
+    *ppx = py;
+    **ppx = 2;
+    assert!(*px == 2);
+    assert!(x == 0);
+    assert!(*py == 2);
+    assert!(y == 2);
+}
+
+/// Box creation
+#[allow(unused_variables)]
+pub fn test_list1() {
+    let l: List<i32> = List::Cons(0, Box::new(List::Nil));
+}
+
+/// Box deref
+pub fn test_box1() {
+    use std::ops::Deref;
+    use std::ops::DerefMut;
+    let mut b: Box<i32> = Box::new(0);
+    let x = b.deref_mut();
+    *x = 1;
+    let x = b.deref();
+    assert!(*x == 1);
+}
+
+pub fn copy_int(x: i32) -> i32 {
+    x
+}
+
+/// Just checking the parameters given to unreachable
+/// Rk.: the input parameter prevents using the function as a unit test.
+pub fn test_unreachable(b: bool) {
+    if b {
+        unreachable!();
+    }
+}
+
+/// Just checking the parameters given to panic
+/// Rk.: the input parameter prevents using the function as a unit test.
+pub fn test_panic(b: bool) {
+    if b {
+        panic!("Panicked!");
+    }
+}
+
+// Just testing that shared loans are correctly handled
+pub fn test_copy_int() {
+    let x = 0;
+    let px = &x;
+    let y = copy_int(x);
+    assert!(*px == y);
+}
+
+pub fn is_cons<T>(l: &List<T>) -> bool {
+    match l {
+        List::Cons(_, _) => true,
+        List::Nil => false,
+    }
+}
+
+pub fn test_is_cons() {
+    let l: List<i32> = List::Cons(0, Box::new(List::Nil));
+
+    assert!(is_cons(&l));
+}
+
+pub fn split_list<T>(l: List<T>) -> (T, List<T>) {
+    match l {
+        List::Cons(hd, tl) => (hd, *tl),
+        _ => panic!(),
+    }
+}
+
+#[allow(unused_variables)]
+pub fn test_split_list() {
+    let l: List<i32> = List::Cons(0, Box::new(List::Nil));
+
+    let (hd, tl) = split_list(l);
+    assert!(hd == 0);
+}
+
+pub fn choose<'a, T>(b: bool, x: &'a mut T, y: &'a mut T) -> &'a mut T {
+    if b {
+        x
+    } else {
+        y
+    }
+}
+
+pub fn choose_test() {
+    let mut x = 0;
+    let mut y = 0;
+    let z = choose(true, &mut x, &mut y);
+    *z += 1;
+    assert!(*z == 1);
+    // drop(z)
+    assert!(x == 1);
+    assert!(y == 0);
+}
+
+/// Test with a char literal - testing serialization
+pub fn test_char() -> char {
+    'a'
+}
+
+/// Mutually recursive types
+pub enum Tree<T> {
+    Leaf(T),
+    Node(T, NodeElem<T>, Box<Tree<T>>),
+}
+
+pub enum NodeElem<T> {
+    Cons(Box<Tree<T>>, Box<NodeElem<T>>),
+    Nil,
+}
+
+/*
+// TODO: those definitions requires semantic termination (breaks the Coq backend
+// because we don't use fuel in this case).
+
+/// Mutually recursive functions
+pub fn even(x: u32) -> bool {
+    if x == 0 {
+        true
+    } else {
+        odd(x - 1)
+    }
+}
+
+pub fn odd(x: u32) -> bool {
+    if x == 0 {
+        false
+    } else {
+        even(x - 1)
+    }
+}
+
+pub fn test_even_odd() {
+    assert!(even(0));
+    assert!(even(4));
+    assert!(odd(1));
+    assert!(odd(5));
+}
+*/
+
+#[allow(clippy::needless_lifetimes)]
+pub fn list_length<'a, T>(l: &'a List<T>) -> u32 {
+    match l {
+        List::Nil => 0,
+        List::Cons(_, l1) => 1 + list_length(l1),
+    }
+}
+
+#[allow(clippy::needless_lifetimes)]
+pub fn list_nth_shared<'a, T>(l: &'a List<T>, i: u32) -> &'a T {
+    match l {
+        List::Nil => {
+            panic!()
+        }
+        List::Cons(x, tl) => {
+            if i == 0 {
+                x
+            } else {
+                list_nth_shared(tl, i - 1)
+            }
+        }
+    }
+}
+
+#[allow(clippy::needless_lifetimes)]
+pub fn list_nth_mut<'a, T>(l: &'a mut List<T>, i: u32) -> &'a mut T {
+    match l {
+        List::Nil => {
+            panic!()
+        }
+        List::Cons(x, tl) => {
+            if i == 0 {
+                x
+            } else {
+                list_nth_mut(tl, i - 1)
+            }
+        }
+    }
+}
+
+/// In-place list reversal - auxiliary function
+pub fn list_rev_aux<T>(li: List<T>, mut lo: List<T>) -> List<T> {
+    match li {
+        List::Nil => lo,
+        List::Cons(hd, mut tl) => {
+            let next = *tl;
+            *tl = lo;
+            lo = List::Cons(hd, tl);
+            list_rev_aux(next, lo)
+        }
+    }
+}
+
+/// In-place list reversal
+#[allow(clippy::needless_lifetimes)]
+pub fn list_rev<'a, T>(l: &'a mut List<T>) {
+    let li = std::mem::replace(l, List::Nil);
+    *l = list_rev_aux(li, List::Nil);
+}
+
+pub fn test_list_functions() {
+    let mut ls = List::Cons(
+        0,
+        Box::new(List::Cons(1, Box::new(List::Cons(2, Box::new(List::Nil))))),
+    );
+    assert!(list_length(&ls) == 3);
+    assert!(*list_nth_shared(&ls, 0) == 0);
+    assert!(*list_nth_shared(&ls, 1) == 1);
+    assert!(*list_nth_shared(&ls, 2) == 2);
+    let x = list_nth_mut(&mut ls, 1);
+    *x = 3;
+    assert!(*list_nth_shared(&ls, 0) == 0);
+    assert!(*list_nth_shared(&ls, 1) == 3); // Updated
+    assert!(*list_nth_shared(&ls, 2) == 2);
+}
+
+pub fn id_mut_pair1<'a, T1, T2>(x: &'a mut T1, y: &'a mut T2) -> (&'a mut T1, &'a mut T2) {
+    (x, y)
+}
+
+pub fn id_mut_pair2<'a, T1, T2>(p: (&'a mut T1, &'a mut T2)) -> (&'a mut T1, &'a mut T2) {
+    p
+}
+
+pub fn id_mut_pair3<'a, 'b, T1, T2>(x: &'a mut T1, y: &'b mut T2) -> (&'a mut T1, &'b mut T2) {
+    (x, y)
+}
+
+pub fn id_mut_pair4<'a, 'b, T1, T2>(p: (&'a mut T1, &'b mut T2)) -> (&'a mut T1, &'b mut T2) {
+    p
+}
+
+/// Testing constants (some constants are hard to retrieve from MIR, because
+/// they are compiled to very low values).
+/// We resort to the following structure to make rustc generate constants...
+pub struct StructWithTuple<T1, T2> {
+    p: (T1, T2),
+}
+
+pub fn new_tuple1() -> StructWithTuple<u32, u32> {
+    StructWithTuple { p: (1, 2) }
+}
+
+pub fn new_tuple2() -> StructWithTuple<i16, i16> {
+    StructWithTuple { p: (1, 2) }
+}
+
+pub fn new_tuple3() -> StructWithTuple<u64, i64> {
+    StructWithTuple { p: (1, 2) }
+}
+
+/// Similar to [StructWithTuple]
+pub struct StructWithPair<T1, T2> {
+    p: Pair<T1, T2>,
+}
+
+pub fn new_pair1() -> StructWithPair<u32, u32> {
+    // This actually doesn't make rustc generate a constant...
+    // I guess it only happens for tuples.
+    StructWithPair {
+        p: Pair { x: 1, y: 2 },
+    }
+}
+
+pub fn test_constants() {
+    assert!(new_tuple1().p.0 == 1);
+    assert!(new_tuple2().p.0 == 1);
+    assert!(new_tuple3().p.0 == 1);
+    assert!(new_pair1().p.x == 1);
+}
+
+/// This assignment is trickier than it seems
+#[allow(unused_assignments)]
+pub fn test_weird_borrows1() {
+    let mut x = 0;
+    let mut px = &mut x;
+    // Context:
+    // x -> [l0]
+    // px -> &mut l0 (0:i32)
+
+    px = &mut (*px);
+}
+
+pub fn test_mem_replace(px: &mut u32) {
+    let y = std::mem::replace(px, 1);
+    assert!(y == 0);
+    *px = 2;
+}
+
+/// Check that matching on borrowed values works well.
+pub fn test_shared_borrow_bool1(b: bool) -> u32 {
+    // Create a shared borrow of b
+    let _pb = &b;
+    // Match on b
+    if b {
+        0
+    } else {
+        1
+    }
+}
+
+/// Check that matching on borrowed values works well.
+/// Testing the concrete execution here.
+pub fn test_shared_borrow_bool2() -> u32 {
+    let b = true;
+    // Create a shared borrow of b
+    let _pb = &b;
+    // Match on b
+    if b {
+        0
+    } else {
+        1
+    }
+}
+
+/// Check that matching on borrowed values works well.
+/// In case of enumerations, we need to strip the outer loans before evaluating
+/// the discriminant.
+pub fn test_shared_borrow_enum1(l: List<u32>) -> u32 {
+    // Create a shared borrow of l
+    let _pl = &l;
+    // Match on l - must ignore the shared loan
+    match l {
+        List::Nil => 0,
+        List::Cons(_, _) => 1,
+    }
+}
+
+/// Check that matching on borrowed values works well.
+/// Testing the concrete execution here.
+pub fn test_shared_borrow_enum2() -> u32 {
+    let l: List<u32> = List::Nil;
+    // Create a shared borrow of l
+    let _pl = &l;
+    // Match on l - must ignore the shared loan
+    match l {
+        List::Nil => 0,
+        List::Cons(_, _) => 1,
+    }
+}
+
+pub fn incr(x: &mut u32) {
+    *x += 1;
+}
+
+pub fn call_incr(mut x: u32) -> u32 {
+    incr(&mut x);
+    x
+}
+
+pub fn read_then_incr(x: &mut u32) -> u32 {
+    let r = *x;
+    *x += 1;
+    r
+}
+
+pub struct Tuple<T1, T2>(T1, T2);
+
+pub fn use_tuple_struct(x: &mut Tuple<u32, u32>) {
+    x.0 = 1;
+}
+
+pub fn create_tuple_struct(x: u32, y: u64) -> Tuple<u32, u64> {
+    Tuple(x, y)
+}
+
+/// Structure with one field
+pub struct IdType<T>(T);
+
+pub fn use_id_type<T>(x: IdType<T>) -> T {
+    x.0
+}
+
+pub fn create_id_type<T>(x: T) -> IdType<T> {
+    IdType(x)
+}
diff --git a/tests/src/paper.rs b/tests/src/paper.rs
new file mode 100644
index 00000000..156f13ab
--- /dev/null
+++ b/tests/src/paper.rs
@@ -0,0 +1,82 @@
+//! The examples from the ICFP submission, all in one place.
+
+// 2.1
+pub fn ref_incr(x: &mut i32) {
+    *x = *x + 1;
+}
+
+pub fn test_incr() {
+    let mut x = 0i32;
+    ref_incr(&mut x);
+    assert!(x == 1);
+}
+
+// 2.2
+pub fn choose<'a, T>(b: bool, x: &'a mut T, y: &'a mut T) -> &'a mut T {
+    if b {
+        return x;
+    } else {
+        return y;
+    }
+}
+
+pub fn test_choose() {
+    let mut x = 0;
+    let mut y = 0;
+    let z = choose(true, &mut x, &mut y);
+    *z = *z + 1;
+    assert!(*z == 1);
+    assert!(x == 1);
+    assert!(y == 0);
+}
+
+// 2.3
+
+pub enum List<T> {
+    Cons(T, Box<List<T>>),
+    Nil,
+}
+use List::Cons;
+use List::Nil;
+
+pub fn list_nth_mut<'a, T>(l: &'a mut List<T>, i: u32) -> &'a mut T {
+    match l {
+        Nil => {
+            panic!()
+        }
+        Cons(x, tl) => {
+            if i == 0 {
+                return x;
+            } else {
+                return list_nth_mut(tl, i - 1);
+            }
+        }
+    }
+}
+
+pub fn sum(l: &List<i32>) -> i32 {
+    match l {
+        Nil => {
+            return 0;
+        }
+        Cons(x, tl) => {
+            return *x + sum(tl);
+        }
+    }
+}
+
+pub fn test_nth() {
+    let mut l = Cons(1, Box::new(Cons(2, Box::new(Cons(3, Box::new(Nil))))));
+    let x = list_nth_mut(&mut l, 2);
+    *x = *x + 1;
+    assert!(sum(&l) == 7);
+}
+
+// 4.3
+pub fn call_choose(mut p: (u32, u32)) -> u32 {
+    let px = &mut p.0;
+    let py = &mut p.1;
+    let pz = choose(true, px, py);
+    *pz = *pz + 1;
+    return p.0;
+}
diff --git a/tests/src/polonius_list.rs b/tests/src/polonius_list.rs
new file mode 100644
index 00000000..8c64110d
--- /dev/null
+++ b/tests/src/polonius_list.rs
@@ -0,0 +1,27 @@
+#![allow(dead_code)]
+
+pub enum List<T> {
+    Cons(T, Box<List<T>>),
+    Nil,
+}
+
+/// An example which comes from the b-epsilon tree.
+///
+/// Returns a mutable borrow to the first portion of the list where we
+/// can find [x]. This allows to do in-place modifications (insertion, filtering)
+/// in a natural manner (this piece of code was inspired by the C++ BeTree).
+pub fn get_list_at_x<'a>(ls: &'a mut List<u32>, x: u32) -> &'a mut List<u32> {
+    match ls {
+        List::Nil => {
+            // We reached the end: just return it
+            ls
+        }
+        List::Cons(hd, tl) => {
+            if *hd == x {
+                ls // Doing this requires NLL
+            } else {
+                get_list_at_x(tl, x)
+            }
+        }
+    }
+}
diff --git a/tests/src/traits.rs b/tests/src/traits.rs
new file mode 100644
index 00000000..27c90586
--- /dev/null
+++ b/tests/src/traits.rs
@@ -0,0 +1,341 @@
+pub trait BoolTrait {
+    // Required method
+    fn get_bool(&self) -> bool;
+
+    // Provided method
+    fn ret_true(&self) -> bool {
+        true
+    }
+}
+
+impl BoolTrait for bool {
+    fn get_bool(&self) -> bool {
+        *self
+    }
+}
+
+pub fn test_bool_trait_bool(x: bool) -> bool {
+    x.get_bool() && x.ret_true()
+}
+
+#[allow(clippy::redundant_pattern_matching)]
+impl<T> BoolTrait for Option<T> {
+    fn get_bool(&self) -> bool {
+        match self {
+            Option::Some(_) => true,
+            Option::None => false,
+        }
+    }
+}
+
+pub fn test_bool_trait_option<T>(x: Option<T>) -> bool {
+    x.get_bool() && x.ret_true()
+}
+
+pub fn test_bool_trait<T: BoolTrait>(x: T) -> bool {
+    x.get_bool()
+}
+
+pub trait ToU64 {
+    fn to_u64(self) -> u64;
+}
+
+impl ToU64 for u64 {
+    fn to_u64(self) -> u64 {
+        self
+    }
+}
+
+impl<A: ToU64> ToU64 for (A, A) {
+    fn to_u64(self) -> u64 {
+        self.0.to_u64() + self.1.to_u64()
+    }
+}
+
+pub fn f<T: ToU64>(x: (T, T)) -> u64 {
+    x.to_u64()
+}
+
+pub fn g<T>(x: (T, T)) -> u64
+where
+    (T, T): ToU64,
+{
+    x.to_u64()
+}
+
+pub fn h0(x: u64) -> u64 {
+    x.to_u64()
+}
+
+pub struct Wrapper<T> {
+    x: T,
+}
+
+impl<T: ToU64> ToU64 for Wrapper<T> {
+    fn to_u64(self) -> u64 {
+        self.x.to_u64()
+    }
+}
+
+pub fn h1(x: Wrapper<u64>) -> u64 {
+    x.to_u64()
+}
+
+pub fn h2<T: ToU64>(x: Wrapper<T>) -> u64 {
+    x.to_u64()
+}
+
+pub trait ToType<T> {
+    fn to_type(self) -> T;
+}
+
+impl ToType<bool> for u64 {
+    fn to_type(self) -> bool {
+        self > 0
+    }
+}
+
+pub trait OfType {
+    fn of_type<T: ToType<Self>>(x: T) -> Self
+    where
+        Self: std::marker::Sized;
+}
+
+pub fn h3<T1: OfType, T2: ToType<T1>>(y: T2) -> T1 {
+    T1::of_type(y)
+}
+
+// Checking what happens if we move trait clauses from a method to its enclosing block
+pub trait OfTypeBis<T: ToType<Self>>
+where
+    Self: std::marker::Sized,
+{
+    fn of_type(x: T) -> Self
+    where
+        Self: std::marker::Sized;
+}
+
+pub fn h4<T1: OfTypeBis<T2>, T2: ToType<T1>>(y: T2) -> T1 {
+    T1::of_type(y)
+}
+
+pub struct TestType<T>(T);
+
+// Checking what happens with nested blocks
+impl<T: ToU64> TestType<T> {
+    pub fn test(&self, x: T) -> bool {
+        struct TestType1(u64);
+        trait TestTrait {
+            fn test(&self) -> bool;
+        }
+
+        // Remark: we can't write: impl TestTrait for TestType<T>,
+        // we have to use a *local* parameter (can't use the outer T).
+        // In other words: the parameters used in the items inside
+        // an impl must be bound by the impl block (can't come from outer
+        // blocks).
+
+        impl TestTrait for TestType1 {
+            fn test(&self) -> bool {
+                self.0 > 1
+            }
+        }
+
+        let x = x.to_u64();
+        let y = TestType1(0);
+        x > 0 && y.test()
+    }
+}
+
+pub struct BoolWrapper(pub bool);
+
+impl<T> ToType<T> for BoolWrapper
+where
+    bool: ToType<T>,
+{
+    fn to_type(self) -> T {
+        self.0.to_type()
+    }
+}
+
+pub trait WithConstTy<const LEN: usize> {
+    const LEN1: usize;
+    // Testing default values
+    const LEN2: usize = 32;
+
+    type V;
+    type W: ToU64;
+
+    // Below: we can't use [Self::Len1] in the type of the array.
+    // Probably because of dyn traits...
+    fn f(x: &mut Self::W, y: &[u8; LEN]);
+}
+
+impl WithConstTy<32> for bool {
+    const LEN1: usize = 12;
+
+    type V = u8;
+    type W = u64;
+
+    fn f(_: &mut Self::W, _: &[u8; 32]) {}
+}
+
+pub fn use_with_const_ty1<const LEN: usize, H: WithConstTy<LEN>>() -> usize {
+    H::LEN1
+}
+
+pub fn use_with_const_ty2<const LEN: usize, H: WithConstTy<LEN>>(_: H::W) {}
+
+pub fn use_with_const_ty3<const LEN: usize, H: WithConstTy<LEN>>(x: H::W) -> u64 {
+    x.to_u64()
+}
+
+pub fn test_where1<'a, T: 'a>(_x: &'a T) {}
+pub fn test_where2<T: WithConstTy<32, V = u32>>(_x: T::V) {}
+
+// Below: testing super traits.
+//
+// Actually, this comes for free: ChildTrait : ParentTrait just adds a trait
+// clause for Self: `Self : ParentTrait`.
+pub trait ParentTrait0 {
+    type W;
+    fn get_name(&self) -> String;
+    fn get_w(&self) -> Self::W;
+}
+pub trait ParentTrait1 {}
+pub trait ChildTrait: ParentTrait0 + ParentTrait1 {}
+
+// But we still need to correctly reference the traits
+pub fn test_child_trait1<T: ChildTrait>(x: &T) -> String {
+    x.get_name()
+}
+
+pub fn test_child_trait2<T: ChildTrait>(x: &T) -> T::W {
+    x.get_w()
+}
+
+// Checking if the order has an importance (we use U::W before we declare that
+// U:ParentTrait0)
+pub fn order1<T: ParentTrait0<W = U::W>, U: ParentTrait0>() {}
+
+/* */
+pub trait ChildTrait1: ParentTrait1 {}
+
+impl ParentTrait1 for usize {}
+impl ChildTrait1 for usize {}
+
+/* [IntoIterator] is interesting because of the condition [Item = Self::Item]
+for the [IntoIter] associated type. */
+pub trait Iterator {
+    type Item;
+}
+
+pub trait IntoIterator {
+    type Item;
+    type IntoIter: Iterator<Item = Self::Item>;
+
+    // Required method
+    fn into_iter(self) -> Self::IntoIter;
+}
+
+/* The traits below are inspired by [Try] and [FromResidual].
+
+   The reference to `Self as Try` in the `FromResidual` clause used to
+   cause a bug.
+*/
+trait Try: FromResidual<<Self as Try>::Residual> {
+    type Residual;
+}
+
+trait FromResidual<T> {}
+
+pub trait WithTarget {
+    type Target;
+}
+
+pub trait ParentTrait2 {
+    type U: WithTarget;
+}
+
+pub trait ChildTrait2: ParentTrait2 {
+    fn convert(x: Self::U) -> <Self::U as WithTarget>::Target;
+}
+
+impl WithTarget for u32 {
+    type Target = u32;
+}
+
+impl ParentTrait2 for u32 {
+    type U = u32;
+}
+
+impl ChildTrait2 for u32 {
+    fn convert(x: u32) -> u32 {
+        x
+    }
+}
+
+/*
+// This one requires a lot of traits
+pub fn test_enumerate(x: usize) {
+    for _ in 0..x {}
+}
+*/
+
+/* Custom function pointers */
+pub trait CFnOnce<Args> {
+    type Output;
+
+    fn call_once(self, args: Args) -> Self::Output;
+}
+
+pub trait CFnMut<Args>: CFnOnce<Args> {
+    fn call_mut(&mut self, args: Args) -> Self::Output;
+}
+
+pub trait CFn<Args>: CFnMut<Args> {
+    fn call(&self, args: Args) -> Self::Output;
+}
+
+pub trait GetTrait {
+    type W;
+    fn get_w(&self) -> Self::W;
+}
+
+pub fn test_get_trait<T: GetTrait>(x: &T) -> T::W {
+    x.get_w()
+}
+
+// Constants with generics
+pub trait Trait {
+    const LEN: usize;
+}
+
+impl<const N: usize, T> Trait for [T; N] {
+    const LEN: usize = N;
+}
+
+impl<T: Trait> Trait for Wrapper<T> {
+    const LEN: usize = 0;
+}
+
+pub fn use_wrapper_len<T: Trait>() -> usize {
+    Wrapper::<T>::LEN
+}
+
+pub struct Foo<T, U> {
+    pub x: T,
+    pub y: U,
+}
+
+impl<T: Trait, U> Foo<T, U> {
+    pub const FOO: Result<T, i32> = Err(0);
+}
+
+pub fn use_foo1<T: Trait, U>() -> Result<T, i32> {
+    Foo::<T, U>::FOO
+}
+
+pub fn use_foo2<T, U: Trait>() -> Result<U, i32> {
+    Foo::<U, T>::FOO
+}
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index d3fe8836..8b4a4208 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -12,7 +12,7 @@ type test_case = {
 (* Run Aeneas on a specific input with the given options *)
 let run_test env case =
   let concat_path = List.fold_left Filename.concat "" in
-  let input_file = concat_path [ env.llbc_dir; "llbc"; case.name ] ^ ".llbc" in
+  let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in
   let dest_dir = concat_path [ "tests"; case.backend; case.subdir ] in
   let args =
     [|