mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-03-07 13:35:54 +00:00
parent 3560be86ac 9c620376c2
commit 3a9b4985e4
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/ast.h
View file

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

2
src/ast/rewriter/bool_rewriter.cpp
View file

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