mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity

ensure ast_manager::are_equal returns true if expr ptrs are equal

Browse source 
found by Nikolaj
This commit is contained in:
Nuno Lopes 2016-03-08 16:53:09 +00:00
parent 809fc86ac7
commit d0de8fff62
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/ast.cpp
View file

@ -1560,6 +1560,9 @@ bool ast_manager::is_unique_value(expr* e) const {
}
bool ast_manager::are_equal(expr * a, expr * b) const {
if (a == b) {
return true;
}
if (is_app(a) && is_app(b)) {
app* ap = to_app(a), *bp = to_app(b);
decl_plugin const * p = get_plugin(ap->get_family_id());