3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00

add suggestions from #835

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-12-11 05:45:40 +01:00
parent 70bb92d016
commit 0765eea486
2 changed files with 2 additions and 1 deletions

View file

@ -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);
}

View file

@ -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