From 0765eea486f1bd55aba5ac30a6ce45f08f9ef67a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Dec 2016 05:45:40 +0100 Subject: [PATCH] add suggestions from #835 Signed-off-by: Nikolaj Bjorner --- src/ast/macros/macro_util.cpp | 2 +- src/muz/rel/dl_base.h | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp index 91bff5ab5..027cce09d 100644 --- a/src/ast/macros/macro_util.cpp +++ b/src/ast/macros/macro_util.cpp @@ -494,7 +494,7 @@ void macro_util::normalize_expr(app * head, expr * t, expr_ref & norm_t) const { tout << "applying substitution to:\n" << mk_ll_pp(t, m_manager) << "\nsubstitution:\n"; for (unsigned i = 0; i < var_mapping.size(); i++) { if (var_mapping[i] != 0) - tout << "#" << i << " -> " << mk_ll_pp(var_mapping[i], m_manager); + tout << "#" << i << " -> " << mk_ll_pp(var_mapping[i], m_manager); }); subst(t, var_mapping.size(), var_mapping.c_ptr(), norm_t); } diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index 9a2db4dbb..d3422f882 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -885,6 +885,7 @@ namespace datalog { class table_row_pair_reduce_fn { public: + virtual ~table_row_pair_reduce_fn() {} /** \brief The function is called for pair of table rows that became duplicit due to projection. The values that are in the first array after return from the function will be used for the