From f3e7c8c9df9e41c8dfdbbe5b3904be63d0a48f84 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 13 Jan 2025 08:13:39 -0800
Subject: [PATCH] include QF_SNIA

---
 src/solver/smt_logics.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp
index 65d3977ab..5e4015a4d 100644
--- a/src/solver/smt_logics.cpp
+++ b/src/solver/smt_logics.cpp
@@ -65,6 +65,7 @@ bool smt_logics::logic_has_arith(symbol const & s) {
         s == "QF_UFNIA" ||
         s == "QF_UFNIRA" ||
         s == "QF_BVRE" ||
+        s == "QF_SNIA" ||
         s == "ALIA" ||
         s == "AUFLIA" ||
         s == "AUFLIRA" ||
@@ -136,11 +137,11 @@ bool smt_logics::logic_has_array(symbol const & s) {
 }
 
 bool smt_logics::logic_has_seq(symbol const & s) {
-    return s == "QF_BVRE" || s == "QF_S" || s == "QF_SLIA" || logic_is_all(s);
+    return s == "QF_BVRE" || logic_has_str(s);
 }
 
 bool smt_logics::logic_has_str(symbol const & s) {
-    return s == "QF_S" || s == "QF_SLIA" || logic_is_all(s);
+    return s == "QF_S" || s == "QF_SLIA" || s == "QF_SNIA" || logic_is_all(s);
 }
 
 bool smt_logics::logic_has_fpa(symbol const & s) {