From dbdd3ea807232b0be83d6a0eba9eb13011eb48e5 Mon Sep 17 00:00:00 2001
From: ericmarin <maarin.eric@gmail.com>
Date: Sun, 21 Jun 2026 15:38:35 +0200
Subject: related work + conclusion

---
 chapters/background/03-satisfiability-modulo-theories.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'chapters/background/03-satisfiability-modulo-theories.tex')

diff --git a/chapters/background/03-satisfiability-modulo-theories.tex b/chapters/background/03-satisfiability-modulo-theories.tex
index bd90559..a55d54d 100644
--- a/chapters/background/03-satisfiability-modulo-theories.tex
+++ b/chapters/background/03-satisfiability-modulo-theories.tex
@@ -19,6 +19,6 @@ To represent a ReLU activation $y = \max(0, x)$ in LRA, we must introduce a disj
     (x > 0 \land y = x) \lor (x \le 0 \land y = 0)
 \end{equation}
 For a network with $N$ ReLU neurons, there are up to $2^N$ possible activation patterns. Solving the
-verification property requires the SMT solver, such as Z3 presented by Demura et al.~\cite{demoura2008z3},
+verification property requires the SMT solver, such as Z3 presented by De Moura et al.~\cite{demoura2008z3},
 to implicitly explore this branching search space.
 
-- 
cgit v1.2.3

