From 125eae06bdea90029fe95fc9c64374ea775779a1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 26 Oct 2021 11:54:29 +0200
Subject: [PATCH] #4869 load datatype parsing for HORN logic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
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 ec1acfdb7..65d3977ab 100644
--- a/src/solver/smt_logics.cpp
+++ b/src/solver/smt_logics.cpp
@@ -160,6 +160,6 @@ bool smt_logics::logic_has_pb(symbol const& s) {
}
bool smt_logics::logic_has_datatype(symbol const& s) {
- return s == "QF_FD" || s == "QF_UFDT" || logic_is_all(s) || s == "QF_DT";
+ return s == "QF_FD" || s == "QF_UFDT" || logic_is_all(s) || s == "QF_DT" || logic_has_horn(s);
}