Move tests from prusti-tests back to prusti

viperproject · Jul 19, 2019 · 3fda824 · 3fda824
1 parent e11e7aa
commit 3fda824
Show file tree

Hide file tree

Showing 431 changed files with 48 additions and 83 deletions.
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
@@ -30,5 +30,5 @@ test:
     - cargo --version
     - cargo build --all
     - cargo test --all --verbose -- --nocapture
-    - ./target/debug/prusti-rustc prusti-tests/tests/verify/pass/no-annotations/assert-true.rs
-    - ./target/debug/prusti-rustc prusti-tests/tests/verify/fail/no-annotations/assert-false.rs || if [ $? -eq 0 ]; then false; fi
+    - ./target/debug/prusti-rustc prusti/tests/verify/pass/no-annotations/assert-true.rs
+    - ./target/debug/prusti-rustc prusti/tests/verify/fail/no-annotations/assert-false.rs || if [ $? -eq 0 ]; then false; fi
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/Cargo.toml b/Cargo.toml
@@ -9,8 +9,6 @@ members = [
 	"jni-gen/systest",
 	"prusti-interface",
 	"prusti-filter",
-	"prusti-tools",
-	"prusti-tests",
 ]
 
 [profile.release]

diff --git a/LICENSE b/LICENSE
@@ -9,7 +9,7 @@ below or http://www.mozilla.org/MPL/2.0/), with the following
     (see http://creativecommons.org/publicdomain/zero/1.0/):
 
     jni-gen/systest
-    prusti-tests/tests
+    prusti/tests
     viper/tests
     viper/benches
 	viper-sys/tests

diff --git a/Makefile b/Makefile
@@ -2,7 +2,7 @@ SHELL := /bin/bash
 RUST_LOG ?= prusti=info
 RUST_TEST_THREADS ?= 1
 JAVA_HOME ?= /usr/lib/jvm/default-java
-RUN_FILE ?= prusti-tests/tests/typecheck/pass/lint.rs
+RUN_FILE ?= prusti/tests/typecheck/pass/lint.rs
 RUN_FILE_FOLDER=$(shell dirname ${RUN_FILE})
 JAVA_LIBJVM_DIR=$(shell dirname "$(shell find "$(shell readlink -f ${JAVA_HOME})" -name "libjvm.so")")
 RUSTUP_TOOLCHAIN=$(shell cat rust-toolchain)
@@ -45,7 +45,7 @@ test: build
 
 test-examples: build
 	$(SET_ENV_VARS) \
-	cargo test -p prusti-tests
+	cargo test -p prusti
 
 build-profile:
 	$(SET_ENV_VARS) \

diff --git a/README.md b/README.md
@@ -9,7 +9,7 @@ Overflow checking can be enabled with a configuration flag, otherwise all intege
 In Prusti, the functional behaviour of a function can be specified by using preconditions, postconditions, and loop invariants.
 The tool checks them, reporting error messages when the code does not adhere to the provided specification.
 
-To see examples of programs annotated with specifications, look into the [`prusti-tests/tests/verify/pass/rosetta`](prusti-tests/tests/verify/pass/rosetta) and [`prusti-tests/tests/verify/pass-overflow/rosetta`](prusti-tests/tests/verify/pass-overflow/rosetta) folders.
+To see examples of programs annotated with specifications, look into the [`prusti/tests/verify/pass/rosetta`](prusti/tests/verify/pass/rosetta) and [`prusti/tests/verify/pass-overflow/rosetta`](prusti/tests/verify/pass-overflow/rosetta) folders.
 
 
 Build for local development

diff --git a/evaluation/benchmark/benchmark.py b/evaluation/benchmark/benchmark.py
@@ -30,24 +30,24 @@
 )
 
 MANUAL_EVALUATION="""
-prusti-tests/tests/verify/pass-overflow/rosetta/100_doors_generic.rs
-prusti-tests/tests/verify/pass-overflow/rosetta/Binary_search_shared.rs
-prusti-tests/tests/verify/pass-overflow/rosetta/Heapsort_generic.rs
-prusti-tests/tests/verify/pass-overflow/rosetta/Knights_tour_generic.rs
-prusti-tests/tests/verify/pass-overflow/rosetta/Knuth_shuffle.rs
-prusti-tests/tests/verify/pass-overflow/rosetta/Langtons_ant.rs
-prusti-tests/tests/verify/pass-overflow/rosetta/Selection_sort_generic.rs
-
-prusti-tests/tests/verify/pass/rosetta/Ackermann_function.rs
-prusti-tests/tests/verify/pass-overflow/rosetta/Binary_search_shared_monomorphised.rs
-prusti-tests/tests/verify/pass/rosetta/Fibonacci_sequence.rs
-prusti-tests/tests/verify/pass/rosetta/Knapsack_Problem.rs
-prusti-tests/tests/verify/pass/larger/first-final.rs
-prusti-tests/tests/verify/pass-overflow/rosetta/Selection_sort.rs
-prusti-tests/tests/verify/pass-overflow/rosetta/Towers_of_Hanoi_spec.rs
-
-prusti-tests/tests/verify/pass-overflow/nll-rfc/borrow_first.rs
-prusti-tests/tests/verify/fail/nll-rfc/message.rs
+prusti/tests/verify/pass-overflow/rosetta/100_doors_generic.rs
+prusti/tests/verify/pass-overflow/rosetta/Binary_search_shared.rs
+prusti/tests/verify/pass-overflow/rosetta/Heapsort_generic.rs
+prusti/tests/verify/pass-overflow/rosetta/Knights_tour_generic.rs
+prusti/tests/verify/pass-overflow/rosetta/Knuth_shuffle.rs
+prusti/tests/verify/pass-overflow/rosetta/Langtons_ant.rs
+prusti/tests/verify/pass-overflow/rosetta/Selection_sort_generic.rs
+
+prusti/tests/verify/pass/rosetta/Ackermann_function.rs
+prusti/tests/verify/pass-overflow/rosetta/Binary_search_shared_monomorphised.rs
+prusti/tests/verify/pass/rosetta/Fibonacci_sequence.rs
+prusti/tests/verify/pass/rosetta/Knapsack_Problem.rs
+prusti/tests/verify/pass/larger/first-final.rs
+prusti/tests/verify/pass-overflow/rosetta/Selection_sort.rs
+prusti/tests/verify/pass-overflow/rosetta/Towers_of_Hanoi_spec.rs
+
+prusti/tests/verify/pass-overflow/nll-rfc/borrow_first.rs
+prusti/tests/verify/fail/nll-rfc/message.rs
 """.strip().split()
 
 

diff --git a/evaluation/script/prepare-artefact-files.sh b/evaluation/script/prepare-artefact-files.sh
@@ -62,13 +62,13 @@ cp "$DIR/../crates/successful-fine-grained.csv" "$ARTEFACT_DIR/evaluation-2/succ
 
 cp -r "$DIR/../artifact/examples/"*.orig "$ARTEFACT_DIR/evaluation-3/originals"
 
-cat "$DIR/../benchmark/benchmark.py" | grep "prusti-tests/tests/verify" | grep -v "overflow" | while read file
+cat "$DIR/../benchmark/benchmark.py" | grep "prusti/tests/verify" | grep -v "overflow" | while read file
 do
     echo === $file ===
     cp -r "$DIR/../../$file" "$ARTEFACT_DIR/evaluation-3/without-overflow-checks/"
 done
 
-cat "$DIR/../benchmark/benchmark.py" | grep "prusti-tests/tests/verify" | grep "overflow" | while read file
+cat "$DIR/../benchmark/benchmark.py" | grep "prusti/tests/verify" | grep "overflow" | while read file
 do
     echo === $file ===
     cp -r "$DIR/../../$file" "$ARTEFACT_DIR/evaluation-3/with-overflow-checks/"

diff --git a/prusti-tests/Cargo.toml b/prusti-tests/Cargo.toml
diff --git a/prusti-tests/README.md b/prusti-tests/README.md
diff --git a/prusti-tools/Cargo.toml b/prusti-tools/Cargo.toml
diff --git a/prusti-tools/README.md b/prusti-tools/README.md
diff --git a/prusti-tools/build.rs b/prusti-tools/build.rs
diff --git a/prusti/Cargo.toml b/prusti/Cargo.toml
@@ -13,13 +13,27 @@ name = "prusti-driver"
 test = false
 path = "src/driver.rs"
 
+[[bin]]
+name = "prusti-rustc"
+test = false
+path = "src/prusti_rustc.rs"
+
+[[bin]]
+name = "cargo-prusti"
+test = false
+path = "src/cargo_prusti.rs"
+
 [dependencies]
 log = { version = "0.4", features = ["release_max_level_info"] }
 env_logger = "0.5.13"
 regex = "1.0.5"
 prusti-contracts = { path = "../prusti-contracts" }
 prusti-interface = { path = "../prusti-interface" }
 prusti-viper = { path = "../prusti-viper" }
+walkdir = "2"
 
 [build-dependencies]
 chrono = "0.4"
+
+[dev-dependencies]
+compiletest_rs = { git = "https://github.com/fpoli/compiletest-rs.git", branch="with-exit-code-101" }
diff --git a/prusti/README.md b/prusti/README.md
@@ -1,3 +1,3 @@
 # Prusti
 
-This crate provides the `prusti-driver` binary.
+This crate provides the Prusti binaries that can be used to verify a single Rust file or an entire crate.
diff --git a/prusti/build.rs b/prusti/build.rs
@@ -4,6 +4,11 @@ use chrono::prelude::Utc;
 use std::process::Command;
 
 fn main() {
+    println!(
+        "cargo:rustc-env=TARGET={}",
+        std::env::var("TARGET").unwrap()
+    );
+
     if let Some(git_hash) = Command::new("git")
         .args(&["rev-parse", "--short=19", "HEAD"])
         .output()

diff --git a/prusti-tools/src/cargo_prusti.rs → prusti/src/cargo_prusti.rs b/prusti-tools/src/cargo_prusti.rs → prusti/src/cargo_prusti.rs
diff --git a/prusti-tools/src/prusti_rustc.rs → prusti/src/prusti_rustc.rs b/prusti-tools/src/prusti_rustc.rs → prusti/src/prusti_rustc.rs
diff --git a/...tests/parse/fail/unsupported_attribute.rs → ...tests/parse/fail/unsupported_attribute.rs b/...tests/parse/fail/unsupported_attribute.rs → ...tests/parse/fail/unsupported_attribute.rs
diff --git a/prusti-tests/tests/parse/pass/doc_attr.rs → prusti/tests/parse/pass/doc_attr.rs b/prusti-tests/tests/parse/pass/doc_attr.rs → prusti/tests/parse/pass/doc_attr.rs
diff --git a/prusti-tests/tests/parse/ui/parenthesis.rs → prusti/tests/parse/ui/parenthesis.rs b/prusti-tests/tests/parse/ui/parenthesis.rs → prusti/tests/parse/ui/parenthesis.rs
diff --git a/...i-tests/tests/parse/ui/parenthesis.stderr → prusti/tests/parse/ui/parenthesis.stderr b/...i-tests/tests/parse/ui/parenthesis.stderr → prusti/tests/parse/ui/parenthesis.stderr
diff --git a/prusti-tests/tests/parse/ui/simple_and.rs → prusti/tests/parse/ui/simple_and.rs b/prusti-tests/tests/parse/ui/simple_and.rs → prusti/tests/parse/ui/simple_and.rs
diff --git a/...ti-tests/tests/parse/ui/simple_and.stderr → prusti/tests/parse/ui/simple_and.stderr b/...ti-tests/tests/parse/ui/simple_and.stderr → prusti/tests/parse/ui/simple_and.stderr
diff --git a/prusti-tests/tests/parse/ui/simple_forall.rs → prusti/tests/parse/ui/simple_forall.rs b/prusti-tests/tests/parse/ui/simple_forall.rs → prusti/tests/parse/ui/simple_forall.rs
diff --git a/...tests/tests/parse/ui/simple_forall.stderr → prusti/tests/parse/ui/simple_forall.stderr b/...tests/tests/parse/ui/simple_forall.stderr → prusti/tests/parse/ui/simple_forall.stderr
diff --git a/prusti-tests/tests/parse/ui/simple_imply.rs → prusti/tests/parse/ui/simple_imply.rs b/prusti-tests/tests/parse/ui/simple_imply.rs → prusti/tests/parse/ui/simple_imply.rs
diff --git a/...-tests/tests/parse/ui/simple_imply.stderr → prusti/tests/parse/ui/simple_imply.stderr b/...-tests/tests/parse/ui/simple_imply.stderr → prusti/tests/parse/ui/simple_imply.stderr
diff --git a/prusti-tests/tests/test.rs → prusti/tests/test.rs b/prusti-tests/tests/test.rs → prusti/tests/test.rs
diff --git a/...ypecheck/fail/specification_type_error.rs → ...ypecheck/fail/specification_type_error.rs b/...ypecheck/fail/specification_type_error.rs → ...ypecheck/fail/specification_type_error.rs
diff --git a/...sts/tests/typecheck/pass/borrow_struct.rs → prusti/tests/typecheck/pass/borrow_struct.rs b/...sts/tests/typecheck/pass/borrow_struct.rs → prusti/tests/typecheck/pass/borrow_struct.rs
diff --git a/...typecheck/pass/destructive_reborrowing.rs → ...typecheck/pass/destructive_reborrowing.rs b/...typecheck/pass/destructive_reborrowing.rs → ...typecheck/pass/destructive_reborrowing.rs
diff --git a/...sts/tests/typecheck/pass/lifetime_gaps.rs → prusti/tests/typecheck/pass/lifetime_gaps.rs b/...sts/tests/typecheck/pass/lifetime_gaps.rs → prusti/tests/typecheck/pass/lifetime_gaps.rs
diff --git a/prusti-tests/tests/typecheck/pass/lint.rs → prusti/tests/typecheck/pass/lint.rs b/prusti-tests/tests/typecheck/pass/lint.rs → prusti/tests/typecheck/pass/lint.rs
diff --git a/prusti-tests/tests/typecheck/pass/loops.rs → prusti/tests/typecheck/pass/loops.rs b/prusti-tests/tests/typecheck/pass/loops.rs → prusti/tests/typecheck/pass/loops.rs
diff --git a/.../tests/typecheck/pass/old_consumed_arg.rs → .../tests/typecheck/pass/old_consumed_arg.rs b/.../tests/typecheck/pass/old_consumed_arg.rs → .../tests/typecheck/pass/old_consumed_arg.rs
diff --git a/...tests/tests/typecheck/pass/reborrowing.rs → prusti/tests/typecheck/pass/reborrowing.rs b/...tests/tests/typecheck/pass/reborrowing.rs → prusti/tests/typecheck/pass/reborrowing.rs
diff --git a/...ts/typecheck/pass/reference_parameters.rs → ...ts/typecheck/pass/reference_parameters.rs b/...ts/typecheck/pass/reference_parameters.rs → ...ts/typecheck/pass/reference_parameters.rs
diff --git a/...sts/tests/typecheck/pass/split_borrows.rs → prusti/tests/typecheck/pass/split_borrows.rs b/...sts/tests/typecheck/pass/split_borrows.rs → prusti/tests/typecheck/pass/split_borrows.rs
diff --git a/...y/fail-overflow/crates/032_num_integer.rs → ...y/fail-overflow/crates/032_num_integer.rs b/...y/fail-overflow/crates/032_num_integer.rs → ...y/fail-overflow/crates/032_num_integer.rs
diff --git a/.../fail-overflow/crates/348_cgmath_point.rs → .../fail-overflow/crates/348_cgmath_point.rs b/.../fail-overflow/crates/348_cgmath_point.rs → .../fail-overflow/crates/348_cgmath_point.rs
diff --git a/...ests/verify/fail-overflow/fail-uint-fn.rs → ...ests/verify/fail-overflow/fail-uint-fn.rs b/...ests/verify/fail-overflow/fail-uint-fn.rs → ...ests/verify/fail-overflow/fail-uint-fn.rs
diff --git a/...ts/tests/verify/fail-overflow/overflow.rs → ...ti/tests/verify/fail-overflow/overflow.rs b/...ts/tests/verify/fail-overflow/overflow.rs → ...ti/tests/verify/fail-overflow/overflow.rs
diff --git a/...ts/verify/fail-overflow/overflow/calls.rs → ...ts/verify/fail-overflow/overflow/calls.rs b/...ts/verify/fail-overflow/overflow/calls.rs → ...ts/verify/fail-overflow/overflow/calls.rs
diff --git a/...erify/fail-overflow/overflow/div_isize.rs → ...erify/fail-overflow/overflow/div_isize.rs b/...erify/fail-overflow/overflow/div_isize.rs → ...erify/fail-overflow/overflow/div_isize.rs
diff --git a/.../verify/fail-overflow/overflow/div_u64.rs → .../verify/fail-overflow/overflow/div_u64.rs b/.../verify/fail-overflow/overflow/div_u64.rs → .../verify/fail-overflow/overflow/div_u64.rs
diff --git a/...ts/verify/fail-overflow/overflow/loops.rs → ...ts/verify/fail-overflow/overflow/loops.rs b/...ts/verify/fail-overflow/overflow/loops.rs → ...ts/verify/fail-overflow/overflow/loops.rs
diff --git a/...sts/verify/fail-overflow/overflow/pure.rs → ...sts/verify/fail-overflow/overflow/pure.rs b/...sts/verify/fail-overflow/overflow/pure.rs → ...sts/verify/fail-overflow/overflow/pure.rs
diff --git a/...ests/tests/verify/fail-overflow/panic3.rs → prusti/tests/verify/fail-overflow/panic3.rs b/...ests/tests/verify/fail-overflow/panic3.rs → prusti/tests/verify/fail-overflow/panic3.rs
diff --git a/...y/fail-overflow/pure-fn-overflow-error.rs → ...y/fail-overflow/pure-fn-overflow-error.rs b/...y/fail-overflow/pure-fn-overflow-error.rs → ...y/fail-overflow/pure-fn-overflow-error.rs
diff --git a/...ify/fail-overflow/rosetta/Langtons_ant.rs → ...ify/fail-overflow/rosetta/Langtons_ant.rs b/...ify/fail-overflow/rosetta/Langtons_ant.rs → ...ify/fail-overflow/rosetta/Langtons_ant.rs
diff --git a/...verify/fail/assert-false/compute-sound.rs → ...verify/fail/assert-false/compute-sound.rs b/...verify/fail/assert-false/compute-sound.rs → ...verify/fail/assert-false/compute-sound.rs
diff --git a/...ify/fail/assert-false/int-option-sound.rs → ...ify/fail/assert-false/int-option-sound.rs b/...ify/fail/assert-false/int-option-sound.rs → ...ify/fail/assert-false/int-option-sound.rs
diff --git a/...ts/verify/fail/assert-false/list-sound.rs → ...ts/verify/fail/assert-false/list-sound.rs b/...ts/verify/fail/assert-false/list-sound.rs → ...ts/verify/fail/assert-false/list-sound.rs
diff --git a/...ts/verify/fail/assert-false/tree-sound.rs → ...ts/verify/fail/assert-false/tree-sound.rs b/...ts/verify/fail/assert-false/tree-sound.rs → ...ts/verify/fail/assert-false/tree-sound.rs
diff --git a/...tests/verify/fail/crates/wrong-081-mio.rs → ...tests/verify/fail/crates/wrong-081-mio.rs b/...tests/verify/fail/crates/wrong-081-mio.rs → ...tests/verify/fail/crates/wrong-081-mio.rs
diff --git a/...verify/fail/crates/wrong-122-same-file.rs → ...verify/fail/crates/wrong-122-same-file.rs b/...verify/fail/crates/wrong-122-same-file.rs → ...verify/fail/crates/wrong-122-same-file.rs
diff --git a/...ts/verify/fail/erdinm/assert-on-expiry.rs → ...ts/verify/fail/erdinm/assert-on-expiry.rs b/...ts/verify/fail/erdinm/assert-on-expiry.rs → ...ts/verify/fail/erdinm/assert-on-expiry.rs
diff --git a/...ts/verify/fail/erdinm/generics-basic-1.rs → ...ts/verify/fail/erdinm/generics-basic-1.rs b/...ts/verify/fail/erdinm/generics-basic-1.rs → ...ts/verify/fail/erdinm/generics-basic-1.rs
diff --git a/...ts/verify/fail/erdinm/generics-basic-2.rs → ...ts/verify/fail/erdinm/generics-basic-2.rs b/...ts/verify/fail/erdinm/generics-basic-2.rs → ...ts/verify/fail/erdinm/generics-basic-2.rs
diff --git a/.../verify/fail/erdinm/generics-basic-3-1.rs → .../verify/fail/erdinm/generics-basic-3-1.rs b/.../verify/fail/erdinm/generics-basic-3-1.rs → .../verify/fail/erdinm/generics-basic-3-1.rs
diff --git a/.../verify/fail/erdinm/generics-basic-3-2.rs → .../verify/fail/erdinm/generics-basic-3-2.rs b/.../verify/fail/erdinm/generics-basic-3-2.rs → .../verify/fail/erdinm/generics-basic-3-2.rs
diff --git a/.../verify/fail/erdinm/generics-basic-3-3.rs → .../verify/fail/erdinm/generics-basic-3-3.rs b/.../verify/fail/erdinm/generics-basic-3-3.rs → .../verify/fail/erdinm/generics-basic-3-3.rs
diff --git a/.../verify/fail/erdinm/generics-basic-3-4.rs → .../verify/fail/erdinm/generics-basic-3-4.rs b/.../verify/fail/erdinm/generics-basic-3-4.rs → .../verify/fail/erdinm/generics-basic-3-4.rs
diff --git a/.../verify/fail/erdinm/generics-basic-3-5.rs → .../verify/fail/erdinm/generics-basic-3-5.rs b/.../verify/fail/erdinm/generics-basic-3-5.rs → .../verify/fail/erdinm/generics-basic-3-5.rs
diff --git a/.../verify/fail/erdinm/generics-basic-3-6.rs → .../verify/fail/erdinm/generics-basic-3-6.rs b/.../verify/fail/erdinm/generics-basic-3-6.rs → .../verify/fail/erdinm/generics-basic-3-6.rs
diff --git a/.../verify/fail/erdinm/generics-basic-4-1.rs → .../verify/fail/erdinm/generics-basic-4-1.rs b/.../verify/fail/erdinm/generics-basic-4-1.rs → .../verify/fail/erdinm/generics-basic-4-1.rs
diff --git a/.../verify/fail/erdinm/generics-basic-4-2.rs → .../verify/fail/erdinm/generics-basic-4-2.rs b/.../verify/fail/erdinm/generics-basic-4-2.rs → .../verify/fail/erdinm/generics-basic-4-2.rs
diff --git a/.../verify/fail/erdinm/generics-basic-5-1.rs → .../verify/fail/erdinm/generics-basic-5-1.rs b/.../verify/fail/erdinm/generics-basic-5-1.rs → .../verify/fail/erdinm/generics-basic-5-1.rs
diff --git a/.../verify/fail/erdinm/generics-basic-5-2.rs → .../verify/fail/erdinm/generics-basic-5-2.rs b/.../verify/fail/erdinm/generics-basic-5-2.rs → .../verify/fail/erdinm/generics-basic-5-2.rs
diff --git a/...s/verify/fail/erdinm/generics-combined.rs → ...s/verify/fail/erdinm/generics-combined.rs b/...s/verify/fail/erdinm/generics-combined.rs → ...s/verify/fail/erdinm/generics-combined.rs
diff --git a/.../verify/fail/erdinm/generics-special-1.rs → .../verify/fail/erdinm/generics-special-1.rs b/.../verify/fail/erdinm/generics-special-1.rs → .../verify/fail/erdinm/generics-special-1.rs
diff --git a/.../verify/fail/erdinm/invariants-basic-1.rs → .../verify/fail/erdinm/invariants-basic-1.rs b/.../verify/fail/erdinm/invariants-basic-1.rs → .../verify/fail/erdinm/invariants-basic-1.rs
diff --git a/.../verify/fail/erdinm/invariants-basic-2.rs → .../verify/fail/erdinm/invariants-basic-2.rs b/.../verify/fail/erdinm/invariants-basic-2.rs → .../verify/fail/erdinm/invariants-basic-2.rs
diff --git a/.../verify/fail/erdinm/invariants-basic-3.rs → .../verify/fail/erdinm/invariants-basic-3.rs b/.../verify/fail/erdinm/invariants-basic-3.rs → .../verify/fail/erdinm/invariants-basic-3.rs
diff --git a/.../verify/fail/erdinm/invariants-basic-4.rs → .../verify/fail/erdinm/invariants-basic-4.rs b/.../verify/fail/erdinm/invariants-basic-4.rs → .../verify/fail/erdinm/invariants-basic-4.rs
diff --git a/.../verify/fail/erdinm/invariants-basic-5.rs → .../verify/fail/erdinm/invariants-basic-5.rs b/.../verify/fail/erdinm/invariants-basic-5.rs → .../verify/fail/erdinm/invariants-basic-5.rs
diff --git a/.../verify/fail/erdinm/invariants-basic-6.rs → .../verify/fail/erdinm/invariants-basic-6.rs b/.../verify/fail/erdinm/invariants-basic-6.rs → .../verify/fail/erdinm/invariants-basic-6.rs
diff --git a/...verify/fail/erdinm/invariants-combined.rs → ...verify/fail/erdinm/invariants-combined.rs b/...verify/fail/erdinm/invariants-combined.rs → ...verify/fail/erdinm/invariants-combined.rs
diff --git a/...ify/fail/erdinm/invariants-pledges-2-1.rs → ...ify/fail/erdinm/invariants-pledges-2-1.rs b/...ify/fail/erdinm/invariants-pledges-2-1.rs → ...ify/fail/erdinm/invariants-pledges-2-1.rs
diff --git a/...ify/fail/erdinm/invariants-pledges-2-2.rs → ...ify/fail/erdinm/invariants-pledges-2-2.rs b/...ify/fail/erdinm/invariants-pledges-2-2.rs → ...ify/fail/erdinm/invariants-pledges-2-2.rs
diff --git a/...ify/fail/erdinm/invariants-pledges-3-1.rs → ...ify/fail/erdinm/invariants-pledges-3-1.rs b/...ify/fail/erdinm/invariants-pledges-3-1.rs → ...ify/fail/erdinm/invariants-pledges-3-1.rs
diff --git a/...ify/fail/erdinm/invariants-pledges-3-2.rs → ...ify/fail/erdinm/invariants-pledges-3-2.rs b/...ify/fail/erdinm/invariants-pledges-3-2.rs → ...ify/fail/erdinm/invariants-pledges-3-2.rs
diff --git a/...erdinm/invariants-typestates-basic-1-1.rs → ...erdinm/invariants-typestates-basic-1-1.rs b/...erdinm/invariants-typestates-basic-1-1.rs → ...erdinm/invariants-typestates-basic-1-1.rs
diff --git a/...erdinm/invariants-typestates-basic-1-2.rs → ...erdinm/invariants-typestates-basic-1-2.rs b/...erdinm/invariants-typestates-basic-1-2.rs → ...erdinm/invariants-typestates-basic-1-2.rs
diff --git a/...erdinm/invariants-typestates-basic-1-3.rs → ...erdinm/invariants-typestates-basic-1-3.rs b/...erdinm/invariants-typestates-basic-1-3.rs → ...erdinm/invariants-typestates-basic-1-3.rs
diff --git a/...erdinm/invariants-typestates-basic-2-1.rs → ...erdinm/invariants-typestates-basic-2-1.rs b/...erdinm/invariants-typestates-basic-2-1.rs → ...erdinm/invariants-typestates-basic-2-1.rs
diff --git a/...erdinm/invariants-typestates-basic-2-2.rs → ...erdinm/invariants-typestates-basic-2-2.rs b/...erdinm/invariants-typestates-basic-2-2.rs → ...erdinm/invariants-typestates-basic-2-2.rs
diff --git a/...erdinm/invariants-typestates-basic-2-3.rs → ...erdinm/invariants-typestates-basic-2-3.rs b/...erdinm/invariants-typestates-basic-2-3.rs → ...erdinm/invariants-typestates-basic-2-3.rs
diff --git a/...sts/verify/fail/erdinm/pledges-basic-1.rs → ...sts/verify/fail/erdinm/pledges-basic-1.rs b/...sts/verify/fail/erdinm/pledges-basic-1.rs → ...sts/verify/fail/erdinm/pledges-basic-1.rs
diff --git a/...s/verify/fail/erdinm/pledges-basic-2-1.rs → ...s/verify/fail/erdinm/pledges-basic-2-1.rs b/...s/verify/fail/erdinm/pledges-basic-2-1.rs → ...s/verify/fail/erdinm/pledges-basic-2-1.rs
diff --git a/...s/verify/fail/erdinm/pledges-basic-2-2.rs → ...s/verify/fail/erdinm/pledges-basic-2-2.rs b/...s/verify/fail/erdinm/pledges-basic-2-2.rs → ...s/verify/fail/erdinm/pledges-basic-2-2.rs
diff --git a/...s/verify/fail/erdinm/pledges-basic-2-3.rs → ...s/verify/fail/erdinm/pledges-basic-2-3.rs b/...s/verify/fail/erdinm/pledges-basic-2-3.rs → ...s/verify/fail/erdinm/pledges-basic-2-3.rs
diff --git a/...s/verify/fail/erdinm/pledges-basic-2-4.rs → ...s/verify/fail/erdinm/pledges-basic-2-4.rs b/...s/verify/fail/erdinm/pledges-basic-2-4.rs → ...s/verify/fail/erdinm/pledges-basic-2-4.rs
diff --git a/...s/verify/fail/erdinm/pledges-basic-2-5.rs → ...s/verify/fail/erdinm/pledges-basic-2-5.rs b/...s/verify/fail/erdinm/pledges-basic-2-5.rs → ...s/verify/fail/erdinm/pledges-basic-2-5.rs
diff --git a/...s/verify/fail/erdinm/pledges-basic-2-6.rs → ...s/verify/fail/erdinm/pledges-basic-2-6.rs b/...s/verify/fail/erdinm/pledges-basic-2-6.rs → ...s/verify/fail/erdinm/pledges-basic-2-6.rs
diff --git a/...rdinm/traits-basic-norm-prov-call-post.rs → ...rdinm/traits-basic-norm-prov-call-post.rs b/...rdinm/traits-basic-norm-prov-call-post.rs → ...rdinm/traits-basic-norm-prov-call-post.rs
diff --git a/...erdinm/traits-basic-norm-prov-call-pre.rs → ...erdinm/traits-basic-norm-prov-call-pre.rs b/...erdinm/traits-basic-norm-prov-call-pre.rs → ...erdinm/traits-basic-norm-prov-call-pre.rs
diff --git a/...rdinm/traits-basic-norm-prov-defi-post.rs → ...rdinm/traits-basic-norm-prov-defi-post.rs b/...rdinm/traits-basic-norm-prov-defi-post.rs → ...rdinm/traits-basic-norm-prov-defi-post.rs
diff --git a/...erdinm/traits-basic-norm-prov-defi-pre.rs → ...erdinm/traits-basic-norm-prov-defi-pre.rs b/...erdinm/traits-basic-norm-prov-defi-pre.rs → ...erdinm/traits-basic-norm-prov-defi-pre.rs
diff --git a/...rdinm/traits-basic-norm-prov-impl-post.rs → ...rdinm/traits-basic-norm-prov-impl-post.rs b/...rdinm/traits-basic-norm-prov-impl-post.rs → ...rdinm/traits-basic-norm-prov-impl-post.rs
diff --git a/...erdinm/traits-basic-norm-prov-impl-pre.rs → ...erdinm/traits-basic-norm-prov-impl-pre.rs b/...erdinm/traits-basic-norm-prov-impl-pre.rs → ...erdinm/traits-basic-norm-prov-impl-pre.rs
diff --git a/...rdinm/traits-basic-norm-reqd-call-post.rs → ...rdinm/traits-basic-norm-reqd-call-post.rs b/...rdinm/traits-basic-norm-reqd-call-post.rs → ...rdinm/traits-basic-norm-reqd-call-post.rs
diff --git a/...erdinm/traits-basic-norm-reqd-call-pre.rs → ...erdinm/traits-basic-norm-reqd-call-pre.rs b/...erdinm/traits-basic-norm-reqd-call-pre.rs → ...erdinm/traits-basic-norm-reqd-call-pre.rs
diff --git a/...rdinm/traits-basic-norm-reqd-impl-post.rs → ...rdinm/traits-basic-norm-reqd-impl-post.rs b/...rdinm/traits-basic-norm-reqd-impl-post.rs → ...rdinm/traits-basic-norm-reqd-impl-post.rs
diff --git a/...erdinm/traits-basic-norm-reqd-impl-pre.rs → ...erdinm/traits-basic-norm-reqd-impl-pre.rs b/...erdinm/traits-basic-norm-reqd-impl-pre.rs → ...erdinm/traits-basic-norm-reqd-impl-pre.rs
diff --git a/...sts/verify/fail/erdinm/traits-combined.rs → ...sts/verify/fail/erdinm/traits-combined.rs b/...sts/verify/fail/erdinm/traits-combined.rs → ...sts/verify/fail/erdinm/traits-combined.rs
diff --git a/...erify/fail/erdinm/typestates-basic-1-1.rs → ...erify/fail/erdinm/typestates-basic-1-1.rs b/...erify/fail/erdinm/typestates-basic-1-1.rs → ...erify/fail/erdinm/typestates-basic-1-1.rs
diff --git a/...erify/fail/erdinm/typestates-basic-1-2.rs → ...erify/fail/erdinm/typestates-basic-1-2.rs b/...erify/fail/erdinm/typestates-basic-1-2.rs → ...erify/fail/erdinm/typestates-basic-1-2.rs
diff --git a/...erify/fail/erdinm/typestates-basic-1-3.rs → ...erify/fail/erdinm/typestates-basic-1-3.rs b/...erify/fail/erdinm/typestates-basic-1-3.rs → ...erify/fail/erdinm/typestates-basic-1-3.rs
diff --git a/...verify/fail/erdinm/typestates-combined.rs → ...verify/fail/erdinm/typestates-combined.rs b/...verify/fail/erdinm/typestates-combined.rs → ...verify/fail/erdinm/typestates-combined.rs
diff --git a/.../tests/verify/fail/fold-unfold/balance.rs → .../tests/verify/fail/fold-unfold/balance.rs b/.../tests/verify/fail/fold-unfold/balance.rs → .../tests/verify/fail/fold-unfold/balance.rs
diff --git a/.../verify/fail/fold-unfold/negative-enum.rs → .../verify/fail/fold-unfold/negative-enum.rs b/.../verify/fail/fold-unfold/negative-enum.rs → .../verify/fail/fold-unfold/negative-enum.rs
diff --git a/...tests/verify/fail/fold-unfold/negative.rs → ...tests/verify/fail/fold-unfold/negative.rs b/...tests/verify/fail/fold-unfold/negative.rs → ...tests/verify/fail/fold-unfold/negative.rs
diff --git a/...ests/verify/fail/issues/issue-25-wrong.rs → ...ests/verify/fail/issues/issue-25-wrong.rs b/...ests/verify/fail/issues/issue-25-wrong.rs → ...ests/verify/fail/issues/issue-25-wrong.rs
diff --git a/...ests/tests/verify/fail/issues/issue-72.rs → prusti/tests/verify/fail/issues/issue-72.rs b/...ests/tests/verify/fail/issues/issue-72.rs → prusti/tests/verify/fail/issues/issue-72.rs
diff --git a/...ests/tests/verify/fail/issues/issue-73.rs → prusti/tests/verify/fail/issues/issue-73.rs b/...ests/tests/verify/fail/issues/issue-73.rs → prusti/tests/verify/fail/issues/issue-73.rs
diff --git a/...ests/tests/verify/fail/issues/issue-74.rs → prusti/tests/verify/fail/issues/issue-74.rs b/...ests/tests/verify/fail/issues/issue-74.rs → prusti/tests/verify/fail/issues/issue-74.rs
diff --git a/.../tests/verify/fail/issues/issue-81-ops.rs → .../tests/verify/fail/issues/issue-81-ops.rs b/.../tests/verify/fail/issues/issue-81-ops.rs → .../tests/verify/fail/issues/issue-81-ops.rs
diff --git a/...ts/verify/fail/issues/issue-81-pure-fn.rs → ...ts/verify/fail/issues/issue-81-pure-fn.rs b/...ts/verify/fail/issues/issue-81-pure-fn.rs → ...ts/verify/fail/issues/issue-81-pure-fn.rs
diff --git a/...ests/tests/verify/fail/issues/issue-81.rs → prusti/tests/verify/fail/issues/issue-81.rs b/...ests/tests/verify/fail/issues/issue-81.rs → prusti/tests/verify/fail/issues/issue-81.rs
diff --git a/...ests/tests/verify/fail/issues/issue-90.rs → prusti/tests/verify/fail/issues/issue-90.rs b/...ests/tests/verify/fail/issues/issue-90.rs → prusti/tests/verify/fail/issues/issue-90.rs
diff --git a/...y/fail/magic-wands/wrong-wand-identity.rs → ...y/fail/magic-wands/wrong-wand-identity.rs b/...y/fail/magic-wands/wrong-wand-identity.rs → ...y/fail/magic-wands/wrong-wand-identity.rs
diff --git a/.../fail/magic-wands/wrong-wand-identity2.rs → .../fail/magic-wands/wrong-wand-identity2.rs b/.../fail/magic-wands/wrong-wand-identity2.rs → .../fail/magic-wands/wrong-wand-identity2.rs
diff --git a/...ti-tests/tests/verify/fail/moves/basic.rs → prusti/tests/verify/fail/moves/basic.rs b/...ti-tests/tests/verify/fail/moves/basic.rs → prusti/tests/verify/fail/moves/basic.rs
diff --git a/...ests/tests/verify/fail/nll-rfc/message.rs → prusti/tests/verify/fail/nll-rfc/message.rs b/...ests/tests/verify/fail/nll-rfc/message.rs → prusti/tests/verify/fail/nll-rfc/message.rs
diff --git a/.../tests/verify/fail/nll-rfc/wrong-case1.rs → .../tests/verify/fail/nll-rfc/wrong-case1.rs b/.../tests/verify/fail/nll-rfc/wrong-case1.rs → .../tests/verify/fail/nll-rfc/wrong-case1.rs
diff --git a/...verify/fail/no-annotations/assert-bool.rs → ...verify/fail/no-annotations/assert-bool.rs b/...verify/fail/no-annotations/assert-bool.rs → ...verify/fail/no-annotations/assert-bool.rs
diff --git a/...erify/fail/no-annotations/assert-false.rs → ...erify/fail/no-annotations/assert-false.rs b/...erify/fail/no-annotations/assert-false.rs → ...erify/fail/no-annotations/assert-false.rs
diff --git a/.../fail/no-annotations/assert-from-macro.rs → .../fail/no-annotations/assert-from-macro.rs b/.../fail/no-annotations/assert-from-macro.rs → .../fail/no-annotations/assert-from-macro.rs
diff --git a/...verify/fail/no-annotations/div-by-zero.rs → ...verify/fail/no-annotations/div-by-zero.rs b/...verify/fail/no-annotations/div-by-zero.rs → ...verify/fail/no-annotations/div-by-zero.rs
diff --git a/...ify/fail/no-annotations/divide-by-zero.rs → ...ify/fail/no-annotations/divide-by-zero.rs b/...ify/fail/no-annotations/divide-by-zero.rs → ...ify/fail/no-annotations/divide-by-zero.rs
diff --git a/...fail/no-annotations/external-call-fail.rs → ...fail/no-annotations/external-call-fail.rs b/...fail/no-annotations/external-call-fail.rs → ...fail/no-annotations/external-call-fail.rs
diff --git a/...fy/fail/no-annotations/multiple-errors.rs → ...fy/fail/no-annotations/multiple-errors.rs b/...fy/fail/no-annotations/multiple-errors.rs → ...fy/fail/no-annotations/multiple-errors.rs
diff --git a/.../verify/fail/no-annotations/never-type.rs → .../verify/fail/no-annotations/never-type.rs b/.../verify/fail/no-annotations/never-type.rs → .../verify/fail/no-annotations/never-type.rs
diff --git a/...tests/verify/fail/no-annotations/panic.rs → ...tests/verify/fail/no-annotations/panic.rs b/...tests/verify/fail/no-annotations/panic.rs → ...tests/verify/fail/no-annotations/panic.rs
diff --git a/...ests/verify/fail/no-annotations/panic2.rs → ...ests/verify/fail/no-annotations/panic2.rs b/...ests/verify/fail/no-annotations/panic2.rs → ...ests/verify/fail/no-annotations/panic2.rs
diff --git a/...fail/no-annotations/predicate-old-expr.rs → ...fail/no-annotations/predicate-old-expr.rs b/...fail/no-annotations/predicate-old-expr.rs → ...fail/no-annotations/predicate-old-expr.rs
diff --git a/...fy/fail/no-annotations/redefine-assert.rs → ...fy/fail/no-annotations/redefine-assert.rs b/...fy/fail/no-annotations/redefine-assert.rs → ...fy/fail/no-annotations/redefine-assert.rs
diff --git a/...rify/fail/no-annotations/unimplemented.rs → ...rify/fail/no-annotations/unimplemented.rs b/...rify/fail/no-annotations/unimplemented.rs → ...rify/fail/no-annotations/unimplemented.rs
diff --git a/...y/fail/no-annotations/unreachable-fail.rs → ...y/fail/no-annotations/unreachable-fail.rs b/...y/fail/no-annotations/unreachable-fail.rs → ...y/fail/no-annotations/unreachable-fail.rs
diff --git a/...verify/fail/no-annotations/unreachable.rs → ...verify/fail/no-annotations/unreachable.rs b/...verify/fail/no-annotations/unreachable.rs → ...verify/fail/no-annotations/unreachable.rs
diff --git a/...ests/tests/verify/fail/pure-fn/fail-pc.rs → prusti/tests/verify/fail/pure-fn/fail-pc.rs b/...ests/tests/verify/fail/pure-fn/fail-pc.rs → prusti/tests/verify/fail/pure-fn/fail-pc.rs
diff --git a/...sts/verify/fail/pure-fn/integer_bounds.rs → ...sts/verify/fail/pure-fn/integer_bounds.rs b/...sts/verify/fail/pure-fn/integer_bounds.rs → ...sts/verify/fail/pure-fn/integer_bounds.rs
diff --git a/.../tests/verify/fail/pure-fn/panic-in-fn.rs → .../tests/verify/fail/pure-fn/panic-in-fn.rs b/.../tests/verify/fail/pure-fn/panic-in-fn.rs → .../tests/verify/fail/pure-fn/panic-in-fn.rs
diff --git a/.../verify/fail/pure-fn/wrong-quantifiers.rs → .../verify/fail/pure-fn/wrong-quantifiers.rs b/.../verify/fail/pure-fn/wrong-quantifiers.rs → .../verify/fail/pure-fn/wrong-quantifiers.rs
diff --git a/.../verify/fail/pure-fn/wrong-ref-mut-arg.rs → .../verify/fail/pure-fn/wrong-ref-mut-arg.rs b/.../verify/fail/pure-fn/wrong-ref-mut-arg.rs → .../verify/fail/pure-fn/wrong-ref-mut-arg.rs
diff --git a/...ts/verify/fail/pure-fn/wrong-simple-fn.rs → ...ts/verify/fail/pure-fn/wrong-simple-fn.rs b/...ts/verify/fail/pure-fn/wrong-simple-fn.rs → ...ts/verify/fail/pure-fn/wrong-simple-fn.rs
diff --git a/...tests/verify/fail/shared-borrows/basic.rs → ...tests/verify/fail/shared-borrows/basic.rs b/...tests/verify/fail/shared-borrows/basic.rs → ...tests/verify/fail/shared-borrows/basic.rs
diff --git a/...erify/fail/shared-borrows/conditionals.rs → ...erify/fail/shared-borrows/conditionals.rs b/...erify/fail/shared-borrows/conditionals.rs → ...erify/fail/shared-borrows/conditionals.rs
diff --git a/...s/verify/fail/shared-borrows/functions.rs → ...s/verify/fail/shared-borrows/functions.rs b/...s/verify/fail/shared-borrows/functions.rs → ...s/verify/fail/shared-borrows/functions.rs
diff --git a/...tests/verify/fail/shared-borrows/loops.rs → ...tests/verify/fail/shared-borrows/loops.rs b/...tests/verify/fail/shared-borrows/loops.rs → ...tests/verify/fail/shared-borrows/loops.rs
diff --git a/...verify/fail/shared-borrows/mut-borrows.rs → ...verify/fail/shared-borrows/mut-borrows.rs b/...verify/fail/shared-borrows/mut-borrows.rs → ...verify/fail/shared-borrows/mut-borrows.rs
diff --git a/...verify/fail/shared-borrows/reborrowing.rs → ...verify/fail/shared-borrows/reborrowing.rs b/...verify/fail/shared-borrows/reborrowing.rs → ...verify/fail/shared-borrows/reborrowing.rs
diff --git a/...ts/verify/fail/with-spec/binary-search.rs → ...ts/verify/fail/with-spec/binary-search.rs b/...ts/verify/fail/with-spec/binary-search.rs → ...ts/verify/fail/with-spec/binary-search.rs
diff --git a/...ts/verify/fail/with-spec/ensures-false.rs → ...ts/verify/fail/with-spec/ensures-false.rs b/...ts/verify/fail/with-spec/ensures-false.rs → ...ts/verify/fail/with-spec/ensures-false.rs
diff --git a/...ify/fail/with-spec/loops-before-inside.rs → ...ify/fail/with-spec/loops-before-inside.rs b/...ify/fail/with-spec/loops-before-inside.rs → ...ify/fail/with-spec/loops-before-inside.rs
diff --git a/.../verify/fail/with-spec/no-precondition.rs → .../verify/fail/with-spec/no-precondition.rs b/.../verify/fail/with-spec/no-precondition.rs → .../verify/fail/with-spec/no-precondition.rs
diff --git a/...ests/verify/fail/with-spec/trees-wrong.rs → ...ests/verify/fail/with-spec/trees-wrong.rs b/...ests/verify/fail/with-spec/trees-wrong.rs → ...ests/verify/fail/with-spec/trees-wrong.rs
diff --git a/...ts/verify/fail/with-spec/unsigned_ints.rs → ...ts/verify/fail/with-spec/unsigned_ints.rs b/...ts/verify/fail/with-spec/unsigned_ints.rs → ...ts/verify/fail/with-spec/unsigned_ints.rs
diff --git a/...s/verify/fail/with-spec/wrong-identity.rs → ...s/verify/fail/with-spec/wrong-identity.rs b/...s/verify/fail/with-spec/wrong-identity.rs → ...s/verify/fail/with-spec/wrong-identity.rs
diff --git a/...sts/verify/fail/with-spec/wrong-method.rs → ...sts/verify/fail/with-spec/wrong-method.rs b/...sts/verify/fail/with-spec/wrong-method.rs → ...sts/verify/fail/with-spec/wrong-method.rs
diff --git a/.../tests/verify/pass-overflow/div_rem_64.rs → .../tests/verify/pass-overflow/div_rem_64.rs b/.../tests/verify/pass-overflow/div_rem_64.rs → .../tests/verify/pass-overflow/div_rem_64.rs
diff --git a/...sts/verify/pass-overflow/iso_week_days.rs → ...sts/verify/pass-overflow/iso_week_days.rs b/...sts/verify/pass-overflow/iso_week_days.rs → ...sts/verify/pass-overflow/iso_week_days.rs
diff --git a/.../verify/pass-overflow/issues/issue-104.rs → .../verify/pass-overflow/issues/issue-104.rs b/.../verify/pass-overflow/issues/issue-104.rs → .../verify/pass-overflow/issues/issue-104.rs
diff --git a/...ts/verify/pass-overflow/mul_add_assign.rs → ...ts/verify/pass-overflow/mul_add_assign.rs b/...ts/verify/pass-overflow/mul_add_assign.rs → ...ts/verify/pass-overflow/mul_add_assign.rs
diff --git a/...ify/pass-overflow/nll-rfc/borrow_first.rs → ...ify/pass-overflow/nll-rfc/borrow_first.rs b/...ify/pass-overflow/nll-rfc/borrow_first.rs → ...ify/pass-overflow/nll-rfc/borrow_first.rs
diff --git a/...y/pass-overflow/nll-rfc/case1-overflow.rs → ...y/pass-overflow/nll-rfc/case1-overflow.rs b/...y/pass-overflow/nll-rfc/case1-overflow.rs → ...y/pass-overflow/nll-rfc/case1-overflow.rs
diff --git a/...s/verify/pass-overflow/nll-rfc/message.rs → ...s/verify/pass-overflow/nll-rfc/message.rs b/...s/verify/pass-overflow/nll-rfc/message.rs → ...s/verify/pass-overflow/nll-rfc/message.rs
diff --git a/...ts/verify/pass-overflow/overflow/calls.rs → ...ts/verify/pass-overflow/overflow/calls.rs b/...ts/verify/pass-overflow/overflow/calls.rs → ...ts/verify/pass-overflow/overflow/calls.rs
diff --git a/...ts/verify/pass-overflow/overflow/loops.rs → ...ts/verify/pass-overflow/overflow/loops.rs b/...ts/verify/pass-overflow/overflow/loops.rs → ...ts/verify/pass-overflow/overflow/loops.rs
diff --git a/...sts/verify/pass-overflow/overflow/pure.rs → ...sts/verify/pass-overflow/overflow/pure.rs b/...sts/verify/pass-overflow/overflow/pure.rs → ...sts/verify/pass-overflow/overflow/pure.rs
diff --git a/...verify/pass-overflow/rosetta/100_doors.rs → ...verify/pass-overflow/rosetta/100_doors.rs b/...verify/pass-overflow/rosetta/100_doors.rs → ...verify/pass-overflow/rosetta/100_doors.rs
diff --git a/...ass-overflow/rosetta/100_doors_generic.rs → ...ass-overflow/rosetta/100_doors_generic.rs b/...ass-overflow/rosetta/100_doors_generic.rs → ...ass-overflow/rosetta/100_doors_generic.rs
diff --git a/...fy/pass-overflow/rosetta/Binary_search.rs → ...fy/pass-overflow/rosetta/Binary_search.rs b/...fy/pass-overflow/rosetta/Binary_search.rs → ...fy/pass-overflow/rosetta/Binary_search.rs
diff --git a/...-overflow/rosetta/Binary_search_shared.rs → ...-overflow/rosetta/Binary_search_shared.rs b/...-overflow/rosetta/Binary_search_shared.rs → ...-overflow/rosetta/Binary_search_shared.rs
diff --git a/...tta/Binary_search_shared_monomorphised.rs → ...tta/Binary_search_shared_monomorphised.rs b/...tta/Binary_search_shared_monomorphised.rs → ...tta/Binary_search_shared_monomorphised.rs
diff --git a/...pass-overflow/rosetta/Heapsort_generic.rs → ...pass-overflow/rosetta/Heapsort_generic.rs b/...pass-overflow/rosetta/Heapsort_generic.rs → ...pass-overflow/rosetta/Heapsort_generic.rs
diff --git a/...-overflow/rosetta/Knights_tour_generic.rs → ...-overflow/rosetta/Knights_tour_generic.rs b/...-overflow/rosetta/Knights_tour_generic.rs → ...-overflow/rosetta/Knights_tour_generic.rs
diff --git a/...fy/pass-overflow/rosetta/Knuth_shuffle.rs → ...fy/pass-overflow/rosetta/Knuth_shuffle.rs b/...fy/pass-overflow/rosetta/Knuth_shuffle.rs → ...fy/pass-overflow/rosetta/Knuth_shuffle.rs
diff --git a/...ify/pass-overflow/rosetta/Langtons_ant.rs → ...ify/pass-overflow/rosetta/Langtons_ant.rs b/...ify/pass-overflow/rosetta/Langtons_ant.rs → ...ify/pass-overflow/rosetta/Langtons_ant.rs
diff --git a/...pass-overflow/rosetta/Mutual_recursion.rs → ...pass-overflow/rosetta/Mutual_recursion.rs b/...pass-overflow/rosetta/Mutual_recursion.rs → ...pass-overflow/rosetta/Mutual_recursion.rs
diff --git a/...y/pass-overflow/rosetta/Selection_sort.rs → ...y/pass-overflow/rosetta/Selection_sort.rs b/...y/pass-overflow/rosetta/Selection_sort.rs → ...y/pass-overflow/rosetta/Selection_sort.rs
diff --git a/...verflow/rosetta/Selection_sort_generic.rs → ...verflow/rosetta/Selection_sort_generic.rs b/...verflow/rosetta/Selection_sort_generic.rs → ...verflow/rosetta/Selection_sort_generic.rs
diff --git a/...ss-overflow/rosetta/Singly_Linked_List.rs → ...ss-overflow/rosetta/Singly_Linked_List.rs b/...ss-overflow/rosetta/Singly_Linked_List.rs → ...ss-overflow/rosetta/Singly_Linked_List.rs
diff --git a/.../pass-overflow/rosetta/Towers_of_Hanoi.rs → .../pass-overflow/rosetta/Towers_of_Hanoi.rs b/.../pass-overflow/rosetta/Towers_of_Hanoi.rs → .../pass-overflow/rosetta/Towers_of_Hanoi.rs
diff --git a/...-overflow/rosetta/Towers_of_Hanoi_spec.rs → ...-overflow/rosetta/Towers_of_Hanoi_spec.rs b/...-overflow/rosetta/Towers_of_Hanoi_spec.rs → ...-overflow/rosetta/Towers_of_Hanoi_spec.rs
diff --git a/...-tests/tests/verify/pass-overflow/uint.rs → prusti/tests/verify/pass-overflow/uint.rs b/...-tests/tests/verify/pass-overflow/uint.rs → prusti/tests/verify/pass-overflow/uint.rs
diff --git a/...-tests/tests/verify/pass/copy/generics.rs → prusti/tests/verify/pass/copy/generics.rs b/...-tests/tests/verify/pass/copy/generics.rs → prusti/tests/verify/pass/copy/generics.rs
diff --git a/.../verify/pass/crates/008-num-traits-pow.rs → .../verify/pass/crates/008-num-traits-pow.rs b/.../verify/pass/crates/008-num-traits-pow.rs → .../verify/pass/crates/008-num-traits-pow.rs
diff --git a/...tests/tests/verify/pass/crates/081-mio.rs → prusti/tests/verify/pass/crates/081-mio.rs b/...tests/tests/verify/pass/crates/081-mio.rs → prusti/tests/verify/pass/crates/081-mio.rs
diff --git a/...tests/verify/pass/crates/122-same-file.rs → ...tests/verify/pass/crates/122-same-file.rs b/...tests/verify/pass/crates/122-same-file.rs → ...tests/verify/pass/crates/122-same-file.rs
diff --git a/.../tests/verify/pass/crates/131-tokio-io.rs → .../tests/verify/pass/crates/131-tokio-io.rs b/.../tests/verify/pass/crates/131-tokio-io.rs → .../tests/verify/pass/crates/131-tokio-io.rs
diff --git a/...fy/pass/crates/ansi-term-external-call.rs → ...fy/pass/crates/ansi-term-external-call.rs b/...fy/pass/crates/ansi-term-external-call.rs → ...fy/pass/crates/ansi-term-external-call.rs
diff --git a/...ti-tests/tests/verify/pass/enums/basic.rs → prusti/tests/verify/pass/enums/basic.rs b/...ti-tests/tests/verify/pass/enums/basic.rs → prusti/tests/verify/pass/enums/basic.rs
diff --git a/...-tests/tests/verify/pass/enums/builtin.rs → prusti/tests/verify/pass/enums/builtin.rs b/...-tests/tests/verify/pass/enums/builtin.rs → prusti/tests/verify/pass/enums/builtin.rs
diff --git a/...s/tests/verify/pass/enums/name-clashes.rs → ...i/tests/verify/pass/enums/name-clashes.rs b/...s/tests/verify/pass/enums/name-clashes.rs → ...i/tests/verify/pass/enums/name-clashes.rs
diff --git a/...ts/verify/pass/erdinm/generics-basic-1.rs → ...ts/verify/pass/erdinm/generics-basic-1.rs b/...ts/verify/pass/erdinm/generics-basic-1.rs → ...ts/verify/pass/erdinm/generics-basic-1.rs
diff --git a/...ts/verify/pass/erdinm/generics-basic-2.rs → ...ts/verify/pass/erdinm/generics-basic-2.rs b/...ts/verify/pass/erdinm/generics-basic-2.rs → ...ts/verify/pass/erdinm/generics-basic-2.rs
diff --git a/...ts/verify/pass/erdinm/generics-basic-3.rs → ...ts/verify/pass/erdinm/generics-basic-3.rs b/...ts/verify/pass/erdinm/generics-basic-3.rs → ...ts/verify/pass/erdinm/generics-basic-3.rs
diff --git a/...ts/verify/pass/erdinm/generics-basic-4.rs → ...ts/verify/pass/erdinm/generics-basic-4.rs b/...ts/verify/pass/erdinm/generics-basic-4.rs → ...ts/verify/pass/erdinm/generics-basic-4.rs
diff --git a/...ts/verify/pass/erdinm/generics-basic-5.rs → ...ts/verify/pass/erdinm/generics-basic-5.rs b/...ts/verify/pass/erdinm/generics-basic-5.rs → ...ts/verify/pass/erdinm/generics-basic-5.rs
diff --git a/...ts/verify/pass/erdinm/generics-basic-6.rs → ...ts/verify/pass/erdinm/generics-basic-6.rs b/...ts/verify/pass/erdinm/generics-basic-6.rs → ...ts/verify/pass/erdinm/generics-basic-6.rs
diff --git a/...ts/verify/pass/erdinm/generics-basic-7.rs → ...ts/verify/pass/erdinm/generics-basic-7.rs b/...ts/verify/pass/erdinm/generics-basic-7.rs → ...ts/verify/pass/erdinm/generics-basic-7.rs
diff --git a/...ts/verify/pass/erdinm/generics-basic-8.rs → ...ts/verify/pass/erdinm/generics-basic-8.rs b/...ts/verify/pass/erdinm/generics-basic-8.rs → ...ts/verify/pass/erdinm/generics-basic-8.rs
diff --git a/.../verify/pass/erdinm/invariants-basic-1.rs → .../verify/pass/erdinm/invariants-basic-1.rs b/.../verify/pass/erdinm/invariants-basic-1.rs → .../verify/pass/erdinm/invariants-basic-1.rs
diff --git a/.../verify/pass/erdinm/invariants-basic-2.rs → .../verify/pass/erdinm/invariants-basic-2.rs b/.../verify/pass/erdinm/invariants-basic-2.rs → .../verify/pass/erdinm/invariants-basic-2.rs
diff --git a/.../verify/pass/erdinm/invariants-basic-3.rs → .../verify/pass/erdinm/invariants-basic-3.rs b/.../verify/pass/erdinm/invariants-basic-3.rs → .../verify/pass/erdinm/invariants-basic-3.rs
diff --git a/.../verify/pass/erdinm/invariants-basic-4.rs → .../verify/pass/erdinm/invariants-basic-4.rs b/.../verify/pass/erdinm/invariants-basic-4.rs → .../verify/pass/erdinm/invariants-basic-4.rs
diff --git a/.../verify/pass/erdinm/invariants-basic-5.rs → .../verify/pass/erdinm/invariants-basic-5.rs b/.../verify/pass/erdinm/invariants-basic-5.rs → .../verify/pass/erdinm/invariants-basic-5.rs
diff --git a/.../verify/pass/erdinm/invariants-basic-6.rs → .../verify/pass/erdinm/invariants-basic-6.rs b/.../verify/pass/erdinm/invariants-basic-6.rs → .../verify/pass/erdinm/invariants-basic-6.rs
diff --git a/...erify/pass/erdinm/invariants-pledges-2.rs → ...erify/pass/erdinm/invariants-pledges-2.rs b/...erify/pass/erdinm/invariants-pledges-2.rs → ...erify/pass/erdinm/invariants-pledges-2.rs
diff --git a/...erify/pass/erdinm/invariants-pledges-3.rs → ...erify/pass/erdinm/invariants-pledges-3.rs b/...erify/pass/erdinm/invariants-pledges-3.rs → ...erify/pass/erdinm/invariants-pledges-3.rs
diff --git a/...erify/pass/erdinm/invariants-pledges-4.rs → ...erify/pass/erdinm/invariants-pledges-4.rs b/...erify/pass/erdinm/invariants-pledges-4.rs → ...erify/pass/erdinm/invariants-pledges-4.rs
diff --git a/...s/erdinm/invariants-typestates-basic-1.rs → ...s/erdinm/invariants-typestates-basic-1.rs b/...s/erdinm/invariants-typestates-basic-1.rs → ...s/erdinm/invariants-typestates-basic-1.rs
diff --git a/...s/erdinm/invariants-typestates-basic-2.rs → ...s/erdinm/invariants-typestates-basic-2.rs b/...s/erdinm/invariants-typestates-basic-2.rs → ...s/erdinm/invariants-typestates-basic-2.rs
diff --git a/...sts/verify/pass/erdinm/pledges-basic-1.rs → ...sts/verify/pass/erdinm/pledges-basic-1.rs b/...sts/verify/pass/erdinm/pledges-basic-1.rs → ...sts/verify/pass/erdinm/pledges-basic-1.rs
diff --git a/...sts/verify/pass/erdinm/pledges-basic-2.rs → ...sts/verify/pass/erdinm/pledges-basic-2.rs b/...sts/verify/pass/erdinm/pledges-basic-2.rs → ...sts/verify/pass/erdinm/pledges-basic-2.rs
diff --git a/...rdinm/traits-basic-norm-prov-call-post.rs → ...rdinm/traits-basic-norm-prov-call-post.rs b/...rdinm/traits-basic-norm-prov-call-post.rs → ...rdinm/traits-basic-norm-prov-call-post.rs
diff --git a/...erdinm/traits-basic-norm-prov-call-pre.rs → ...erdinm/traits-basic-norm-prov-call-pre.rs b/...erdinm/traits-basic-norm-prov-call-pre.rs → ...erdinm/traits-basic-norm-prov-call-pre.rs
diff --git a/...rdinm/traits-basic-norm-prov-defi-post.rs → ...rdinm/traits-basic-norm-prov-defi-post.rs b/...rdinm/traits-basic-norm-prov-defi-post.rs → ...rdinm/traits-basic-norm-prov-defi-post.rs
diff --git a/...erdinm/traits-basic-norm-prov-defi-pre.rs → ...erdinm/traits-basic-norm-prov-defi-pre.rs b/...erdinm/traits-basic-norm-prov-defi-pre.rs → ...erdinm/traits-basic-norm-prov-defi-pre.rs
diff --git a/...rdinm/traits-basic-norm-prov-impl-post.rs → ...rdinm/traits-basic-norm-prov-impl-post.rs b/...rdinm/traits-basic-norm-prov-impl-post.rs → ...rdinm/traits-basic-norm-prov-impl-post.rs
diff --git a/...erdinm/traits-basic-norm-prov-impl-pre.rs → ...erdinm/traits-basic-norm-prov-impl-pre.rs b/...erdinm/traits-basic-norm-prov-impl-pre.rs → ...erdinm/traits-basic-norm-prov-impl-pre.rs
diff --git a/...rdinm/traits-basic-norm-reqd-call-post.rs → ...rdinm/traits-basic-norm-reqd-call-post.rs b/...rdinm/traits-basic-norm-reqd-call-post.rs → ...rdinm/traits-basic-norm-reqd-call-post.rs
diff --git a/...erdinm/traits-basic-norm-reqd-call-pre.rs → ...erdinm/traits-basic-norm-reqd-call-pre.rs b/...erdinm/traits-basic-norm-reqd-call-pre.rs → ...erdinm/traits-basic-norm-reqd-call-pre.rs
diff --git a/...rdinm/traits-basic-norm-reqd-impl-post.rs → ...rdinm/traits-basic-norm-reqd-impl-post.rs b/...rdinm/traits-basic-norm-reqd-impl-post.rs → ...rdinm/traits-basic-norm-reqd-impl-post.rs
diff --git a/...erdinm/traits-basic-norm-reqd-impl-pre.rs → ...erdinm/traits-basic-norm-reqd-impl-pre.rs b/...erdinm/traits-basic-norm-reqd-impl-pre.rs → ...erdinm/traits-basic-norm-reqd-impl-pre.rs
diff --git a/.../verify/pass/erdinm/typestates-basic-1.rs → .../verify/pass/erdinm/typestates-basic-1.rs b/.../verify/pass/erdinm/typestates-basic-1.rs → .../verify/pass/erdinm/typestates-basic-1.rs
diff --git a/...pass/expiring-loans/borrow-die-with-if.rs → ...pass/expiring-loans/borrow-die-with-if.rs b/...pass/expiring-loans/borrow-die-with-if.rs → ...pass/expiring-loans/borrow-die-with-if.rs
diff --git a/...s/expiring-loans/borrow-die-with-magic.rs → ...s/expiring-loans/borrow-die-with-magic.rs b/...s/expiring-loans/borrow-die-with-magic.rs → ...s/expiring-loans/borrow-die-with-magic.rs
diff --git a/...s/expiring-loans/borrow-die-with-moves.rs → ...s/expiring-loans/borrow-die-with-moves.rs b/...s/expiring-loans/borrow-die-with-moves.rs → ...s/expiring-loans/borrow-die-with-moves.rs
diff --git a/...verify/pass/expiring-loans/borrow-join.rs → ...verify/pass/expiring-loans/borrow-join.rs b/...verify/pass/expiring-loans/borrow-join.rs → ...verify/pass/expiring-loans/borrow-join.rs
diff --git a/.../verify/pass/expiring-loans/borrow_die.rs → .../verify/pass/expiring-loans/borrow_die.rs b/.../verify/pass/expiring-loans/borrow_die.rs → .../verify/pass/expiring-loans/borrow_die.rs
diff --git a/...ify/pass/expiring-loans/issue-25-simpl.rs → ...ify/pass/expiring-loans/issue-25-simpl.rs b/...ify/pass/expiring-loans/issue-25-simpl.rs → ...ify/pass/expiring-loans/issue-25-simpl.rs
diff --git a/...ify/pass/expiring-loans/pure-fn-loan-2.rs → ...ify/pass/expiring-loans/pure-fn-loan-2.rs b/...ify/pass/expiring-loans/pure-fn-loan-2.rs → ...ify/pass/expiring-loans/pure-fn-loan-2.rs
diff --git a/...erify/pass/expiring-loans/pure-fn-loan.rs → ...erify/pass/expiring-loans/pure-fn-loan.rs b/...erify/pass/expiring-loans/pure-fn-loan.rs → ...erify/pass/expiring-loans/pure-fn-loan.rs
diff --git a/...rify/pass/expiring-loans/return_borrow.rs → ...rify/pass/expiring-loans/return_borrow.rs b/...rify/pass/expiring-loans/return_borrow.rs → ...rify/pass/expiring-loans/return_borrow.rs
diff --git a/...s/expiring-loans/simple-expire-borrows.rs → ...s/expiring-loans/simple-expire-borrows.rs b/...s/expiring-loans/simple-expire-borrows.rs → ...s/expiring-loans/simple-expire-borrows.rs
diff --git a/...ass/expiring-loans/use_returned_borrow.rs → ...ass/expiring-loans/use_returned_borrow.rs b/...ass/expiring-loans/use_returned_borrow.rs → ...ass/expiring-loans/use_returned_borrow.rs
diff --git a/...ts/tests/verify/pass/fold-unfold/basic.rs → ...ti/tests/verify/pass/fold-unfold/basic.rs b/...ts/tests/verify/pass/fold-unfold/basic.rs → ...ti/tests/verify/pass/fold-unfold/basic.rs
diff --git a/...tests/verify/pass/initialization/deref.rs → ...tests/verify/pass/initialization/deref.rs b/...tests/verify/pass/initialization/deref.rs → ...tests/verify/pass/initialization/deref.rs
diff --git a/...alization/deref.rs.reassignment1.def_init → ...alization/deref.rs.reassignment1.def_init b/...alization/deref.rs.reassignment1.def_init → ...alization/deref.rs.reassignment1.def_init
diff --git a/...lization/deref.rs.reassignment2a.def_init → ...lization/deref.rs.reassignment2a.def_init b/...lization/deref.rs.reassignment2a.def_init → ...lization/deref.rs.reassignment2a.def_init
diff --git a/...lization/deref.rs.reassignment2b.def_init → ...lization/deref.rs.reassignment2b.def_init b/...lization/deref.rs.reassignment2b.def_init → ...lization/deref.rs.reassignment2b.def_init
diff --git a/...s/verify/pass/initialization/variables.rs → ...s/verify/pass/initialization/variables.rs b/...s/verify/pass/initialization/variables.rs → ...s/verify/pass/initialization/variables.rs
diff --git a/...itialization/variables.rs._test1.def_init → ...itialization/variables.rs._test1.def_init b/...itialization/variables.rs._test1.def_init → ...itialization/variables.rs._test1.def_init
diff --git a/...s/tests/verify/pass/issues/issue-118-1.rs → ...i/tests/verify/pass/issues/issue-118-1.rs b/...s/tests/verify/pass/issues/issue-118-1.rs → ...i/tests/verify/pass/issues/issue-118-1.rs
diff --git a/...sts/tests/verify/pass/issues/issue-118.rs → prusti/tests/verify/pass/issues/issue-118.rs b/...sts/tests/verify/pass/issues/issue-118.rs → prusti/tests/verify/pass/issues/issue-118.rs
diff --git a/...sts/tests/verify/pass/issues/issue-128.rs → prusti/tests/verify/pass/issues/issue-128.rs b/...sts/tests/verify/pass/issues/issue-128.rs → prusti/tests/verify/pass/issues/issue-128.rs
diff --git a/...sts/tests/verify/pass/issues/issue-133.rs → prusti/tests/verify/pass/issues/issue-133.rs b/...sts/tests/verify/pass/issues/issue-133.rs → prusti/tests/verify/pass/issues/issue-133.rs
diff --git a/...sts/tests/verify/pass/issues/issue-134.rs → prusti/tests/verify/pass/issues/issue-134.rs b/...sts/tests/verify/pass/issues/issue-134.rs → prusti/tests/verify/pass/issues/issue-134.rs
diff --git a/...sts/tests/verify/pass/issues/issue-138.rs → prusti/tests/verify/pass/issues/issue-138.rs b/...sts/tests/verify/pass/issues/issue-138.rs → prusti/tests/verify/pass/issues/issue-138.rs
diff --git a/...sts/tests/verify/pass/issues/issue-144.rs → prusti/tests/verify/pass/issues/issue-144.rs b/...sts/tests/verify/pass/issues/issue-144.rs → prusti/tests/verify/pass/issues/issue-144.rs
diff --git a/...sts/tests/verify/pass/issues/issue-145.rs → prusti/tests/verify/pass/issues/issue-145.rs b/...sts/tests/verify/pass/issues/issue-145.rs → prusti/tests/verify/pass/issues/issue-145.rs
diff --git a/...sts/tests/verify/pass/issues/issue-156.rs → prusti/tests/verify/pass/issues/issue-156.rs b/...sts/tests/verify/pass/issues/issue-156.rs → prusti/tests/verify/pass/issues/issue-156.rs
diff --git a/...sts/tests/verify/pass/issues/issue-170.rs → prusti/tests/verify/pass/issues/issue-170.rs b/...sts/tests/verify/pass/issues/issue-170.rs → prusti/tests/verify/pass/issues/issue-170.rs
diff --git a/...s/tests/verify/pass/issues/issue-187-1.rs → ...i/tests/verify/pass/issues/issue-187-1.rs b/...s/tests/verify/pass/issues/issue-187-1.rs → ...i/tests/verify/pass/issues/issue-187-1.rs
diff --git a/...ests/tests/verify/pass/issues/issue-25.rs → prusti/tests/verify/pass/issues/issue-25.rs b/...ests/tests/verify/pass/issues/issue-25.rs → prusti/tests/verify/pass/issues/issue-25.rs
diff --git a/...ests/tests/verify/pass/issues/issue-34.rs → prusti/tests/verify/pass/issues/issue-34.rs b/...ests/tests/verify/pass/issues/issue-34.rs → prusti/tests/verify/pass/issues/issue-34.rs
diff --git a/...ests/tests/verify/pass/issues/issue-39.rs → prusti/tests/verify/pass/issues/issue-39.rs b/...ests/tests/verify/pass/issues/issue-39.rs → prusti/tests/verify/pass/issues/issue-39.rs
diff --git a/...ests/tests/verify/pass/issues/issue-44.rs → prusti/tests/verify/pass/issues/issue-44.rs b/...ests/tests/verify/pass/issues/issue-44.rs → prusti/tests/verify/pass/issues/issue-44.rs
diff --git a/...s/verify/pass/issues/issue-46-old-expr.rs → ...s/verify/pass/issues/issue-46-old-expr.rs b/...s/verify/pass/issues/issue-46-old-expr.rs → ...s/verify/pass/issues/issue-46-old-expr.rs
diff --git a/...ify/pass/issues/issue-47-extract-simpl.rs → ...ify/pass/issues/issue-47-extract-simpl.rs b/...ify/pass/issues/issue-47-extract-simpl.rs → ...ify/pass/issues/issue-47-extract-simpl.rs
diff --git a/...ts/verify/pass/issues/issue-47-extract.rs → ...ts/verify/pass/issues/issue-47-extract.rs b/...ts/verify/pass/issues/issue-47-extract.rs → ...ts/verify/pass/issues/issue-47-extract.rs
diff --git a/...s/verify/pass/issues/issue-47-move-ref.rs → ...s/verify/pass/issues/issue-47-move-ref.rs b/...s/verify/pass/issues/issue-47-move-ref.rs → ...s/verify/pass/issues/issue-47-move-ref.rs
diff --git a/...erify/pass/issues/issue-47-replace-arg.rs → ...erify/pass/issues/issue-47-replace-arg.rs b/...erify/pass/issues/issue-47-replace-arg.rs → ...erify/pass/issues/issue-47-replace-arg.rs
diff --git a/...rify/pass/issues/issue-47-replace-self.rs → ...rify/pass/issues/issue-47-replace-self.rs b/...rify/pass/issues/issue-47-replace-self.rs → ...rify/pass/issues/issue-47-replace-self.rs
diff --git a/...ests/tests/verify/pass/issues/issue-61.rs → prusti/tests/verify/pass/issues/issue-61.rs b/...ests/tests/verify/pass/issues/issue-61.rs → prusti/tests/verify/pass/issues/issue-61.rs
diff --git a/...ests/tests/verify/pass/issues/issue-75.rs → prusti/tests/verify/pass/issues/issue-75.rs b/...ests/tests/verify/pass/issues/issue-75.rs → prusti/tests/verify/pass/issues/issue-75.rs
diff --git a/...ests/tests/verify/pass/issues/issue-85.rs → prusti/tests/verify/pass/issues/issue-85.rs b/...ests/tests/verify/pass/issues/issue-85.rs → prusti/tests/verify/pass/issues/issue-85.rs
diff --git a/...ests/tests/verify/pass/issues/issue-98.rs → prusti/tests/verify/pass/issues/issue-98.rs b/...ests/tests/verify/pass/issues/issue-98.rs → prusti/tests/verify/pass/issues/issue-98.rs
diff --git a/...s/tests/verify/pass/larger/first-final.rs → ...i/tests/verify/pass/larger/first-final.rs b/...s/tests/verify/pass/larger/first-final.rs → ...i/tests/verify/pass/larger/first-final.rs
diff --git a/...-tests/tests/verify/pass/loop-invs/fib.rs → prusti/tests/verify/pass/loop-invs/fib.rs b/...-tests/tests/verify/pass/loop-invs/fib.rs → prusti/tests/verify/pass/loop-invs/fib.rs
diff --git a/...ts/tests/verify/pass/loop-invs/if-loop.rs → ...ti/tests/verify/pass/loop-invs/if-loop.rs b/...ts/tests/verify/pass/loop-invs/if-loop.rs → ...ti/tests/verify/pass/loop-invs/if-loop.rs
diff --git a/...ests/verify/pass/loop-invs/loop-fields.rs → ...ests/verify/pass/loop-invs/loop-fields.rs b/...ests/verify/pass/loop-invs/loop-fields.rs → ...ests/verify/pass/loop-invs/loop-fields.rs
diff --git a/...s/verify/pass/loop-invs/nested-loops-2.rs → ...s/verify/pass/loop-invs/nested-loops-2.rs b/...s/verify/pass/loop-invs/nested-loops-2.rs → ...s/verify/pass/loop-invs/nested-loops-2.rs
diff --git a/...s/verify/pass/loop-invs/nested-loops-3.rs → ...s/verify/pass/loop-invs/nested-loops-3.rs b/...s/verify/pass/loop-invs/nested-loops-3.rs → ...s/verify/pass/loop-invs/nested-loops-3.rs
diff --git a/...tests/verify/pass/loop-invs/simple-inv.rs → ...tests/verify/pass/loop-invs/simple-inv.rs b/...tests/verify/pass/loop-invs/simple-inv.rs → ...tests/verify/pass/loop-invs/simple-inv.rs
diff --git a/...ests/verify/pass/loop-invs/simple-loop.rs → ...ests/verify/pass/loop-invs/simple-loop.rs b/...ests/verify/pass/loop-invs/simple-loop.rs → ...ests/verify/pass/loop-invs/simple-loop.rs
diff --git a/...ts/verify/pass/loop-invs/simple-nested.rs → ...ts/verify/pass/loop-invs/simple-nested.rs b/...ts/verify/pass/loop-invs/simple-nested.rs → ...ts/verify/pass/loop-invs/simple-nested.rs
diff --git a/...ests/verify/pass/loop-invs/sum-framing.rs → ...ests/verify/pass/loop-invs/sum-framing.rs b/...ests/verify/pass/loop-invs/sum-framing.rs → ...ests/verify/pass/loop-invs/sum-framing.rs
diff --git a/...-tests/tests/verify/pass/loop-invs/sum.rs → prusti/tests/verify/pass/loop-invs/sum.rs b/...-tests/tests/verify/pass/loop-invs/sum.rs → prusti/tests/verify/pass/loop-invs/sum.rs
diff --git a/.../verify/pass/magic-wands/wand-identity.rs → .../verify/pass/magic-wands/wand-identity.rs b/.../verify/pass/magic-wands/wand-identity.rs → .../verify/pass/magic-wands/wand-identity.rs
diff --git a/...verify/pass/magic-wands/wand-identity2.rs → ...verify/pass/magic-wands/wand-identity2.rs b/...verify/pass/magic-wands/wand-identity2.rs → ...verify/pass/magic-wands/wand-identity2.rs
diff --git a/...verify/pass/magic-wands/wand-identity3.rs → ...verify/pass/magic-wands/wand-identity3.rs b/...verify/pass/magic-wands/wand-identity3.rs → ...verify/pass/magic-wands/wand-identity3.rs
diff --git a/...ti-tests/tests/verify/pass/moves/basic.rs → prusti/tests/verify/pass/moves/basic.rs b/...ti-tests/tests/verify/pass/moves/basic.rs → prusti/tests/verify/pass/moves/basic.rs
diff --git a/...erify/pass/mut-borrows/basic-reborrows.rs → ...erify/pass/mut-borrows/basic-reborrows.rs b/...erify/pass/mut-borrows/basic-reborrows.rs → ...erify/pass/mut-borrows/basic-reborrows.rs
diff --git a/...ts/tests/verify/pass/mut-borrows/basic.rs → ...ti/tests/verify/pass/mut-borrows/basic.rs b/...ts/tests/verify/pass/mut-borrows/basic.rs → ...ti/tests/verify/pass/mut-borrows/basic.rs
diff --git a/.../verify/pass/mut-borrows/binary_search.rs → .../verify/pass/mut-borrows/binary_search.rs b/.../verify/pass/mut-borrows/binary_search.rs → .../verify/pass/mut-borrows/binary_search.rs
diff --git a/...tests/verify/pass/mut-borrows/drop-dag.rs → ...tests/verify/pass/mut-borrows/drop-dag.rs b/...tests/verify/pass/mut-borrows/drop-dag.rs → ...tests/verify/pass/mut-borrows/drop-dag.rs
diff --git a/...sts/tests/verify/pass/mut-borrows/drop.rs → prusti/tests/verify/pass/mut-borrows/drop.rs b/...sts/tests/verify/pass/mut-borrows/drop.rs → prusti/tests/verify/pass/mut-borrows/drop.rs
diff --git a/...s/verify/pass/mut-borrows/empty-method.rs → ...s/verify/pass/mut-borrows/empty-method.rs b/...s/verify/pass/mut-borrows/empty-method.rs → ...s/verify/pass/mut-borrows/empty-method.rs
diff --git a/...ify/pass/mut-borrows/generic-reborrows.rs → ...ify/pass/mut-borrows/generic-reborrows.rs b/...ify/pass/mut-borrows/generic-reborrows.rs → ...ify/pass/mut-borrows/generic-reborrows.rs
diff --git a/...sts/tests/verify/pass/mut-borrows/move.rs → prusti/tests/verify/pass/mut-borrows/move.rs b/...sts/tests/verify/pass/mut-borrows/move.rs → prusti/tests/verify/pass/mut-borrows/move.rs
diff --git a/...erify/pass/mut-borrows/num-traits-mult.rs → ...erify/pass/mut-borrows/num-traits-mult.rs b/...erify/pass/mut-borrows/num-traits-mult.rs → ...erify/pass/mut-borrows/num-traits-mult.rs
diff --git a/.../tests/verify/pass/mut-borrows/ref-arg.rs → .../tests/verify/pass/mut-borrows/ref-arg.rs b/.../tests/verify/pass/mut-borrows/ref-arg.rs → .../tests/verify/pass/mut-borrows/ref-arg.rs
diff --git a/.../tests/verify/pass/mut-borrows/restore.rs → .../tests/verify/pass/mut-borrows/restore.rs b/.../tests/verify/pass/mut-borrows/restore.rs → .../tests/verify/pass/mut-borrows/restore.rs
diff --git a/...ts/tests/verify/pass/mut-borrows/tuple.rs → ...ti/tests/verify/pass/mut-borrows/tuple.rs b/...ts/tests/verify/pass/mut-borrows/tuple.rs → ...ti/tests/verify/pass/mut-borrows/tuple.rs
diff --git a/...tests/verify/pass/nll-rfc/borrow_first.rs → ...tests/verify/pass/nll-rfc/borrow_first.rs b/...tests/verify/pass/nll-rfc/borrow_first.rs → ...tests/verify/pass/nll-rfc/borrow_first.rs