From a8bb7736e2e86963bd5761cc05079447abeeaba6 Mon Sep 17 00:00:00 2001
From: ericmarin <maarin.eric@gmail.com>
Date: Tue, 23 Jun 2026 15:26:01 +0200
Subject: using official template + fixing language errors

---
 chapters/core/implementation/04-python-module.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'chapters/core/implementation/04-python-module.tex')

diff --git a/chapters/core/implementation/04-python-module.tex b/chapters/core/implementation/04-python-module.tex
index 6023c2e..ab817c4 100644
--- a/chapters/core/implementation/04-python-module.tex
+++ b/chapters/core/implementation/04-python-module.tex
@@ -15,14 +15,14 @@ The methods offered by \texttt{vein.Solver} are:
 \end{itemize}
 
 The framework uses a \textit{lazy evaluation} strategy: when loading a neural network, it is placed
-into a pending queue and it is reduced to normal form only after the \texttt{check} method is
+into a pending queue, and it is reduced to normal form only after the \texttt{check} method is
 called.
 
 The specification follows the SMT-LIB\footnote{\href{https://smt-lib.org}{\textbf{SMT-LIB Website}}}
 format. It should contain the input and output symbolic variables declarations, optional range
-constraints on the input variables and the properties to be verified. For Multi-Network (relational)
+constraints on the input variables, and the properties to be verified. For Multi-Network (relational)
 verification, the system ensures that multiple networks share the same input symbolic variables.
-This approach allows Z3 to compare their outputs directly given the same inputs.
+This approach allows Z3 to compare the outputs directly, given the same inputs.
 
 The execution pipeline is implemented within the \texttt{check} method:
 \begin{itemize}
-- 
cgit v1.2.3

