From b7ea90c12be97e33a06192a58398c8e0097085b4 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Thu, 12 Jul 2018 18:36:09 +0100
Subject: [PATCH] bv_decl_plugin: remove some mem allocs of parameters
---
src/ast/bv_decl_plugin.cpp | 6 +++---
src/util/trace.h | 1 -
2 files changed, 3 insertions(+), 4 deletions(-)
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() {}