diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp
index 39d147ed1..d670888ed 100644
--- a/src/api/api_datatype.cpp
+++ b/src/api/api_datatype.cpp
@@ -51,7 +51,7 @@ extern "C" {
         constructor_decl* constrs[1] = { mk_constructor_decl(to_symbol(name), recognizer, acc.size(), acc.c_ptr()) };
 
         {
-            datatype_decl * dt = mk_datatype_decl(to_symbol(name), 1, constrs);
+            datatype_decl * dt = mk_datatype_decl(dt_util, to_symbol(name), 1, constrs);
             bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &dt, 0, 0, tuples);
             del_datatype_decl(dt);
 
@@ -113,7 +113,7 @@ extern "C" {
 
 
         {
-            datatype_decl * dt = mk_datatype_decl(to_symbol(name), n, constrs.c_ptr());
+            datatype_decl * dt = mk_datatype_decl(dt_util, to_symbol(name), n, constrs.c_ptr());
             bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &dt, 0, 0, sorts);
             del_datatype_decl(dt);
 
@@ -160,6 +160,7 @@ extern "C" {
         LOG_Z3_mk_list_sort(c, name, elem_sort, nil_decl, is_nil_decl, cons_decl, is_cons_decl, head_decl, tail_decl);
         RESET_ERROR_CODE();
         ast_manager& m = mk_c(c)->m();
+        datatype_util& dt_util = mk_c(c)->dtutil();
         mk_c(c)->reset_last_result();
         datatype_util data_util(m);
         accessor_decl* head_tail[2] = {
@@ -174,7 +175,7 @@ extern "C" {
 
         sort_ref_vector sorts(m);
         {
-            datatype_decl * decl = mk_datatype_decl(to_symbol(name), 2, constrs);
+            datatype_decl * decl = mk_datatype_decl(dt_util, to_symbol(name), 2, constrs);
             bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &decl, 0, 0, sorts);
             del_datatype_decl(decl);
 
@@ -316,6 +317,7 @@ extern "C" {
                                            Z3_symbol name,
                                            unsigned num_constructors,
                                            Z3_constructor constructors[]) {
+        datatype_util& dt_util = mk_c(c)->dtutil();
         ptr_vector<constructor_decl> constrs;
         for (unsigned i = 0; i < num_constructors; ++i) {
             constructor* cn = reinterpret_cast<constructor*>(constructors[i]);
@@ -330,7 +332,7 @@ extern "C" {
             }
             constrs.push_back(mk_constructor_decl(cn->m_name, cn->m_tester, acc.size(), acc.c_ptr()));
         }
-        return mk_datatype_decl(to_symbol(name), num_constructors, constrs.c_ptr());
+        return mk_datatype_decl(dt_util, to_symbol(name), num_constructors, constrs.c_ptr());
     }
 
     Z3_sort Z3_API Z3_mk_datatype(Z3_context c,
diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index e2aa54236..1c090bc33 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -95,7 +95,7 @@ public:
     ptr_vector<constructor_decl> const & get_constructors() const { return m_constructors; }
 };
 
-datatype_decl * mk_datatype_decl(symbol const & n, unsigned num_constructors, constructor_decl * const * cs) {
+datatype_decl * mk_datatype_decl(datatype_util&, symbol const & n, unsigned num_constructors, constructor_decl * const * cs) {
     return alloc(datatype_decl, n, num_constructors, cs);
 }
 
diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
index b9c2602ef..e3e1b7b10 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -16,7 +16,7 @@ Author:
 Revision History:
 
 --*/
-// define DATATYPE_V2
+//define DATATYPE_V2
 #ifdef DATATYPE_V2
 #include "ast/datatype_decl_plugin2.h"
 #else
@@ -79,14 +79,14 @@ class datatype_decl;
 class datatype_util;
 
 accessor_decl * mk_accessor_decl(symbol const & n, type_ref const & t);
-void del_accessor_decl(accessor_decl * d);
-void del_accessor_decls(unsigned num, accessor_decl * const * as);
+//void del_accessor_decl(accessor_decl * d);
+//void del_accessor_decls(unsigned num, accessor_decl * const * as);
 // Remark: the constructor becomes the owner of the accessor_decls
 constructor_decl * mk_constructor_decl(symbol const & n, symbol const & r, unsigned num_accessors, accessor_decl * const * acs);
-void del_constructor_decl(constructor_decl * d);
-void del_constructor_decls(unsigned num, constructor_decl * const * cs);
+//void del_constructor_decl(constructor_decl * d);
+//void del_constructor_decls(unsigned num, constructor_decl * const * cs);
 // Remark: the datatype becomes the owner of the constructor_decls
-datatype_decl * mk_datatype_decl(symbol const & n, unsigned num_constructors, constructor_decl * const * cs);
+datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_constructors, constructor_decl * const * cs);
 void del_datatype_decl(datatype_decl * d);
 void del_datatype_decls(unsigned num, datatype_decl * const * ds);
 
diff --git a/src/ast/datatype_decl_plugin2.cpp b/src/ast/datatype_decl_plugin2.cpp
index 2fc62af31..c059907d5 100644
--- a/src/ast/datatype_decl_plugin2.cpp
+++ b/src/ast/datatype_decl_plugin2.cpp
@@ -1,5 +1,5 @@
 /*++
-Copyright (c) 2006 Microsoft Corporation
+Copyright (c) 2017 Microsoft Corporation
 
 Module Name:
 
@@ -11,18 +11,21 @@ Abstract:
 
 Author:
 
-    Leonardo de Moura (leonardo) 2008-01-10.
+    Nikolaj Bjorner (nbjorner) 2017-9-1 
 
 Revision History:
 
 --*/
+
+#include "ast/datatype_decl_plugin.h"
+
+#ifdef DATATYPE_V2
 #include "util/warning.h"
 #include "ast/datatype_decl_plugin2.h"
 #include "ast/array_decl_plugin.h"
 #include "ast/ast_smt2_pp.h"
 
 
-#ifdef DATATYPE_V2
 namespace datatype {
 
     void accessor::fix_range(sort_ref_vector const& dts) {
@@ -57,6 +60,7 @@ namespace datatype {
     util& constructor::u() const { return m_def->u(); }
 
     func_decl_ref constructor::instantiate(sort_ref_vector const& ps) const {
+        ast_manager& m = ps.get_manager();
         sort_ref_vector domain(m);
         for (accessor const* a : accessors()) {
             domain.push_back(a->instantiate(ps)->get_range());
@@ -281,6 +285,11 @@ namespace datatype {
             }
         }
 
+        def* plugin::mk(symbol const& name, unsigned n, sort * const * params) {
+            ast_manager& m = *m_manager;
+            return alloc(def, m, u(), name, m_class_id, n, params);
+        }
+
         def& plugin::add(symbol const& name, unsigned n, sort * const * params) {
             ast_manager& m = *m_manager;
             def* d = 0;
@@ -313,6 +322,21 @@ namespace datatype {
             u().compute_datatype_size_functions(m_def_block);
         }
 
+        bool plugin::mk_datatypes(unsigned num_datatypes, def * const * datatypes, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_sorts) {
+            begin_def_block();
+            for (unsigned i = 0; i < num_datatypes; ++i) {
+                if (m_defs.find(datatypes[i]->name(), d)) dealloc(d);
+                m_defs.insert(datatypes[i]->name(), datatypes[i]);
+                m_def_block.push_back(datatypes[i]->name());
+            }
+            end_def_block();            
+            sort_ref_vector ps(*m_manager);
+            for (symbol const& s : m_def_block) {                
+                new_sorts.push_back(m_defs[s]->instantiate(ps));
+            }
+            return true;
+        }
+
         void plugin::del(symbol const& s) {
             def* d = 0;
             if (m_defs.find(s, d)) dealloc(d);
@@ -705,7 +729,7 @@ namespace datatype {
         return d;
     }
 
-    func_decl * util::get_recognizer_constructor(func_decl * recognizer) {
+    func_decl * util::get_recognizer_constructor(func_decl * recognizer) const {
         SASSERT(is_recognizer(recognizer));
         return to_func_decl(recognizer->get_parameter(0).get_ast());
     }
@@ -856,6 +880,22 @@ namespace datatype {
         return 0;
     }
 
+    unsigned util::get_constructor_idx(func_decl * f) const {
+        unsigned idx = 0;
+        def const& d = get_def(f->get_range());
+        for (constructor* c : d) {
+            if (c->name() == f->get_name()) {
+                return idx;
+            }
+            ++idx;
+        }
+        UNREACHABLE();
+        return 0;
+    }
+    unsigned util::get_recognizer_constructor_idx(func_decl * f) const {
+        return get_constructor_idx(get_recognizer_constructor(f));
+    }
+
 
     /**
        \brief Two datatype sorts s1 and s2 are siblings if they were
@@ -870,6 +910,12 @@ namespace datatype {
         }
     }
 
+    unsigned util::get_datatype_num_constructors(sort * ty) {
+        def const& d = get_def(ty->get_name());
+        return d.constructors().size();
+    }
+
+
     void util::display_datatype(sort *s0, std::ostream& strm) {
         ast_mark mark;
         ptr_buffer<sort> todo;
@@ -902,4 +948,14 @@ namespace datatype {
         }
     }
 }
+
+datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_constructors, constructor_decl * const * cs) {
+    datatype::decl::plugin* p = u.get_plugin();
+    datatype::def( d = p->mk(n, 0, 0);
+    for (unsigned i = 0; i < num_constructors; ++i) {
+        d->add(cs[i]);
+    }
+    return d;
+}
+
 #endif
diff --git a/src/ast/datatype_decl_plugin2.h b/src/ast/datatype_decl_plugin2.h
index c8aa042f1..c79939a5b 100644
--- a/src/ast/datatype_decl_plugin2.h
+++ b/src/ast/datatype_decl_plugin2.h
@@ -1,5 +1,5 @@
 /*++
-Copyright (c) 2006 Microsoft Corporation
+Copyright (c) 2017 Microsoft Corporation
 
 Module Name:
 
@@ -11,10 +11,13 @@ Abstract:
 
 Author:
 
-    Leonardo de Moura (leonardo) 2008-01-09.
+    Nikolaj Bjorner (nbjorner) 2017-9-1 
 
 Revision History:
 
+    rewritten to support SMTLIB-2.6 parameters from
+     Leonardo de Moura (leonardo) 2008-01-09.
+
 --*/
 #ifndef DATATYPE_DECL_PLUGIN2_H_
 #define DATATYPE_DECL_PLUGIN2_H_
@@ -74,12 +77,11 @@ namespace datatype {
     };
 
     class constructor {
-        ast_manager&     m;
         symbol           m_name;
         ptr_vector<accessor> m_accessors;
         def*             m_def;
     public:
-        constructor(ast_manager& m, symbol n): m(m), m_name(n) {}
+        constructor(symbol n): m_name(n) {}
         ~constructor();
         void add(accessor* a) { m_accessors.push_back(a); a->attach(this); }
         symbol const& name() const { return m_name; }
@@ -262,8 +264,12 @@ namespace datatype {
 
             def& add(symbol const& name, unsigned n, sort * const * params);
 
+            def* mk(symbol const& name, unsigned n, sort * const * params);
+
             void del(symbol const& d);
 
+            bool mk_datatypes(unsigned num_datatypes, def * const * datatypes, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_sorts);
+
             def const& get_def(sort* s) const { return *(m_defs[datatype_name(s)]); }
             def& get_def(symbol const& s) { return *(m_defs[s]); }
 
@@ -299,9 +305,7 @@ namespace datatype {
         family_id     m_family_id;
         mutable decl::plugin* m_plugin;
 
-        
-        func_decl * get_constructor(sort * ty, unsigned c_id) const;
-        
+                
         obj_map<sort, ptr_vector<func_decl> *>      m_datatype2constructors;
         obj_map<sort, func_decl *>                  m_datatype2nonrec_constructor;
         obj_map<func_decl, ptr_vector<func_decl> *> m_constructor2accessors;
@@ -310,14 +314,13 @@ namespace datatype {
         obj_map<func_decl, func_decl *>             m_accessor2constructor;
         obj_map<sort, bool>                         m_is_recursive;
         obj_map<sort, bool>                         m_is_enum;
-        mutable obj_map<sort, bool>                         m_is_fully_interp;
+        mutable obj_map<sort, bool>                 m_is_fully_interp;
         mutable ast_ref_vector                      m_asts;
         ptr_vector<ptr_vector<func_decl> >          m_vectors;
         unsigned                                    m_start;
-        mutable ptr_vector<sort>                            m_fully_interp_trail;
+        mutable ptr_vector<sort>                    m_fully_interp_trail;
         
         func_decl * get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set);
-        func_decl * get_constructor(sort * ty, unsigned c_id);
 
         friend class decl::plugin;
 
@@ -353,7 +356,7 @@ namespace datatype {
         func_decl * get_constructor_recognizer(func_decl * constructor);
         ptr_vector<func_decl> const & get_constructor_accessors(func_decl * constructor);
         func_decl * get_accessor_constructor(func_decl * accessor);
-        func_decl * get_recognizer_constructor(func_decl * recognizer);
+        func_decl * get_recognizer_constructor(func_decl * recognizer) const;
         family_id get_family_id() const { return m_family_id; }
         bool are_siblings(sort * s1, sort * s2);
         bool is_func_decl(op_kind k, unsigned num_params, parameter const* params, func_decl* f);
@@ -362,11 +365,12 @@ namespace datatype {
         void display_datatype(sort *s, std::ostream& strm);
         bool is_fully_interp(sort * s) const;
         sort_ref_vector datatype_params(sort * s) const;
+        unsigned get_constructor_idx(func_decl * f) const;
+        unsigned get_recognizer_constructor_idx(func_decl * f) const;
     };
 
 };
 
-#ifdef DATATYPE_V2
 typedef datatype::accessor accessor_decl;
 typedef datatype::constructor constructor_decl;
 typedef datatype::def datatype_decl;
@@ -394,7 +398,22 @@ inline accessor_decl * mk_accessor_decl(symbol const & n, type_ref const & t) {
         return alloc(accessor_decl, n, t.get_sort());
     }
 }
-#endif
+
+inline constructor_decl * mk_constructor_decl(symbol const & n, symbol const & r, unsigned num_accessors, accessor_decl * * acs) {
+    constructor_decl* c = alloc(constructor_decl, n);
+    for (unsigned i = 0; i < num_accessors; ++i) {
+        c->add(acs[i]);
+    }
+    return c;
+}
+
+
+
+// Remark: the datatype becomes the owner of the constructor_decls
+datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_constructors, constructor_decl * const * cs);
+inline void del_datatype_decl(datatype_decl * d) {}
+inline void del_datatype_decls(unsigned num, datatype_decl * const * ds) {}
+
 
 #endif /* DATATYPE_DECL_PLUGIN_H_ */
 
diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index ff1894a18..fbfcabd78 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -455,7 +455,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
             st = BR_DONE;
         }
     }
-    if (is_numeral(arg2, a2) && is_neg_poly(arg1, new_arg1)) {
+    if (m_arith_lhs && is_numeral(arg2, a2) && is_neg_poly(arg1, new_arg1)) {
         a2.neg();
         new_arg2 = m_util.mk_numeral(a2, m_util.is_int(new_arg1));
         switch (kind) {
@@ -523,7 +523,7 @@ expr_ref arith_rewriter::neg_monomial(expr* e) const {
         }
         else {
             args.push_back(m_util.mk_numeral(rational(-1), m_util.is_int(e)));
-            args.append(to_app(e)->get_num_args(), to_app(e)->get_args());
+            args.push_back(e);
         }
     }
     else {
diff --git a/src/ast/rewriter/poly_rewriter.h b/src/ast/rewriter/poly_rewriter.h
index c00464383..23743399e 100644
--- a/src/ast/rewriter/poly_rewriter.h
+++ b/src/ast/rewriter/poly_rewriter.h
@@ -36,6 +36,7 @@ protected:
     bool                    m_sort_sums;
     bool                    m_hoist_mul;
     bool                    m_hoist_cmul;
+    bool                    m_ast_order;
 
     bool is_numeral(expr * n) const { return Config::is_numeral(n); }
     bool is_numeral(expr * n, numeral & r) const { return Config::is_numeral(n, r); }
diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h
index 8fda040b6..b52440393 100644
--- a/src/ast/rewriter/poly_rewriter_def.h
+++ b/src/ast/rewriter/poly_rewriter_def.h
@@ -18,7 +18,8 @@ Notes:
 --*/
 #include "ast/rewriter/poly_rewriter.h"
 #include "ast/rewriter/poly_rewriter_params.hpp"
-// include "ast/ast_lt.h"
+#include "ast/rewriter/arith_rewriter_params.hpp"
+#include "ast/ast_lt.h"
 #include "ast/ast_ll_pp.h"
 #include "ast/ast_smt2_pp.h"
 
@@ -33,6 +34,8 @@ void poly_rewriter<Config>::updt_params(params_ref const & _p) {
     m_som_blowup = p.som_blowup();
     if (!m_flat) m_som = false;
     if (m_som) m_hoist_mul = false;
+    arith_rewriter_params ap(_p);
+    m_ast_order  = !ap.arith_ineq_lhs();
 }
 
 template<typename Config>
@@ -485,6 +488,8 @@ void poly_rewriter<Config>::hoist_cmul(expr_ref_buffer & args) {
 
 template<typename Config>
 bool poly_rewriter<Config>::mon_lt::operator()(expr* e1, expr * e2) const {
+    if (rw.m_ast_order) 
+        return lt(e1,e2);
     return ordinal(e1) < ordinal(e2);
 }
 
diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp
index 034b067c7..a9ce0b69c 100644
--- a/src/cmd_context/pdecl.cpp
+++ b/src/cmd_context/pdecl.cpp
@@ -566,7 +566,8 @@ datatype_decl * pdatatype_decl::instantiate_decl(pdecl_manager & m, sort * const
     for (auto c : m_constructors) {
         cs.push_back(c->instantiate_decl(m, s));
     }
-    return mk_datatype_decl(m_name, cs.size(), cs.c_ptr());
+    datatype_util util(m.m());
+    return mk_datatype_decl(util, m_name, cs.size(), cs.c_ptr());
 }
 
 struct datatype_decl_buffer {
@@ -679,9 +680,7 @@ struct pdecl_manager::sort_info {
     }
     virtual ~sort_info() {}
     virtual unsigned obj_size() const { return sizeof(sort_info); }
-    virtual void finalize(pdecl_manager & m) {
-        m.dec_ref(m_decl);
-    }
+    virtual void finalize(pdecl_manager & m) { m.dec_ref(m_decl); }
     virtual void display(std::ostream & out, pdecl_manager const & m) const = 0;
     virtual format * pp(pdecl_manager const & m) const = 0;
 };
diff --git a/src/cmd_context/pdecl.h b/src/cmd_context/pdecl.h
index 66e9cff53..e7fae8dd5 100644
--- a/src/cmd_context/pdecl.h
+++ b/src/cmd_context/pdecl.h
@@ -23,6 +23,7 @@ Revision History:
 #include "util/obj_hashtable.h"
 #include "util/dictionary.h"
 #include "ast/format.h"
+#include "ast/datatype_decl_plugin.h"
 
 class pdecl_manager;
 
@@ -139,10 +140,10 @@ public:
     virtual void display(std::ostream & out) const;
 };
 
-class datatype_decl_plugin;
-class datatype_decl;
-class constructor_decl;
-class accessor_decl;
+//class datatype_decl_plugin;
+//class datatype_decl;
+//class constructor_decl;
+//class accessor_decl;
 
 class pdatatypes_decl;
 class pdatatype_decl;
diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp
index b9dbe83ca..9109f6b3c 100644
--- a/src/muz/bmc/dl_bmc_engine.cpp
+++ b/src/muz/bmc/dl_bmc_engine.cpp
@@ -979,7 +979,7 @@ namespace datalog {
                     symbol is_name(_name.str().c_str());
                     cnstrs.push_back(mk_constructor_decl(name, is_name, accs.size(), accs.c_ptr()));
                 }
-                dts.push_back(mk_datatype_decl(pred->get_name(), cnstrs.size(), cnstrs.c_ptr()));
+                dts.push_back(mk_datatype_decl(dtu, pred->get_name(), cnstrs.size(), cnstrs.c_ptr()));
             }
 
 
@@ -1027,7 +1027,7 @@ namespace datalog {
                     accs.push_back(mk_accessor_decl(name, tr));
                     cnstrs.push_back(mk_constructor_decl(name, is_name, accs.size(), accs.c_ptr()));
                 }
-                dts.push_back(mk_datatype_decl(symbol("Path"), cnstrs.size(), cnstrs.c_ptr()));
+                dts.push_back(mk_datatype_decl(dtu, symbol("Path"), cnstrs.size(), cnstrs.c_ptr()));
                 VERIFY (dtp->mk_datatypes(dts.size(), dts.c_ptr(), 0, 0, new_sorts));
                 m_path_sort = new_sorts[0].get();
             }
diff --git a/src/test/get_consequences.cpp b/src/test/get_consequences.cpp
index e8868c661..229cbe834 100644
--- a/src/test/get_consequences.cpp
+++ b/src/test/get_consequences.cpp
@@ -65,9 +65,8 @@ void test2() {
     constructor_decl* G = mk_constructor_decl(symbol("G"), symbol("is-G"), 0, 0);
     constructor_decl* B = mk_constructor_decl(symbol("B"), symbol("is-B"), 0, 0);
     constructor_decl* constrs[3] = { R, G, B };
-    datatype_decl * enum_sort = mk_datatype_decl(symbol("RGB"), 3, constrs);
+    datatype_decl * enum_sort = mk_datatype_decl(dtutil, symbol("RGB"), 3, constrs);
     VERIFY(dt.mk_datatypes(1, &enum_sort, 0, 0, new_sorts));    
-    del_constructor_decls(3, constrs);
     sort* rgb = new_sorts[0].get();
 
     expr_ref x = mk_const(m, "x", rgb), y = mk_const(m, "y", rgb), z = mk_const(m, "z", rgb);