From f3147d6e220bd23dee7fd9996838ae1ba22982a1 Mon Sep 17 00:00:00 2001
From: Pierre Bouvier <53953588+tic-toc@users.noreply.github.com>
Date: Mon, 26 Oct 2020 20:01:21 +0100
Subject: [PATCH] Fix: QF_UFDT has UF (#4755)

---
 src/solver/smt_logics.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp
index bf0651a95..ec1acfdb7 100644
--- a/src/solver/smt_logics.cpp
+++ b/src/solver/smt_logics.cpp
@@ -148,7 +148,7 @@ bool smt_logics::logic_has_fpa(symbol const & s) {
 }
 
 bool smt_logics::logic_has_uf(symbol const & s) {
-    return s == "QF_UF" || s == "UF" || s == "QF_DT" || s == "SMTFD";
+    return s == "QF_UF" || s == "UF" || s == "QF_UFDT" || s == "SMTFD";
 }
 
 bool smt_logics::logic_has_horn(symbol const& s) {