Merge branch 'master' of https://github.com/z3prover/z3

src/api/python/z3/z3.py

@@ -6818,8 +6818,8 @@ class FiniteDomainSortRef(SortRef):
 
     def size(self):
         """Return the size of the finite domain sort"""
-        r = (ctype.c_ulonglong * 1)()
+        r = (ctypes.c_ulonglong * 1)()
-        if Z3_get_finite_domain_sort_size(self.ctx_ref(), self.ast(), r):
+        if Z3_get_finite_domain_sort_size(self.ctx_ref(), self.ast, r):
             return r[0]
         else:
             raise Z3Exception("Failed to retrieve finite domain sort size")

src/ast/ast.cpp

@@ -1532,6 +1532,17 @@ void ast_manager::copy_families_plugins(ast_manager const & from) {
               tout << "fid: " << fid << " fidname: " << get_family_name(fid) << "\n";
           });
     ast_translation trans(const_cast<ast_manager&>(from), *this, false);
+    // Inheriting plugins can create new family ids. Since new family ids are
+    // assigned in the order that they are created, this can result in differing
+    // family ids. To avoid this, we first assign all family ids and only then inherit plugins.
+    for (family_id fid = 0; from.m_family_manager.has_family(fid); fid++) {
+      symbol fid_name   = from.get_family_name(fid);
+      if (!m_family_manager.has_family(fid)) {
+          family_id new_fid = mk_family_id(fid_name);
+          (void)new_fid;
+          TRACE("copy_families_plugins", tout << "new target fid created: " << new_fid << " fid_name: " << fid_name << "\n";);
+      }
+    }
     for (family_id fid = 0; from.m_family_manager.has_family(fid); fid++) {
       SASSERT(from.is_builtin_family_id(fid) == is_builtin_family_id(fid));
       SASSERT(!from.is_builtin_family_id(fid) || m_family_manager.has_family(fid));
@@ -1539,11 +1550,6 @@ void ast_manager::copy_families_plugins(ast_manager const & from) {
       TRACE("copy_families_plugins", tout << "copying: " << fid_name << ", src fid: " << fid
             << ", target has_family: " << m_family_manager.has_family(fid) << "\n";
             if (m_family_manager.has_family(fid)) tout << get_family_id(fid_name) << "\n";);
-      if (!m_family_manager.has_family(fid)) {
-          family_id new_fid = mk_family_id(fid_name);
-          (void)new_fid;
-          TRACE("copy_families_plugins", tout << "new target fid created: " << new_fid << " fid_name: " << fid_name << "\n";);
-      }
       TRACE("copy_families_plugins", tout << "target fid: " << get_family_id(fid_name) << "\n";);
       SASSERT(fid == get_family_id(fid_name));
       if (from.has_plugin(fid) && !has_plugin(fid)) {

src/ast/fpa/fpa2bv_converter.cpp

@@ -25,7 +25,7 @@ Notes:
 #include "ast/fpa/fpa2bv_converter.h"
 #include "ast/rewriter/fpa_rewriter.h"
 
-#define BVULT(X,Y,R) { expr_ref bvult_eq(m), bvult_not(m); m_simp.mk_eq(X, Y, bvult_eq); m_simp.mk_not(bvult_eq, bvult_not); expr_ref t(m); t = m_bv_util.mk_ule(X,Y); m_simp.mk_and(t, bvult_not, R); }
+#define BVULT(X,Y,R) { expr_ref t(m); t = m_bv_util.mk_ule(Y,X); m_simp.mk_not(t, R); }
 
 fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
     m(m),

src/util/lp/dense_matrix.h

@@ -81,11 +81,12 @@ public:
 
     void set_number_of_rows(unsigned /*m*/) override {}
     void set_number_of_columns(unsigned /*n*/) override {}
+#ifdef Z3DEBUG
+    T get_elem(unsigned i, unsigned j) const override { return m_values[i * m_n + j]; }
+#endif
 
-    T get_elem(unsigned i, unsigned j) const { return m_values[i * m_n + j]; }
+    unsigned row_count() const override { return m_m; }
-
+    unsigned column_count() const override { return m_n; }
-    unsigned row_count() const { return m_m; }
-    unsigned column_count() const { return m_n; }
 
     void set_elem(unsigned i, unsigned j, const T& val) {  m_values[i * m_n + j] = val;  }
 

src/util/lp/eta_matrix.h

@@ -83,8 +83,8 @@ public:
     void apply_from_right(vector<T> & w) override;
     void apply_from_right(indexed_vector<T> & w) override;
 
-    T get_elem(unsigned i, unsigned j) const;
 #ifdef Z3DEBUG
+    T get_elem(unsigned i, unsigned j) const override;
     unsigned row_count() const override { return m_length; }
     unsigned column_count() const override { return m_length; }
     void set_number_of_rows(unsigned m) override { m_length = m; }

src/util/lp/lu.h

@@ -78,10 +78,10 @@ public:
     void set_number_of_columns(unsigned n) override { m_m = n; m_n = n; }
     T m_one_over_val;
 
-    T get_elem (unsigned i, unsigned j) const;
+    T get_elem (unsigned i, unsigned j) const override;
 
-    unsigned row_count() const { return m_m; } // not defined }
+    unsigned row_count() const override { return m_m; } // not defined }
-    unsigned column_count() const { return m_m; } // not defined  }
+    unsigned column_count() const override { return m_m; } // not defined  }
 #endif
     void apply_from_left(vector<X> & w, lp_settings &) override {
         w[m_i] /= m_val;