mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Fix #430: disable rewriting of concatentations with constants because it breaks equality propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
2a65503235
commit
cf970fd76a
|
@ -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 {
|
||||
|
|
|
@ -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))
|
||||
|
|
Loading…
Reference in a new issue