From fced47386e405b26ce6c72b592c85b9710e6a76e Mon Sep 17 00:00:00 2001
From: mikolas <mikolas.janota@gmail.com>
Date: Mon, 4 Apr 2016 11:31:23 +0100
Subject: [PATCH] More work on trailing 0 analysis.

---
 src/ast/rewriter/bv_rewriter.cpp | 4 +---
 src/ast/rewriter/bv_rewriter.h   | 3 +++
 src/ast/rewriter/bv_trailing.h   | 1 -
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index d30e082f2..19b4bd122 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -20,7 +20,6 @@ Notes:
 #include"bv_rewriter_params.hpp"
 #include"poly_rewriter_def.h"
 #include"ast_smt2_pp.h"
-#include"bv_trailing.h"
 
 
 void bv_rewriter::updt_local_params(params_ref const & _p) {
@@ -2094,8 +2093,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
     }
 
     if (m_trailing) {
-        bv_trailing bvt(m_mk_extract);
-        st = bvt.eq_remove_trailing(lhs, rhs, result);
+        st = m_rm_trailing.eq_remove_trailing(lhs, rhs, result);
         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;
diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h
index e9b76768a..7135c52ba 100644
--- a/src/ast/rewriter/bv_rewriter.h
+++ b/src/ast/rewriter/bv_rewriter.h
@@ -23,6 +23,7 @@ Notes:
 #include"bv_decl_plugin.h"
 #include"arith_decl_plugin.h"
 #include"mk_extract_proc.h"
+#include"bv_trailing.h"
 
 class bv_rewriter_core {
 protected:
@@ -47,6 +48,7 @@ public:
 
 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;
@@ -138,6 +140,7 @@ public:
     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);
     }
diff --git a/src/ast/rewriter/bv_trailing.h b/src/ast/rewriter/bv_trailing.h
index 4ff24a5d9..0af909e8f 100644
--- a/src/ast/rewriter/bv_trailing.h
+++ b/src/ast/rewriter/bv_trailing.h
@@ -17,7 +17,6 @@
 #ifndef BV_TRAILING_H_
 #define BV_TRAILING_H_
 #include"ast.h"
-#include"bv_rewriter.h"
 #include"rewriter_types.h"
 #include"mk_extract_proc.h"
 class bv_trailing {