From 30021dd74fd797754ccc5d357ba97a91a773ed2c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 19 Mar 2025 08:57:23 -1000 Subject: [PATCH] fix #7590 logic alphabet soup Signed-off-by: Nikolaj Bjorner --- src/solver/smt_logics.cpp | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp index 02c884268..1afea69dc 100644 --- a/src/solver/smt_logics.cpp +++ b/src/solver/smt_logics.cpp @@ -70,14 +70,8 @@ bool smt_logics::logic_has_bv(symbol const & s) { bool smt_logics::logic_has_array(symbol const & s) { return - s.str().find("QF_A") != std::string::npos || - s == "ALIA" || - s == "AUFLIA" || - s == "AUFLIRA" || - s == "AUFNIA" || - s == "AUFNIRA" || - s == "AUFBV" || - s == "ABV" || + s.str().starts_with("QF_A") || + s.str().starts_with("A") || logic_is_all(s) || s == "SMTFD" || s == "HORN";