From f1a2e875b594391a2491aacc56d70f283a3fed80 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 5 Apr 2019 03:06:41 -0700
Subject: [PATCH] fixing #2217

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/python/z3/z3.py          | 7 +++++++
 src/ast/datatype_decl_plugin.cpp | 6 +++++-
 src/smt/smt_context.h            | 1 -
 src/smt/theory_datatype.cpp      | 8 +++++++-
 4 files changed, 19 insertions(+), 3 deletions(-)

diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 76e87775a..9276c3502 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -10379,3 +10379,10 @@ def Range(lo, hi, ctx = None):
 
 # Special Relations
 
+def PartialOrder(n, s):
+    ctx = s.ctx
+    return FuncDeclRef(Z3_mk_partial_order(ctx, n, s.ast), ctx)
+
+def TreeOrder(n, s):
+    ctx = s.ctx
+    return FuncDeclRef(Z3_mk_tree_order(ctx, n, s.ast), ctx)
diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index e8f276aa8..c98cc06f8 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -290,6 +290,7 @@ namespace datatype {
                     obj_map<sort, sort_size> S;
                     for (unsigned i = 0; i + 1 < num_parameters; ++i) {
                         sort* r = to_sort(parameters[i + 1].get_ast());
+                        TRACE("datatype", tout << "inserting " << mk_ismt2_pp(r, *m_manager) << " " << r->get_num_elements() << "\n";);
                         S.insert(d->params()[i], r->get_num_elements()); 
                     }
                     sort_size ts = d->sort_size()->eval(S);
@@ -693,7 +694,7 @@ namespace datatype {
     }
 
     param_size::size* util::get_sort_size(sort_ref_vector const& params, sort* s) {
-        if (params.empty()) {
+        if (params.empty() && !is_datatype(s)) {
             return param_size::size::mk_offset(s->get_num_elements());
         }
         if (is_datatype(s)) {
@@ -742,6 +743,7 @@ namespace datatype {
         map<symbol, status, symbol_hash_proc, symbol_eq_proc> already_found;
         map<symbol, param_size::size*, symbol_hash_proc, symbol_eq_proc> szs;
 
+        TRACE("datatype", for (auto const& s : names) tout << s << " "; tout << "\n";);
         svector<symbol> todo(names);
         status st;
         while (!todo.empty()) {
@@ -780,6 +782,7 @@ namespace datatype {
             todo.pop_back();
             already_found.insert(s, BLACK);
             if (is_infinite) {
+                TRACE("datatype", tout << "infinite " << s << "\n";);
                 d.set_sort_size(param_size::size::mk_offset(sort_size::mk_infinite()));
                 continue;
             }
@@ -792,6 +795,7 @@ namespace datatype {
                 }
                 s_add.push_back(param_size::size::mk_times(s_mul));
             }
+            TRACE("datatype", tout << "set sort size " << s << "\n";);
             d.set_sort_size(param_size::size::mk_plus(s_add));
         }
     }
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 42111c591..d4d4ec6fb 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -923,7 +923,6 @@ namespace smt {
         failure            m_last_search_failure;
         ptr_vector<theory> m_incomplete_theories; //!< theories that failed to produce a model
         bool               m_searching;
-        bool               m_propagating;
         unsigned           m_num_conflicts;
         unsigned           m_num_conflicts_since_restart;
         unsigned           m_num_conflicts_since_lemma_gc;
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index dd1b302e1..d084191be 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -372,7 +372,13 @@ namespace smt {
         //   
         // If the theory variable is not created for 'a', then a wrong model will be generated.
         TRACE("datatype", tout << "apply_sort_cnstr: #" << n->get_owner_id() << "\n";);
-        TRACE("datatype_bug", tout << "apply_sort_cnstr:\n" << mk_pp(n->get_owner(), get_manager()) << "\n";);
+            TRACE("datatype_bug", 
+                  tout << "apply_sort_cnstr:\n" << mk_pp(n->get_owner(), get_manager()) << " ";
+                  tout << m_util.is_datatype(s) << " ";
+                  if (m_util.is_datatype(s)) tout << "is-infinite: " << s->is_infinite() << " "; 
+                  if (m_util.is_datatype(s)) tout << "attached: " << is_attached_to_var(n) << " ";
+                  tout << "\n";
+                  );
         if ((get_context().has_quantifiers() || (m_util.is_datatype(s) && !s->is_infinite())) && !is_attached_to_var(n)) {
             mk_var(n);
         }