From 1d701f51b279613ba72ffbc66ea4ea5ee368cbb3 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 2 Dec 2024 11:31:24 -0600 Subject: [PATCH] Minor optimization to search (#1170) In the final version of the ULM, we want to enforce that semantics are deterministic. We do this using the search feature and the `--execute-to-branch` option which treats all states with more than one successor as final states and does not rewrite them further. I tested this by running the ethereum test suite with this option and all the tests passed (with a few trivial changes to the semantics). A minor change resulted from this effort: if only a single state is active at a given time, we do not need to do the expensive equality check performed by `erase`. It is sufficient to simply clear the hash set. --- runtime/util/search.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/runtime/util/search.cpp b/runtime/util/search.cpp index 4c52f5abf..901db51aa 100644 --- a/runtime/util/search.cpp +++ b/runtime/util/search.cpp @@ -72,7 +72,11 @@ std::unordered_set take_search_steps( while (!states.empty() && depth != 0) { state = states.front(); states.pop_front(); - states_set.erase(state); + if (states.empty()) { + states_set.clear(); + } else { + states_set.erase(state); + } if (depth > 0) { depth--;