From e8080d2307cb7a7b82a5eb1663b09d28ca13680e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 22 Jun 2019 23:55:11 +0200 Subject: [PATCH] revert normalizing ordering on equality as it breaks others and doesn't necessarily lead to simplification Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bool_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 90e6c37d7..14a06a5f7 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -646,7 +646,7 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) app* bool_rewriter::mk_eq(expr* lhs, expr* rhs) { - // if (lhs->get_id() > rhs->get_id()) std::swap(lhs, rhs); + // degrades simplification on if (lhs->get_id() > rhs->get_id()) std::swap(lhs, rhs); return m().mk_eq(lhs, rhs); }