diff --git a/notebooks/experiments/SMT_Translation_Experiments.ipynb b/notebooks/experiments/SMT_Translation_Experiments.ipynb
new file mode 100644
index 0000000000000000000000000000000000000000..40c0aa6bc85c32ec9b846c521aa07f0a027d0c4a
--- /dev/null
+++ b/notebooks/experiments/SMT_Translation_Experiments.ipynb
@@ -0,0 +1,197 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "# Experiments in SMTLib Translation #\n",
+ "\n",
+ "Let us look at a simple example that poses problems for the Z3/CVC4 backend:"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "metadata": {},
+ "outputs": [
+ {
+ "ename": "CommandExecutionException",
+ "evalue": ":solve: Computation not completed: no solution found (but one might exist)",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[31m:solve: Computation not completed: no solution found (but one might exist)\u001b[0m"
+ ]
+ }
+ ],
+ "source": [
+ ":solve z3 f = {1|->3, 2|->6} & r = f~[{6}]"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "To understand why this simple constraint cannot be solved, we have to know how the translation works:\n",
+ "The relational inverse gets translated into two universal quantifications for SMTLib:\n",
+ "```\n",
+ " x = y~\n",
+ "<=>\n",
+ " !(st11,st12).(st11 |-> st12 : x => st12 |-> st11 : y) & \n",
+ " !(st11,st12).(st12 |-> st11 : y => st11 |-> st12 : x))\n",
+ "```\n",
+ "Similarly, r = f[s] is translated as follows:\n",
+ "```\n",
+ " r = f[s]\n",
+ "<=>\n",
+ " !st27.(st27 : r => #st26.(st26 |-> st27 : f & st26 : s) & \n",
+ " !st27.(#st26.(st26 |-> st27 : f & st26 : s) => st27 : r)\n",
+ "```\n",
+ "The resulting predicate (without the inverse and image operators) is the following, which Z3 cannot solve (but ProB can)."
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/latex": [
+ "$\\mathit{f} = \\{(1\\mapsto 3),(2\\mapsto 6)\\} \\wedge (\\exists /* LET */ (\\mathit{st13}).( (\\mathit{st13})=\\mathit{r} \\wedge \\forall \\mathit{st15}\\cdot (\\mathit{st15} \\in \\mathit{st13} \\mathbin\\Rightarrow \\exists \\mathit{st16}\\cdot (6 \\mapsto \\mathit{st15} \\in \\mathit{st16} \\wedge (\\forall (\\mathit{st17},\\mathit{st18})\\cdot (\\mathit{st17} \\mapsto \\mathit{st18} \\in \\mathit{st16} \\mathbin\\Rightarrow \\mathit{st18} \\mapsto \\mathit{st17} \\in \\mathit{f}) \\wedge \\forall (\\mathit{st17},\\mathit{st18})\\cdot (\\mathit{st18} \\mapsto \\mathit{st17} \\in \\mathit{f} \\mathbin\\Rightarrow \\mathit{st17} \\mapsto \\mathit{st18} \\in \\mathit{st16})))) \\wedge \\forall \\mathit{st15}\\cdot (\\exists \\mathit{st19}\\cdot (6 \\mapsto \\mathit{st15} \\in \\mathit{st19} \\wedge (\\forall (\\mathit{st20},\\mathit{st21})\\cdot (\\mathit{st20} \\mapsto \\mathit{st21} \\in \\mathit{st19} \\mathbin\\Rightarrow \\mathit{st21} \\mapsto \\mathit{st20} \\in \\mathit{f}) \\wedge \\forall (\\mathit{st20},\\mathit{st21})\\cdot (\\mathit{st21} \\mapsto \\mathit{st20} \\in \\mathit{f} \\mathbin\\Rightarrow \\mathit{st20} \\mapsto \\mathit{st21} \\in \\mathit{st19}))) \\mathbin\\Rightarrow \\mathit{st15} \\in \\mathit{st13})))$"
+ ],
+ "text/plain": [
+ "f = {(1↦3),(2↦6)} ∧ (∃ /* LET */ (st13).( (st13)=r ∧ ∀st15·(st15 ∈ st13 ⇒ ∃st16·(6 ↦ st15 ∈ st16 ∧ (∀(st17,st18)·(st17 ↦ st18 ∈ st16 ⇒ st18 ↦ st17 ∈ f) ∧ ∀(st17,st18)·(st18 ↦ st17 ∈ f ⇒ st17 ↦ st18 ∈ st16)))) ∧ ∀st15·(∃st19·(6 ↦ st15 ∈ st19 ∧ (∀(st20,st21)·(st20 ↦ st21 ∈ st19 ⇒ st21 ↦ st20 ∈ f) ∧ ∀(st20,st21)·(st21 ↦ st20 ∈ f ⇒ st20 ↦ st21 ∈ st19))) ⇒ st15 ∈ st13)))"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":prettyprint f = {(1|->3),(2|->6)} &\n",
+ "#st13.(r = st13 & (\n",
+ " !st15.(st15 : st13 => #st14.(#st16.(st14 |-> st15 : st16 & \n",
+ " (!(st17,st18).(st17 |-> st18 : st16 => st18 |-> st17 : f) & \n",
+ " !(st17,st18).(st18 |-> st17 : f => st17 |-> st18 : st16))) & st14 : {6})) & \n",
+ " !st15.(#st14.(#st19.(st14 |-> st15 : st19 & (!(st20,st21).(st20 |-> st21 : st19 => st21 |-> st20 : f) &\n",
+ " !(st20,st21).(st21 |-> st20 : f => st20 |-> st21 : st19))) & st14 : {6}) => st15 : st13)))"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "Execution time: 0.194111316 seconds"
+ ],
+ "text/plain": [
+ "Execution time: 0.194111316 seconds"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ },
+ {
+ "data": {
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\tr = {2}\n",
+ "\tf = {(1↦3),(2↦6)}"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":time :solve prob f = {(1|->3),(2|->6)} &\n",
+ "#st13.(r = st13 & (\n",
+ " !st15.(st15 : st13 => #st14.(#st16.(st14 |-> st15 : st16 & \n",
+ " (!(st17,st18).(st17 |-> st18 : st16 => st18 |-> st17 : f) & \n",
+ " !(st17,st18).(st18 |-> st17 : f => st17 |-> st18 : st16))) & st14 : {6})) & \n",
+ " !st15.(#st14.(#st19.(st14 |-> st15 : st19 & (!(st20,st21).(st20 |-> st21 : st19 => st21 |-> st20 : f) &\n",
+ " !(st20,st21).(st21 |-> st20 : f => st20 |-> st21 : st19))) & st14 : {6}) => st15 : st13)))\n",
+ "\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "metadata": {},
+ "source": [
+ "Experiment in Rodin: adding r={2} as theorem and use SMT Plugin using the technique suggested by Laurent:\n",
+ "\n",
+ "pour voir la traduction d’Event-B vers SMT, créer un fichier texte contenant\n",
+ "```\n",
+ " org.eventb.smt.core/debug = true\n",
+ " org.eventb.smt.core/debug/translator = true\n",
+ " org.eventb.smt.core/debug/translator_details = true\n",
+ "```\n",
+ "et lancer Rodin avec les paramètres `-debug <text-file>`.\n",
+ "\n",
+ "À chaque fois qu’un solveur SMT est lancé, le contenu du fichier SMT sera affiché dans la console.\n",
+ "\n",
+ "```\n",
+ "; translated from Event-B with the PP approach of Rodin SMT Plugin\n",
+ "\n",
+ "(set-info :status unsat)\n",
+ "(set-logic AUFLIA)\n",
+ "(declare-fun f (Int Int) Bool)\n",
+ "(declare-fun r (Int) Bool)\n",
+ "\n",
+ "(assert (and \n",
+ " (forall ((x Int) (x0 Int)) \n",
+ " (= \n",
+ " (f x x0) \n",
+ " (or \n",
+ " (and \n",
+ " (= x 1) \n",
+ " (= x0 3)) \n",
+ " (and \n",
+ " (= x 2) \n",
+ " (= x0 6))))) \n",
+ " (forall ((x1 Int)) \n",
+ " (= \n",
+ " (r x1) \n",
+ " (exists ((x2 Int)) \n",
+ " (and \n",
+ " (= x2 6) \n",
+ " (f x1 x2)))))))\n",
+ "(assert (not \n",
+ " (forall ((x3 Int)) \n",
+ " (= \n",
+ " (r x3) \n",
+ " (= x3 2)))))\n",
+ "(check-sat)\n",
+ "```"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": []
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "ProB 2",
+ "language": "prob",
+ "name": "prob2"
+ },
+ "language_info": {
+ "file_extension": ".prob",
+ "mimetype": "text/x-prob",
+ "name": "prob"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}