From 780346c7ca86a6f8ab9ac6fe4ecb032cc8b5c52b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 24 Jul 2020 13:22:19 -0700
Subject: [PATCH] address model generation bugs raised in #4518 and #4324

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/seq_decl_plugin.cpp |  2 +-
 src/model/seq_factory.h     | 22 ++++++++++++++++++----
 src/smt/seq_skolem.cpp      |  6 +++---
 3 files changed, 22 insertions(+), 8 deletions(-)

diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index b2c24547a..a3759e6e7 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -1130,7 +1130,7 @@ expr* seq_decl_plugin::get_some_value(sort* s) {
 }
 
 app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range) {
-    SASSERT(range);
+    SASSERT(range);    
     parameter param(name);
     func_decl* f = m.mk_func_decl(get_family_id(), _OP_SEQ_SKOLEM, 1, &param, n, args, range);
     return m.mk_app(f, n, args);
diff --git a/src/model/seq_factory.h b/src/model/seq_factory.h
index 77a186478..6679c4f52 100644
--- a/src/model/seq_factory.h
+++ b/src/model/seq_factory.h
@@ -86,7 +86,7 @@ public:
                 return true;
             }
             else {
-                    return false;
+                return false;
             }
         }
         NOT_IMPLEMENTED_YET();
@@ -106,7 +106,7 @@ public:
         sort* seq = nullptr, *ch = nullptr;
         if (u.is_re(s, seq)) {
             expr* v0 = get_fresh_value(seq);
-                return u.re.mk_to_re(v0);
+            return u.re.mk_to_re(v0);
         }
         if (u.is_char(s)) {
             //char s[2] = { ++m_char, 0 };
@@ -115,9 +115,23 @@ public:
         }
         if (u.is_seq(s, ch)) {
             expr* v = m_model.get_fresh_value(ch);
-            if (!v) return nullptr;
-            return u.str.mk_unit(v);
+            if (v) {
+                return u.str.mk_unit(v);
             }
+            else {
+                v = u.str.mk_unit(m_model.get_some_value(ch));
+                expr* uniq = nullptr;
+                if (m_unique_sequences.find(s, uniq)) {
+                    uniq = u.str.mk_concat(v, uniq);
+                }
+                else {
+                    uniq = v;
+                }                
+                m_trail.push_back(uniq);
+                m_unique_sequences.insert(s, uniq);
+                return uniq;
+            }
+        }        
         UNREACHABLE();
         return nullptr;
     }
diff --git a/src/smt/seq_skolem.cpp b/src/smt/seq_skolem.cpp
index e110d41c7..5d53cd6d3 100644
--- a/src/smt/seq_skolem.cpp
+++ b/src/smt/seq_skolem.cpp
@@ -46,7 +46,9 @@ expr_ref seq_skolem::mk(symbol const& s, expr* e1, expr* e2, expr* e3, expr* e4,
     if (!range) {
         range = m.get_sort(e1);
     }
-    return expr_ref(seq.mk_skolem(s, len, es, range), m);
+    expr_ref result(seq.mk_skolem(s, len, es, range), m);
+    m_rewrite(result);
+    return result;
 }
 
 expr_ref seq_skolem::mk_max_unfolding_depth(unsigned depth) { 
@@ -113,13 +115,11 @@ decompose_main:
         head = seq.str.mk_unit(seq.str.mk_nth_i(s, idx));
         tail = mk(m_tail, s, idx);
         m_rewrite(head);
-        m_rewrite(tail);
     }
     else {
         head = seq.str.mk_unit(seq.str.mk_nth_i(e, a.mk_int(0)));
         tail = mk(m_tail, e, a.mk_int(0));
         m_rewrite(head);
-        m_rewrite(tail);
     }
 }