From 1c70bcee69110fff57f293f5f6049bf14b1c2123 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Tue, 24 Sep 2019 13:18:16 -0400
Subject: [PATCH] z3str3: setup uninterpreted functions as though they were
 string variables

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

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index aa0ee2167..823cb3824 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -8417,7 +8417,7 @@ namespace smt {
                     TRACE("str", tout << "found string-integer conversion term: " << mk_pp(ex, get_manager()) << std::endl;);
                     string_int_conversion_terms.push_back(ap);
                     m_library_aware_axiom_todo.push_back(n);
-                } else if (ap->get_num_args() == 0 && !u.str.is_string(ap)) {
+                } else if (/*ap->get_num_args() == 0 &&*/ !u.str.is_string(ap)) {
                     // if ex is a variable, add it to our list of variables
                     TRACE("str", tout << "tracking variable " << mk_ismt2_pp(ap, get_manager()) << std::endl;);
                     variable_set.insert(ex);