From d05d3bac4f8e57fc9168af1a80d93221cfad9bfa Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 5 Sep 2017 20:12:48 -0700
Subject: [PATCH] fix instantiations

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/pdecl.cpp       | 26 ++++++++++++++++++++++++--
 src/parsers/smt2/smt2parser.cpp |  5 ++++-
 2 files changed, 28 insertions(+), 3 deletions(-)

diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp
index 1887d677d..2293072a2 100644
--- a/src/cmd_context/pdecl.cpp
+++ b/src/cmd_context/pdecl.cpp
@@ -604,8 +604,30 @@ struct datatype_decl_buffer {
 
 #ifdef DATATYPE_V2
 sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) {
-    UNREACHABLE();
-    return 0;
+    // TBD: copied
+    SASSERT(n == m_num_params);
+    sort * r = find(s);
+    if (r)
+        return r;
+    buffer<parameter> ps;
+    ps.push_back(parameter(m_name));
+    for (unsigned i = 0; i < n; i++)
+        ps.push_back(parameter(s[i]));
+    datatype_util util(m.m());
+    r = m.m().mk_sort(util.get_family_id(), DATATYPE_SORT, ps.size(), ps.c_ptr());
+    cache(m, s, r);
+    m.save_info(r, this, n, s);
+    if (m_num_params > 0 && util.is_declared(r)) {
+        bool has_typevar = false;
+        // crude check ..
+        for (unsigned i = 0; !has_typevar && i < n; ++i) {
+            has_typevar = s[i]->get_name().is_numerical();
+        }
+        if (!has_typevar) {
+            m.notify_new_dt(r, this);
+        }
+    }
+    return r;
 }
 #else
 sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) {
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 8144ebc08..7bfc8bd99 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -917,7 +917,10 @@ namespace smt2 {
                 pdatatype_decl * d = new_dt_decls[i];
                 symbol duplicated;
                 check_duplicate(d, line, pos);
-                m_ctx.insert(d);
+                if (!is_smt2_6) {
+                    // datatypes are inserted up front in SMT2.6 mode, so no need to re-insert them.
+                    m_ctx.insert(d);
+                }
             }                
 #endif
             TRACE("declare_datatypes", tout << "i: " << i << " new_dt_decls.size(): " << sz << "\n";