From 210ddf92aab09acc796b2a7fe34ba3bd983cbd62 Mon Sep 17 00:00:00 2001
From: Nguyễn Gia Phong <cnx@loang.net>
Date: Mon, 11 Dec 2023 13:34:41 +0900
Subject: Finish content

---
 technique.tex | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'technique.tex')

diff --git a/technique.tex b/technique.tex
index 470449f..af1fa92 100644
--- a/technique.tex
+++ b/technique.tex
@@ -333,6 +333,9 @@ If the path constraints of both states are \gls{sat} with at least
 one difference in outputs, a \gls{difftest} can be generated
 from the \gls{smt} model.
 
+Halt states are reached naturally at the program's termination or an error.
+The latter category also includes sanitizer traps for \gls{ub}.
+
 \begin{algorithm}
   \caption{\Gls{difftest} generation}\label{diffgen}
   \begin{algorithmic}[1]
@@ -379,8 +382,6 @@ from the \gls{smt} model.
 \subsection{Decision tree construction}
 From each \gls{difftest}, a set of clusters of revisions with the same output
 is constructed.  We then superimpose these clustering sets to create
-hierarchical clusterings or a decision tree.  A minimal tree, i.e~a tree
-with the shortest height, is found through exhaustively search though
-all subsets of set of clustering sets.
-
-TODO: analyse complexity
+hierarchical clusterings or a decision tree.  A minimal tree, i.e.~a tree
+with the shortest height, is found by searching through the subsets
+of set of clustering sets.
-- 
cgit 1.4.1

