From ff1429413d7026b8ff1a07b3176f3e581a1acb36 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Mon, 1 Mar 2021 10:31:48 +0000
Subject: [PATCH] Z3_subst: avoid unneded cache lookups

---
 src/ast/rewriter/expr_safe_replace.cpp | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

diff --git a/src/ast/rewriter/expr_safe_replace.cpp b/src/ast/rewriter/expr_safe_replace.cpp
index cc0e5a3a4..8f9321dbf 100644
--- a/src/ast/rewriter/expr_safe_replace.cpp
+++ b/src/ast/rewriter/expr_safe_replace.cpp
@@ -67,18 +67,16 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
             m_args.reset();
             bool arg_differs = false, has_all_args = true;
             for (expr* arg : *c) {
-                expr* d = m_cache[arg];
-                if (d) {
-                    if (has_all_args) {
+                if (has_all_args) {
+                    if (expr* d = m_cache[arg]) {
                         m_args.push_back(d);
                         arg_differs |= arg != d;
                         SASSERT(arg->get_sort() == d->get_sort());
+                        continue;
                     }
                 }
-                else {
-                    m_todo.push_back(arg);
-                    has_all_args = false;
-                }
+                m_todo.push_back(arg);
+                has_all_args = false;
             }
             if (has_all_args) {
                 if (arg_differs) {