From edbe1087e3e738ac2dc799213c9ba9ca49df3f52 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 26 Jul 2023 15:08:21 +0200
Subject: [PATCH] one check in get_name is enough

---
 src/math/polysat/naming.cpp | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/math/polysat/naming.cpp b/src/math/polysat/naming.cpp
index df9ac6236..64583fa16 100644
--- a/src/math/polysat/naming.cpp
+++ b/src/math/polysat/naming.cpp
@@ -53,8 +53,6 @@ namespace polysat {
     }
 
     pvar name_manager::mk_name(pdd const& t, bool allow_values) {
-        if (t.is_var())
-            return t.var();
         SASSERT(allow_values || !t.is_val());  // we probably don't want names for constants
         pvar v = get_name(t);
         if (v != null_var)