From f0a02e408dace944c95562ee7b37bf146ad7dfdb Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Tue, 10 Oct 2023 17:32:25 -0700 Subject: [PATCH] fix lint --- src/halmos/__main__.py | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index d1e68bbc..0f44a6b9 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -971,7 +971,11 @@ def refine(query: str) -> str: # TODO: replace `(evm_bvudiv x y)` with `(ite (= y (_ bv0 256)) (_ bv0 256) (bvudiv x y))` # as bvudiv is undefined when y = 0; also similarly for evm_bvurem query = re.sub(r"(\(\s*)evm_(bv[a-z]+)(_[0-9]+)?\b", r"\1\2", query) - return re.sub(r"\(\s*declare-fun\s+evm_(bv[a-z]+)(_[0-9]+)?\b", r"(declare-fun dummy_\1\2", query) + return re.sub( + r"\(\s*declare-fun\s+evm_(bv[a-z]+)(_[0-9]+)?\b", + r"(declare-fun dummy_\1\2", + query, + ) def gen_model(args: Namespace, idx: int, ex: Exec) -> ModelWithContext: