From 5987d9ae20f2b6f897b7eeee9cadd8c226f097d2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 2 Jul 2020 11:14:29 -0700
Subject: [PATCH] cache computing strings and regexes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/seq_decl_plugin.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index d849df13c..f862125e0 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -548,6 +548,10 @@ sort* seq_decl_plugin::apply_binding(ptr_vector<sort> const& binding, sort* s) {
         SASSERT(is_sort(s->get_parameter(0).get_ast()));
         sort* p = apply_binding(binding, to_sort(s->get_parameter(0).get_ast()));
         parameter param(p);
+        if (p == m_char && s->get_decl_kind() == SEQ_SORT)
+            return m_string;
+        if (p == m_string && s->get_decl_kind() == RE_SORT)
+            return m_reglan;
         return mk_sort(s->get_decl_kind(), 1, &param);
     }
     return s;