diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
index 4869949b7..6bbe3ce13 100644
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@@ -401,7 +401,7 @@ bool bv_decl_plugin::get_int2bv_size(unsigned num_parameters, parameter const *
         m_manager->raise_exception("int2bv expects one parameter");
         return false;
     }
-    parameter p(parameters[0]);
+    const parameter &p = parameters[0];
     if (p.is_int()) {
         result = p.get_int();
         return true;
@@ -428,7 +428,7 @@ func_decl * bv_decl_plugin::mk_num_decl(unsigned num_parameters, parameter const
     // After SMT-COMP, I should find all offending modules.
     // For now, I will just simplify the numeral here.
     parameter p0(mod(parameters[0].get_rational(), rational::power_of_two(bv_size)));
-    parameter ps[2] = { p0, parameters[1] };
+    parameter ps[2] = { std::move(p0), parameters[1] };
     sort * bv = get_bv_sort(bv_size);
     return m_manager->mk_const_decl(m_bv_sym, bv, func_decl_info(m_family_id, OP_BV_NUM, num_parameters, ps));
 }
@@ -746,7 +746,7 @@ void bv_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const
 expr * bv_decl_plugin::get_some_value(sort * s) {
     SASSERT(s->is_sort_of(m_family_id, BV_SORT));
     unsigned bv_size = s->get_parameter(0).get_int();
-    parameter p[2] = { parameter(rational(0)), parameter(static_cast<int>(bv_size)) };
+    parameter p[2] = { parameter(rational::zero()), parameter(static_cast<int>(bv_size)) };
     return m_manager->mk_app(m_family_id, OP_BV_NUM, 2, p, 0, nullptr);
 }
 
diff --git a/src/util/trace.h b/src/util/trace.h
index c0dc90f23..1a245036f 100644
--- a/src/util/trace.h
+++ b/src/util/trace.h
@@ -51,7 +51,6 @@ void finalize_trace();
 static inline void enable_trace(const char * tag) {}
 static inline void enable_all_trace(bool flag) {}
 static inline void disable_trace(const char * tag) {}
-// On a default Visual C++ build on Windows, a non-void function either needs to return a value, or we have to add: #pragma warning(default:4716)  
 static inline bool is_trace_enabled(const char * tag) { return false; }
 static inline void close_trace() {}
 static inline void open_trace() {}