remove unsound rewrite

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

src/ast/rewriter/arith_rewriter.cpp

@@ -1209,7 +1209,7 @@ br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) {
             result = m().mk_app(get_fid(), to_app(arg)->get_decl()->get_decl_kind(), int_args.size(), int_args.c_ptr());
             return BR_REWRITE1;
         }
-        if (!int_args.empty() && (m_util.is_add(arg) || m_util.is_mul(arg))) {
+        if (!int_args.empty() && m_util.is_add(arg)) {
             decl_kind k = to_app(arg)->get_decl()->get_decl_kind();
             expr_ref t1(m().mk_app(get_fid(), k, int_args.size(), int_args.c_ptr()), m());
             expr_ref t2(m().mk_app(get_fid(), k, real_args.size(), real_args.c_ptr()), m());

src/util/ref_vector.h

@@ -186,6 +186,7 @@ public:
             std::swap(m_nodes[i], m_nodes[sz-i-1]);
         }
     }
+
 };
 
 template<typename T, typename TManager>
@@ -304,6 +305,31 @@ public:
     
     // prevent abuse:
     ref_vector & operator=(ref_vector const & other) = delete;
+
+    ref_vector&& filter(std::function<bool(T)>& predicate) {
+        ref_vector result(m());
+        for (auto& t : *this)
+            if (predicate(t)) result.push_back(t);
+        return result;
+    }
+
+    template <typename S>
+    vector<S>&& map(std::function<S(T)>& f) {
+        vector<S> result;
+        for (auto& t : *this)
+            result.push_back(f(t));
+        return result;
+    }
+
+    ref_vector&& map(std::function<T(T)>& f) {
+        ref_vector result(m());
+        for (auto& t : *this)
+            result.push_back(f(t));
+        return result;
+    }
+
+
+
 };
 
 template<typename T>

src/util/vector.h

@@ -28,6 +28,7 @@ Revision History:
 #include<algorithm>
 #include<type_traits>
 #include<memory.h>
+#include<functional>
 #include "util/memory_manager.h"
 #include "util/hash.h"
 #include "util/z3_exception.h"
@@ -230,6 +231,21 @@ public:
         return *this;
     }
 
+    vector&& filter(std::function<bool(T)>& predicate) {
+        vector result;
+        for (auto& t : *this)
+            if (predicate(t)) result.push_back(t);
+        return result;
+    }
+
+    template <typename S>
+    vector<S>&& map(std::function<S(T)>& f) {
+        vector<S> result;
+        for (auto& t : *this)
+            result.push_back(f(t));
+        return result;
+    }
+
     void reset() { 
         if (m_data) {
             if (CallDestructors) {