From a5e4e520fb5712be29107c67304a28d83254919b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 12 Aug 2020 10:12:22 -0700
Subject: [PATCH] fix #4628 - not really a bug, but style nit. uf1 and uf2 need
 both to be called

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/hoist_rewriter.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ast/rewriter/hoist_rewriter.cpp b/src/ast/rewriter/hoist_rewriter.cpp
index 31909f12b..99ccbd91e 100644
--- a/src/ast/rewriter/hoist_rewriter.cpp
+++ b/src/ast/rewriter/hoist_rewriter.cpp
@@ -154,7 +154,7 @@ unsigned hoist_rewriter::mk_var(expr* e) {
     if (m_expr2var.find(e, v)) {
         return v;
     }
-    v = m_uf1.mk_var();
+    m_uf1.mk_var();
     v = m_uf2.mk_var();
     SASSERT(v == m_var2expr.size());
     m_expr2var.insert(e, v);