From 11f14a4763533dbc24b0e98d115071036025d4f6 Mon Sep 17 00:00:00 2001
From: ericmarin <maarin.eric@gmail.com>
Date: Mon, 22 Jun 2026 00:43:45 +0200
Subject: refinement

---
 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 a40df41..6023c2e 100644
--- a/chapters/core/implementation/04-python-module.tex
+++ b/chapters/core/implementation/04-python-module.tex
@@ -1,8 +1,8 @@
 \subsection{Python Module}
 \label{sec:python-module}
 
-The core functionality of the VEIN system is implemented via the \texttt{vein.Solver}, an extension of
-the \texttt{z3.Solver} class offered in the Z3 python
+The core functionality of the \textbf{VEIN} system is implemented via the \texttt{vein.Solver}, an extension of
+the \texttt{z3.Solver} class offered in the Z3 Python
 package\footnote{\href{https://pypi.org/project/z3-solver}{\textbf{PyPi package}}}. This design choice
 ensures flexibility and ease of use for researchers already familiar with using the Z3 Python API.
 
@@ -19,7 +19,7 @@ into a pending queue and it is reduced to normal form only after the \texttt{che
 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 declaration, optional range
+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)
 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.
-- 
cgit v1.2.3

