remove buggy bv-trailing

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/rewriter/CMakeLists.txt

@@ -33,7 +33,6 @@ z3_add_component(rewriter
     seq_rewriter.cpp
     th_rewriter.cpp
     var_subst.cpp
-    bv_trailing.cpp
     mk_extract_proc.cpp
   COMPONENT_DEPENDENCIES
     ast

src/ast/rewriter/bv_rewriter.cpp

@@ -29,7 +29,6 @@ void bv_rewriter::updt_local_params(params_ref const & _p) {
     m_elim_sign_ext = p.elim_sign_ext();
     m_mul2concat = p.mul2concat();
     m_bit2bool = p.bit2bool();
-    m_trailing = p.bv_trailing();
     m_urem_simpl = p.bv_urem_simpl();
     m_blast_eq_value = p.blast_eq_value();
     m_split_concat_eq = p.split_concat_eq();
@@ -2591,15 +2590,6 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
             return st;
     }
 
-    if (m_trailing) {        
-        st = m_rm_trailing.eq_remove_trailing(lhs, rhs, result);
-        m_rm_trailing.reset_cache(1 << 12);
-        if (st != BR_FAILED) {
-            TRACE("eq_remove_trailing", tout << mk_ismt2_pp(lhs, m()) << "\n=\n" << mk_ismt2_pp(rhs, m()) << "\n----->\n" << mk_ismt2_pp(result, m()) << "\n";);
-            return st;
-        }
-    }
-
     st = mk_mul_eq(lhs, rhs, result);
     if (st != BR_FAILED) {
         TRACE("mk_mul_eq", tout << mk_ismt2_pp(lhs, m()) << "\n=\n" << mk_ismt2_pp(rhs, m()) << "\n----->\n" << mk_ismt2_pp(result,m()) << "\n";);

src/ast/rewriter/bv_rewriter.h

@@ -23,7 +23,6 @@ Module Name:
 #include "ast/bv_decl_plugin.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/rewriter/mk_extract_proc.h"
-#include "ast/rewriter/bv_trailing.h"
 
 class bv_rewriter_core {
 protected:
@@ -49,7 +48,6 @@ class bv_rewriter_core {
 
 class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     mk_extract_proc m_mk_extract;
-    bv_trailing     m_rm_trailing;
     arith_util m_autil;
     bool       m_hi_div0;
     bool       m_elim_sign_ext;
@@ -61,7 +59,6 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     bool       m_split_concat_eq;
     bool       m_bvnot2arith;
     bool       m_bv_sort_ac;
-    bool       m_trailing;
     bool       m_extract_prop;
     bool       m_bvnot_simpl;
     bool       m_le_extra;
@@ -159,7 +156,6 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     bv_rewriter(ast_manager & m, params_ref const & p = params_ref()):
         poly_rewriter<bv_rewriter_core>(m, p),
         m_mk_extract(m_util),
-        m_rm_trailing(m_mk_extract),
         m_autil(m) {
         updt_local_params(p);
     }

src/ast/rewriter/bv_rewriter_params.pyg

@@ -9,7 +9,6 @@ def_module_params(module_name='rewriter',
                           ("mul2concat", BOOL, False, "replace multiplication by a power of two into a concatenation"),
                           ("bvnot2arith", BOOL, False, "replace (bvnot x) with (bvsub -1 x)"),
                           ("bv_sort_ac", BOOL, False, "sort the arguments of all AC operators"),
-                          ("bv_trailing", BOOL, False, "lean removal of trailing zeros"),
                           ("bv_extract_prop", BOOL, False, "attempt to partially propagate extraction inwards"),
                           ("bv_not_simpl", BOOL, False, "apply simplifications for bvnot"),
                           ("bv_ite2id", BOOL, False, "rewrite ite that can be simplified to identity"),