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