From 9c620376c2f117a0c5d419faafc922075c449e81 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 7 Mar 2016 13:15:12 +0000 Subject: [PATCH] simplify ast::are_equal(), since pointer equality is sufficient --- src/ast/ast.h | 2 +- src/ast/rewriter/bool_rewriter.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index c386ccd63..6c69e4037 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -972,7 +972,7 @@ public: */ virtual bool is_unique_value(app * a) const { return false; } - virtual bool are_equal(app * a, app * b) const { return a == b && is_unique_value(a) && is_unique_value(b); } + virtual bool are_equal(app * a, app * b) const { return a == b; } virtual bool are_distinct(app * a, app * b) const { return a != b && is_unique_value(a) && is_unique_value(b); } diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 48dffdb58..71be3d1c2 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -671,7 +671,7 @@ static bool is_ite_value_tree_neq_value(ast_manager & m, app * ite, app * val) { #endif br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { - if (lhs == rhs) { + if (m().are_equal(lhs, rhs)) { result = m().mk_true(); return BR_DONE; }