fixes for #4634

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Aug 13, 2020 · 72d1403 · 72d1403
1 parent c41abf2
commit 72d1403
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 0 deletions.
diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
@@ -645,6 +645,7 @@ namespace datatype {
         SASSERT(is_datatype(s));
         bool fi = true;
         return fi;
+#if 0
         if (m_is_fully_interp.find(s, fi)) {
             return fi;
         }
@@ -671,6 +672,7 @@ namespace datatype {
         m_is_fully_interp.insert(s, is_interp);
         m_asts.push_back(s);
         return true;
+#endif
     }
 
     /**

diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
@@ -1172,9 +1172,11 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r
     m_mpz_manager.set(remaining, max_exp_diff_adj);
     while (m_mpz_manager.gt(remaining, INT32_MAX)) {
         throw default_exception("zero extension overflow floating point types are too large");
+#if 0
         edr_tmp = m_bv_util.mk_zero_extend(INT32_MAX, edr_tmp);
         nedr_tmp = m_bv_util.mk_zero_extend(INT32_MAX, nedr_tmp);
         m_mpz_manager.sub(remaining, INT32_MAX, remaining);
+#endif
     }
     if (!m_mpz_manager.is_zero(remaining)) {
         edr_tmp = m_bv_util.mk_zero_extend(m_mpz_manager.get_uint(remaining), edr_tmp);