diff --git a/assets/glossary.tex b/assets/glossary.tex
index 32c25cb..7c4b609 100644
--- a/assets/glossary.tex
+++ b/assets/glossary.tex
@@ -238,7 +238,7 @@
 }
 
 \newglossaryentry{flatzinc}{
-  name={Flat\-Zinc},{}
+  name={Flat\-Zinc},
   description={A subset of \gls{minizinc} chosen to represent \glspl{slv-mod}. It is the standard format in which \gls{minizinc} communicates with its \glspl{solver}},
 }
 
diff --git a/chapters/1_introduction.tex b/chapters/1_introduction.tex
index d2a48ec..1d0043a 100644
--- a/chapters/1_introduction.tex
+++ b/chapters/1_introduction.tex
@@ -60,7 +60,7 @@ Finally, \lrefrange{line:intro:con:start}{line:intro:con:end} express the \const
 
 \begin{listing}
 	\amplfile{assets/listing/intro_open_shop.mod}
-	\caption{\label{lst:intro-open-shop} An \glsxtrshort{ampl} model of the open shop problem}
+	\caption{\label{lst:intro-open-shop} An \glsxtrshort{ampl} model of the open shop problem.}
 \end{listing}
 
 The \glsxtrshort{ampl} model provides a clear definition of the problem class, but it can be argued that its meaning is hard to decipher.
diff --git a/chapters/2_background.tex b/chapters/2_background.tex
index 4259091..b299f6f 100644
--- a/chapters/2_background.tex
+++ b/chapters/2_background.tex
@@ -102,7 +102,7 @@ Its expressive language and extensive library of \glspl{global} allow users to e
 
 \begin{listing}
 	\mznfile{assets/listing/back_knapsack.mzn}
-	\caption{\label{lst:back-mzn-knapsack} A \minizinc{} model describing a 0-1 knapsack problem}
+	\caption{\label{lst:back-mzn-knapsack} A \minizinc{} model describing a 0-1 knapsack problem.}
 \end{listing}
 
 Note that, although more textual and explicit, the \minizinc{} model definition is very similar to our earlier mathematical definition.
@@ -906,7 +906,7 @@ Different types of \solvers{} can also have access to different types of \constr
 
 	\begin{listing}
 		\mznfile{assets/listing/back_tsp.mzn}
-		\caption{\label{lst:back-mzn-tsp} An \minizinc{} model describing the \gls{tsp}}
+		\caption{\label{lst:back-mzn-tsp} An \minizinc{} model describing the \gls{tsp}.}
 	\end{listing}
 
 	A \minizinc{} model for the same problem is shown in \cref{lst:back-mzn-tsp}.
@@ -1276,8 +1276,7 @@ For instance, this replaces enumerated types by normal integers.
 \begin{figure}
 	\centering
 	\includegraphics[width=\linewidth]{assets/img/back_compilation_structure}
-	\caption{\label{fig:back-mzn-comp} The compilation structure of the \minizinc\
-		compiler.}
+	\caption{\label{fig:back-mzn-comp} The compilation structure of the \minizinc \compiler{}.}
 \end{figure}
 
 The middle-end contains the most important two processes: \gls{rewriting} and optimization.
diff --git a/chapters/3_rewriting.tex b/chapters/3_rewriting.tex
index 7e91ef7..c762b58 100644
--- a/chapters/3_rewriting.tex
+++ b/chapters/3_rewriting.tex
@@ -32,7 +32,7 @@ The process can even be made incremental: in \cref{ch:incremental} we discuss ho
 \begin{figure}
 	\centering
 	\includegraphics[width=\linewidth]{assets/img/rew_compilation_structure}
-	\caption{\label{fig:rew-comp} The proposed process for the compilation of	\minizinc{} instances.}
+	\caption{\label{fig:rew-comp} The proposed process for the compilation of \minizinc{} instances.}
 \end{figure}
 
 The process of the new architecture is shown in \cref{fig:rew-comp}.
@@ -339,8 +339,7 @@ Although pure \microzinc{} behaves the same under any call evaluation strategy,
 		\infer1[(CallNative)]{\Sem{F(\(a_1, \ldots, a_k\))}{\Prog, \Env} \Rightarrow{}
 			\tuple{\ensuremath{\texttt{constraint}~\ptinline{F}(a_1, \ldots, a_k), \Env}}}
 	\end{prooftree}
-	\caption{\label{fig:rew-rewrite-to-nzn-calls} Rewriting rules for partial evaluation
-		of \microzinc{} calls to \nanozinc{}.}
+	\caption{\label{fig:rew-rewrite-to-nzn-calls} Rewriting rules for partial evaluation of \microzinc{} calls to \nanozinc{}.}
 \end{figure*}
 
 The rules in \cref{fig:rew-rewrite-to-nzn-calls} handle function calls.
@@ -393,8 +392,7 @@ Since these are directly supported by the \solver{}, they simply need to be tran
 		\infer[no rule]1{\Sem{\(\mathbf{I}_{[x_{i} \mapsto v_{\langle{}i\rangle}, \forall{} 1 \leq{} i \leq{} k]} \mid{} \mathbf{X}_{[x_{i} \mapsto v_{\langle{}i\rangle}, \forall{} 1 \leq{} i \leq{} k]}\)}{\Prog, \Env', \Ctx} \Rightarrow{} \tuple{x, \Env''}}
 		\infer1[(ItemTupD)]{\Sem{\(\left(t_{1}\texttt{:}~x_{1}, \ldots, t_{k}\texttt{:}~x_{k}\right) = E\texttt{;} \mathbf{I} \mid{} \mathbf{X}\)}{\Prog, \Env, \Ctx} \Rightarrow{} \tuple{x, \Env''}}
 	\end{prooftree}
-	\caption{\label{fig:rew-rewrite-to-nzn-let} Rewriting rules for partial evaluation
-		of \microzinc{} \glspl{let} to \nanozinc{}.}
+	\caption{\label{fig:rew-rewrite-to-nzn-let} Rewriting rules for partial evaluation of \microzinc{} \glspl{let} to \nanozinc{}.}
 \end{figure*}
 
 The rules in \cref{fig:rew-rewrite-to-nzn-let} consider \glspl{let}.
@@ -453,8 +451,7 @@ We use the notation \(x_{\langle{}i\rangle}\) to mark the \(i^{\text{th}}\) memb
 		\infer1[(ListG)]{\Sem{\([E~|~ x \mbox{~in~} \mathit{PE}, \mathit{GE} \mbox{~where~} G]\)}{\Prog, \Env} \Rightarrow{}
 		\tuple{\mbox{concat} [ A_v~|~v \in{} S ], \Env{} \cup{} \bigcup{}_{v \in{} S} \Env{}_{v}}}
 	\end{prooftree}
-	\caption{\label{fig:rew-rewrite-to-nzn-other} Rewriting rules for partial evaluation
-		of other \microzinc{} expressions to \nanozinc{}.}
+	\caption{\label{fig:rew-rewrite-to-nzn-other} Rewriting rules for partial evaluation of other \microzinc{} expressions to \nanozinc{}.}
 \end{figure*}
 
 Finally, the rules in \cref{fig:rew-rewrite-to-nzn-other} handle the evaluation of \variables{}, constants, \glspl{conditional} and \glspl{comprehension}.
@@ -821,9 +818,7 @@ These are very encouraging results, given that we are comparing a largely unopti
 		\includegraphics[width=\columnwidth]{assets/img/rew_compare_memory}
 		\caption{\label{sfig:rew-comparemem}Maximum resident set size (kbytes)}
 	\end{subfigure}
-	\caption{\label{fig:4-runtime}Performance on \gls{rewriting} MiniZinc Challenge
-		\instances{}. \minizinc{} 2.5.5 (x-axis) vs new architecture (y-axis), log-log
-		plot. Dots below the line indicate the new system is better.}
+	\caption{\label{fig:4-runtime}Performance on \gls{rewriting} \minizinc{} Challenge \instances{}. \minizinc{} 2.5.5 (x-axis) vs our prototype (y-axis), log-log plot. Dots below the line indicate the new system is better.}
 \end{figure}
 
 Our second experiment considers three well-known computational recursive functions: Ackermann, Fibonacci, and Takeuchi.
diff --git a/chapters/4_half_reif.tex b/chapters/4_half_reif.tex
index 16fbbd6..133db6e 100644
--- a/chapters/4_half_reif.tex
+++ b/chapters/4_half_reif.tex
@@ -434,7 +434,7 @@ The behaviour of these transformations is shown in \cref{fig:half-ctx-trans}.
 		\hypo{\ctxeval{\texttt{[}e_{1}, \ldots, e_{n}\texttt{]}}{ctx}}
 		\infer1[(Arr)]{\ctxeval{e_{1}}{ctx}, \ldots, \ctxeval{e_{n}}{ctx}}
 	\end{prooftree}
-	\caption{\label{fig:half-analysis-expr} Context inference rules for \microzinc\ expressions.}
+	\caption{\label{fig:half-analysis-expr} Context inference rules for \microzinc{} expressions.}
 \end{figure*}
 
 \Cref{fig:half-analysis-expr} shows the inference rules for all \microzinc{} expressions, apart from \glspl{let}.
@@ -494,7 +494,7 @@ However, we currently do not provide such analysis and annotate functions by han
 			\Return{\tuple{\mixc, \ldots, \mixc}}
 		}
 	}
-	\caption{\label{alg:arg-ctx} Definition of the ``argCtx'' function for \minizinc\ operators.}
+	\caption{\label{alg:arg-ctx} Definition of the ``argCtx'' function for \minizinc{} operators.}
 \end{algorithm}
 
 The context in which the result of a call expression is used must also be considered.
@@ -568,7 +568,7 @@ If such an expression is evaluated in the context \(ctx\), then its members can
 		\hypo{\ctxitem{\epsilon{}}}
 		\infer1[(Item0)]{}
 	\end{prooftree}
-	\caption{\label{fig:half-analysis-it} Context inference rules for \microzinc\ let-expressions.}
+	\caption{\label{fig:half-analysis-it} Context inference rules for \microzinc{} let-expressions.}
 \end{figure*}
 
 \Cref{fig:half-analysis-it} shows the inference rules for \glspl{let} and their inner items.
@@ -814,7 +814,7 @@ The goal of the algorithm is now to identify and remove vertices that are not ma
 		}
 	}
 	\(G' \longleftarrow \tuple{V', E'}\)\;
-	\caption{\label{alg:half-compression} implication \gls{chain-compression} algorithm}
+	\caption{\label{alg:half-compression} implication \gls{chain-compression} algorithm.}
 \end{algorithm}
 
 The algorithm can be further improved by considering implied conjunctions.
@@ -872,6 +872,60 @@ All usages of the previously recorded \gls{cvar} are replaced by the new result.
 The dependency tracking, through the use of \constraints{} attached to \variables{}, ensures that all defining \constraints{} are removed from the model.
 This ensures that all \variables{} and \constraints{} created for the earlier version are correctly removed.
 
+\begin{example}
+
+	Consider, for example, the following \minizinc{} fragment, which uses the linearization of \mzninline{int_le}.
+
+	\begin{mzn}
+		predicate int_le_imp(var int: x, int: y, var bool: b) =
+			x <= ub(x) - (ub(x) - y) * b;
+			
+		predicate int_le_reif(var int: x, int: y, var bool: b) =
+			x <= ub(x) - (ub(x) - y) * b /\ x >= (y + 1) - (y + 1) * b;
+
+		var 1..10: i;
+		constraint j \/ int_le(i, 4);
+		constraint k xor int_le(i, 4);
+	\end{mzn}
+
+	In this fragment the call \mzninline{int_le(i, 4)} occurs both in \posc{} and \mixc{} context.
+	Although, in this case, the \compiler{} is able to hoist the expression to share it between the two \constraint{}, as discussed in \cref{sec:rew-cse}, the same expressions might result from function \gls{rewriting} were this is not possible.
+	After \gls{rewriting} the first \constraint{}, the \nanozinc{} program would contain the following definitions.
+
+	\begin{nzn}
+		var bool: b1;
+		↳ constraint int_lin_le([1, 6], [i, b1], 10);
+		constraint bool_clause([j, b1], []);
+	\end{nzn}
+
+	In this program \mzninline{b1} is the \gls{cvar} of the \gls{half-reif} of the \mzninline{int_le(i, 4)} call.
+	The \gls{cvar} is added to the \gls{cse} table as the result of the call.
+	However, since the second call is in \mixc{} context, it cannot use the \gls{half-reif}, and must create the \gls{reif} instead.
+	This results in the following \nanozinc{} program.
+
+	\begin{nzn}
+		var bool: b1;
+		↳ constraint int_lin_le([1, 6], [i, b1], 10);
+		constraint bool_clause([j, b1], []);
+		var bool: b2;
+		↳ constraint int_lin_le([1, 6], [i, b2], 10);
+		↳ constraint int_lin_le([-1, -5], [i, b2], -5);
+		constraint bool_not(k, b2);
+	\end{nzn}
+
+	Now when \mzninline{b2} is added to the \gls{cse} table as the \gls{cvar} of the \gls{reif} of the \mzninline{int_le(i, 4)} call, it notices that there is already a result in table for the same call in a weaker context.
+	As such, it replaces all occurrences of the \gls{cvar} of the \gls{half-reif}, found in the table, with the \gls{cvar} of the \gls{reif}.
+	Once all usage of the \gls{cvar} have been removed, it and its dependent \constraints{} are removed, resulting in the following \nanozinc{} program.
+
+	\begin{nzn}
+		constraint bool_clause([j, b2], []);
+		var bool: b2;
+		↳ constraint int_lin_le([1, 6], [i, b2], 10);
+		↳ constraint int_lin_le([-1, -5], [i, b2], -5);
+		constraint bool_not(k, b2);
+	\end{nzn}
+\end{example}
+
 Because the expression itself is changed when a negation is moved inwards, it may not always be clear when the same expression is used in both \posc{} and \negc{} context.
 This problem is solved by introducing a canonical form for expressions where negations can be pushed inwards.
 In this form the result of \gls{rewriting} an expression and its negation are collected in the same place within the \gls{cse} table.
diff --git a/chapters/5_incremental.tex b/chapters/5_incremental.tex
index c799275..8c56bcd 100644
--- a/chapters/5_incremental.tex
+++ b/chapters/5_incremental.tex
@@ -36,12 +36,12 @@ For example, \mzninline{uniform_neighbourhood(x, 0.2)} would result in each vari
 
 \begin{listing}
 	\mznfile{assets/listing/inc_lns_minisearch_pred.mzn}
-	\caption{\label{lst:inc-lns-minisearch-pred} A simple random \gls{lns} predicate implemented in \minisearch{}}
+	\caption{\label{lst:inc-lns-minisearch-pred} A simple random \gls{lns} predicate implemented in \minisearch{}.}
 \end{listing}
 
 \begin{listing}
 	\mznfile{assets/listing/inc_lns_minisearch.mzn}
-	\caption{\label{lst:inc-lns-minisearch} A simple \gls{lns} \gls{meta-optimization} implemented in \minisearch{}}
+	\caption{\label{lst:inc-lns-minisearch} A simple \gls{lns} \gls{meta-optimization} implemented in \minisearch{}.}
 \end{listing}
 
 The second part of a \minisearch{} \gls{meta-optimization} is the \gls{meta-optimization} algorithm itself.
@@ -97,8 +97,7 @@ Finally, the \mzninline{restart_limit} stops the search after a fixed number of
 
 \begin{listing}
 	\mznfile{assets/listing/inc_restart_ann.mzn}
-	\caption{\label{lst:inc-restart-ann} New annotations to control the restarting
-		behaviour}
+	\caption{\label{lst:inc-restart-ann} New annotations to control the restarting behaviour.}
 \end{listing}
 
 \subsection{Advanced Meta-Optimisation Algorithms}
@@ -136,7 +135,7 @@ Like \mzninline{sol}, it has versions for all basic \variable{} types.
 
 \begin{listing}
 	\mznfile{assets/listing/inc_state_access.mzn}
-	\caption{\label{lst:inc-state-access} Functions for accessing previous \solver{} states}
+	\caption{\label{lst:inc-state-access} Functions for accessing previous \solver{} states.}
 \end{listing}
 
 In order to be able to initialize the \variables{} used for state access, we interpret \mzninline{on_restart} also before initial search using the same semantics.
@@ -166,7 +165,7 @@ Therefore, users have to define their overall strategy in a new predicate.
 
 \begin{listing}
 	\mznfile{assets/listing/inc_basic_complete.mzn}
-	\caption{\label{lst:inc-basic-complete} Complete \gls{lns} example}
+	\caption{\label{lst:inc-basic-complete} A complete \gls{lns} example.}
 \end{listing}
 
 We can also define round-robin and adaptive strategies using these primitives.
@@ -178,8 +177,7 @@ This will activate a different \gls{neighbourhood} for each subsequent \gls{rest
 
 \begin{listing}
 	\mznfile{assets/listing/inc_round_robin.mzn}
-	\caption{\label{lst:inc-round-robin} A predicate providing the round-robin
-		meta-heuristic}
+	\caption{\label{lst:inc-round-robin} A predicate providing the round-robin meta-heuristic.}
 \end{listing}
 
 %\paragraph{Adaptive \gls{lns}}
@@ -189,7 +187,7 @@ For adaptive \gls{lns}, a simple strategy is to change the size of the \gls{neig
 
 \begin{listing}
 	\mznfile{assets/listing/inc_adaptive.mzn}
-	\caption{\label{lst:inc-adaptive} A simple adaptive neighbourhood}
+	\caption{\label{lst:inc-adaptive} A simple adaptive neighbourhood.}
 \end{listing}
 
 \subsection{Optimization strategies}
@@ -314,7 +312,7 @@ It simply replaces the functional form by a predicate \mzninline{status} (declar
 
 \begin{listing}
 	\mznfile{assets/listing/inc_status.mzn}
-	\caption{\label{lst:inc-status} MiniZinc definition of the \mzninline{status} function}
+	\caption{\label{lst:inc-status} MiniZinc definition of the \mzninline{status} function.}
 \end{listing}
 
 \paragraph{\mzninline{sol} and \mzninline{last_val}}
@@ -329,8 +327,7 @@ We use the current \domain{} of the \variable{}, \mzninline{dom(x)}, as the \dom
 
 \begin{listing}
 	\mznfile{assets/listing/inc_sol_function.mzn}
-	\caption{\label{lst:inc-int-sol} MiniZinc definition of the \mzninline{sol}
-		function for integer variables}
+	\caption{\label{lst:inc-int-sol} MiniZinc definition of the \mzninline{sol} function for integer \variables{}.}
 \end{listing}
 
 The compilation of \mzninline{last_val} is similar to that for \mzninline{sol}.
@@ -345,8 +342,7 @@ As such, it can be used in combination with other functions, such as \mzninline{
 
 \begin{listing}
 	\mznfile{assets/listing/inc_uniform_slv.mzn}
-	\caption{\label{lst:inc-int-rnd} MiniZinc definition of the
-		\mzninline{uniform_nbh} function for floats}
+	\caption{\label{lst:inc-int-rnd} MiniZinc definition of the floating point \mzninline{uniform_nbh} function.}
 \end{listing}
 
 \paragraph{\mzninline{complete}}
@@ -418,7 +414,7 @@ Note that the \flatzinc{} \gls{slv-mod} shown here has been simplified for prese
 
 \begin{listing}
 	\mznfile{assets/listing/inc_basic_complete_transformed.mzn}
-	\caption{\label{lst:inc-flat-pred} \flatzinc{} that results from compiling \\
+	\caption{\label{lst:inc-flat-pred} The \flatzinc{} \gls{slv-mod} that results from \gls{rewriting} \\
 		\mzninline{basic_lns(uniformNeighbourhood(x,0.2))}.}
 \end{listing}
 
@@ -636,8 +632,7 @@ These orders can then be freely reassigned to any other slab.
 
 \begin{listing}
 	\mznfile{assets/listing/inc_steelmillslab_neighbourhood.mzn}
-	\caption{\label{lst:inc-free-bin}Steel mill slab: \gls{neighbourhood} that frees
-		all orders assigned to a selected slab.}
+	\caption{\label{lst:inc-free-bin}Steel mill slab: \gls{neighbourhood} that frees all orders assigned to a selected slab.}
 \end{listing}
 
 
diff --git a/chapters/A2_benchmark.tex b/chapters/A2_benchmark.tex
index b86c406..b4d1164 100644
--- a/chapters/A2_benchmark.tex
+++ b/chapters/A2_benchmark.tex
@@ -277,7 +277,7 @@ The data and original model are available at:
 
 \begin{listing}
 	\mznfile{assets/listing/prize.mzn}
-	\caption{\label{lst:bench-prize} A \minizinc{} model for the Prize Collecting Path problem}
+	\caption{\label{lst:bench-prize} A \minizinc{} model for the Prize Collecting Path problem.}
 \end{listing}
 
 \paragraph{QCP-Max} This problem was introduced in by \textcite{feydy-2011-half-reif} in the original paper on \gls{half-reif}.
@@ -292,6 +292,6 @@ The data and original model are available at:
 
 \begin{listing}
 	\mznfile{assets/listing/qcp_max.mzn}
-	\caption{\label{lst:bench-qcpmax} A \minizinc{} model for the QCP-Max problem}
+	\caption{\label{lst:bench-qcpmax} A \minizinc{} model for the QCP-Max problem.}
 \end{listing}