From cf970fd76afaedcfa4fcadb3bafc6e010502fe84 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 5 Feb 2016 10:59:24 +0000 Subject: [PATCH 1/2] Fix #430: disable rewriting of concatentations with constants because it breaks equality propagation Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bv_rewriter.cpp | 4 ++-- src/tactic/core/solve_eqs_tactic.cpp | 10 +++++++--- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 6a652c2f7..ab78eaf97 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -2010,8 +2010,8 @@ bool bv_rewriter::is_add_mul_const(expr* e) const { bool bv_rewriter::is_concat_target(expr* lhs, expr* rhs) const { return - (m_util.is_concat(lhs) && (is_concat_split_target(rhs) || has_numeral(to_app(lhs)))) || - (m_util.is_concat(rhs) && (is_concat_split_target(lhs) || has_numeral(to_app(rhs)))); + (m_util.is_concat(lhs) && is_concat_split_target(rhs)) || + (m_util.is_concat(rhs) && is_concat_split_target(lhs)); } bool bv_rewriter::has_numeral(app* a) const { diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index e436d19c4..1923869a4 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -106,9 +106,13 @@ class solve_eqs_tactic : public tactic { } } bool trivial_solve(expr * lhs, expr * rhs, app_ref & var, expr_ref & def, proof_ref & pr) { - return - trivial_solve1(lhs, rhs, var, def, pr) || - trivial_solve1(rhs, lhs, var, def, pr); + if (trivial_solve1(lhs, rhs, var, def, pr)) return true; + if (trivial_solve1(rhs, lhs, var, def, pr)) { + if (m_produce_proofs) { + pr = m().mk_commutativity(m().mk_eq(lhs, rhs)); + } + } + return false; } // (ite c (= x t1) (= x t2)) --> (= x (ite c t1 t2)) From eae17a43a2dc66b99d12c7596044b82b933760fa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 5 Feb 2016 11:00:17 +0000 Subject: [PATCH 2/2] Fix #430: disable rewriting of concatentations with constants because it breaks equality propagation Signed-off-by: Nikolaj Bjorner --- src/tactic/core/solve_eqs_tactic.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index 1923869a4..f23d874a6 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -111,6 +111,7 @@ class solve_eqs_tactic : public tactic { if (m_produce_proofs) { pr = m().mk_commutativity(m().mk_eq(lhs, rhs)); } + return true; } return false; }