diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 5f19994ca..f1e964fb9 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -622,8 +622,8 @@ void seq_decl_plugin::init() {
     m_sigs[OP_STRING_CONST]      = nullptr;
     m_sigs[_OP_STRING_STRIDOF]   = alloc(psig, m, "str.indexof", 0, 3, str2TintT, intT);
     m_sigs[_OP_STRING_STRREPL]   = alloc(psig, m, "str.replace", 0, 3, str3T, strT);
-    m_sigs[OP_STRING_ITOS]       = alloc(psig, m, "int.to.str", 0, 1, &intT, strT);
-    m_sigs[OP_STRING_STOI]       = alloc(psig, m, "str.to.int", 0, 1, &strT, intT);
+    m_sigs[OP_STRING_ITOS]       = alloc(psig, m, "str.from_int", 0, 1, &intT, strT);
+    m_sigs[OP_STRING_STOI]       = alloc(psig, m, "str.to_int", 0, 1, &strT, intT);
     m_sigs[OP_STRING_LT]         = alloc(psig, m, "str.<", 0, 2, str2T, boolT);
     m_sigs[OP_STRING_LE]         = alloc(psig, m, "str.<=", 0, 2, str2T, boolT);
     m_sigs[_OP_STRING_CONCAT]    = alloc(psig, m, "str.++", 1, 2, str2T, strT);
@@ -928,7 +928,13 @@ void seq_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol cons
         }
     }
     op_names.push_back(builtin_name("str.in.re", _OP_STRING_IN_REGEXP));
+    op_names.push_back(builtin_name("str.in-re", _OP_STRING_IN_REGEXP));
     op_names.push_back(builtin_name("str.to.re", _OP_STRING_TO_REGEXP));
+    op_names.push_back(builtin_name("str.to-re", _OP_STRING_TO_REGEXP));
+    op_names.push_back(builtin_name("str.to-int", OP_STRING_STOI));
+    op_names.push_back(builtin_name("str.to.int", OP_STRING_STOI));
+    op_names.push_back(builtin_name("str.from-int", OP_STRING_ITOS));
+    op_names.push_back(builtin_name("int.to.str", OP_STRING_ITOS));
     op_names.push_back(builtin_name("re.nostr",  _OP_REGEXP_EMPTY));
     op_names.push_back(builtin_name("re.complement", OP_RE_COMPLEMENT));
 }
diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp
index 1c3101e25..697f8b750 100644
--- a/src/cmd_context/check_logic.cpp
+++ b/src/cmd_context/check_logic.cpp
@@ -182,7 +182,7 @@ struct check_logic::imp {
             m_bvs         = true;
             m_quantifiers = true;
         }
-        else if (logic == "QF_S") {
+        else if (logic == "QF_S" || logic == "QF_SLIA") {
             m_uf          = true;
             m_bvs         = true;
             m_ints        = true;
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 2e2e9da0f..d3d6c1f0c 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -129,7 +129,7 @@ namespace smt {
             setup_QF_FP();
         else if (m_logic == "QF_FPBV" || m_logic == "QF_BVFP")
             setup_QF_FPBV();
-        else if (m_logic == "QF_S")
+        else if (m_logic == "QF_S" || m_logic == "QF_SLIA")
             setup_QF_S();
         else if (m_logic == "QF_DT")
             setup_QF_DT();
@@ -177,7 +177,7 @@ namespace smt {
                  setup_QF_BVRE();
             else if (m_logic == "QF_AUFLIA")
                 setup_QF_AUFLIA(st);
-            else if (m_logic == "QF_S")
+            else if (m_logic == "QF_S" || m_logic == "QF_SLIA")
                 setup_QF_S();
             else if (m_logic == "AUFLIA")
                 setup_AUFLIA(st);
diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp
index f454fb9c6..9b77bca6d 100644
--- a/src/solver/smt_logics.cpp
+++ b/src/solver/smt_logics.cpp
@@ -85,6 +85,7 @@ bool smt_logics::logic_has_arith(symbol const & s) {
         s == "QF_FPBV" ||
         s == "QF_BVFP" ||
         s == "QF_S" ||
+        s == "QF_SLIA" ||
         logic_is_allcsp(s) ||
         s == "QF_FD" ||
         s == "HORN" ||
@@ -135,11 +136,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" || logic_is_allcsp(s);
+    return s == "QF_BVRE" || s == "QF_S" || s == "QF_SLIA" || logic_is_allcsp(s);
 }
 
 bool smt_logics::logic_has_str(symbol const & s) {
-    return s == "QF_S" || logic_is_allcsp(s);
+    return s == "QF_S" || s == "QF_SLIA" || logic_is_allcsp(s);
 }
 
 bool smt_logics::logic_has_fpa(symbol const & s) {