fix #3930

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/datatype_decl_plugin.cpp

@@ -1239,7 +1239,7 @@ namespace datatype {
     }
 
     unsigned util::get_datatype_num_constructors(sort * ty) {
-		if (!is_declared(ty)) return 0;
+        if (!is_declared(ty)) return 0;
         def const& d = get_def(ty->get_name());
         return d.constructors().size();
     }

src/cmd_context/pdecl.cpp

@@ -217,17 +217,17 @@ class psort_app : public psort {
         unsigned operator()(psort_app const * d, unsigned idx) const { return d->m_args[idx]->hash(); }
     };
 
-    sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override {
+    sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override {        
         sort * r = find(s);
         if (r)
             return r;
         sort_ref_buffer args_i(m.m());
         unsigned sz = m_args.size();
-        for (unsigned i = 0; i < sz; i++) {
+        for (unsigned i = 0; i < sz; ++i) {
             sort * a = m_args[i]->instantiate(m, n, s);
             args_i.push_back(a);
         }
-        r = m_decl->instantiate(m, args_i.size(), args_i.c_ptr());
+        r = m_decl->instantiate(m, args_i.size(), args_i.c_ptr());        
         cache(m, s, r);
         return r;
     }
@@ -685,8 +685,10 @@ sort* pdecl_manager::instantiate_datatype(psort_decl* p, symbol const& name, uns
 
     pdecl_manager& m = *this;
     sort * r = p->find(s);
-    if (r)
+    if (r) {
+        notify_datatype(r, p, n, s);
         return r;
+    }
     buffer<parameter> ps;
     ps.push_back(parameter(name));
     for (unsigned i = 0; i < n; i++)
@@ -695,7 +697,16 @@ sort* pdecl_manager::instantiate_datatype(psort_decl* p, symbol const& name, uns
     r = m.m().mk_sort(util.get_family_id(), DATATYPE_SORT, ps.size(), ps.c_ptr());
     p->cache(m, s, r);
     m.save_info(r, p, n, s);
-    if (n > 0 && util.is_declared(r)) {
+    notify_datatype(r, p, n, s);
+    return r;
+}
+
+void pdecl_manager::notify_datatype(sort *r, psort_decl* p, unsigned n, sort* const* s) {
+    if (m_notified.contains(r) || n == 0)
+        return;
+    pdecl_manager& m = *this;
+    datatype_util util(m.m());
+    if (util.is_declared(r)) {
         bool has_typevar = false;
         // crude check ..
         for (unsigned i = 0; !has_typevar && i < n; ++i) {
@@ -704,8 +715,8 @@ sort* pdecl_manager::instantiate_datatype(psort_decl* p, symbol const& name, uns
         if (!has_typevar) {
             m.notify_new_dt(r, p);
         }
+        m_notified.insert(r);
     }
-    return r;
 }
 
 bool pdatatypes_decl::instantiate(pdecl_manager & m, sort * const * s) {

src/cmd_context/pdecl.h

@@ -287,6 +287,7 @@ class pdecl_manager {
     struct indexed_sort_info;
 
     obj_map<sort, sort_info *>   m_sort2info; // for pretty printing sorts
+    obj_hashtable<sort>          m_notified;
 
     void init_list();
     void del_decl_core(pdecl * p);
@@ -316,6 +317,7 @@ public:
     bool fix_missing_refs(pdatatypes_decl * s, symbol & missing) { return s->fix_missing_refs(missing); }
     sort * instantiate_datatype(psort_decl* p, symbol const& name, unsigned n, sort * const* s);
     sort * instantiate(psort * s, unsigned num, sort * const * args);
+    void notify_datatype(sort *r, psort_decl* p, unsigned n, sort* const* s);
 
     void lazy_dec_ref(pdecl * p) { p->dec_ref(); if (p->get_ref_count() == 0) m_to_delete.push_back(p); }
     template<typename T>

src/smt/theory_seq.cpp

@@ -3918,6 +3918,8 @@ void theory_seq::add_itos_axiom(expr* e) {
     add_axiom(eq1, ge0);
 
     add_axiom(mk_literal(m_autil.mk_ge(mk_len(e), m_autil.mk_int(0))));    
+
+
     
     // n >= 0 => stoi(itos(n)) = n
     app_ref stoi(m_util.str.mk_stoi(e), m);
@@ -3954,7 +3956,8 @@ bool theory_seq::add_itos_val_axiom(expr* e) {
     }
     add_length_to_eqc(e);
 
-    if (get_length(e, val) && val.is_pos()  && val.is_unsigned() && (!m_si_axioms.find(e, val2) || val != val2)) {
+    if (get_length(e, val) && val.is_pos()  && val.is_unsigned() && 
+        (!m_si_axioms.find(e, val2) || val != val2)) {
         add_si_axiom(e, n, val.get_unsigned());
         m_si_axioms.insert(e, val);
         m_trail_stack.push(push_replay(alloc(replay_is_axiom, m, e)));
@@ -3977,7 +3980,8 @@ bool theory_seq::add_stoi_val_axiom(expr* e) {
     }
     add_length_to_eqc(n);
 
-    if (get_length(n, val) && val.is_pos() && val.is_unsigned() && (!m_si_axioms.find(e, val2) || val2 != val)) {
+    if (get_length(n, val) && val.is_pos() && val.is_unsigned() && 
+        (!m_si_axioms.find(e, val2) || val2 != val)) {
         add_si_axiom(n, e, val.get_unsigned());        
         m_si_axioms.insert(e, val);
         m_trail_stack.push(push_replay(alloc(replay_is_axiom, m, e)));
@@ -4013,6 +4017,7 @@ expr_ref theory_seq::digit2int(expr* ch) {
 // 10^k <= n < 10^{k+1}-1 => len(e) => k
 
 void theory_seq::add_si_axiom(expr* e, expr* n, unsigned k) {
+
     context& ctx = get_context();
     zstring s;
     expr_ref ith_char(m), num(m), coeff(m);