mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

revert rewriting of OP_LE, OP_GE as it breaks axioms

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-12 09:32:03 -07:00
parent 804f065215
commit ff1b35663b
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -4395,6 +4395,8 @@ br_status seq_rewriter::reduce_re_eq(expr* l, expr* r, expr_ref& result) {
br_status seq_rewriter::mk_le_core(expr * l, expr * r, expr_ref & result) { br_status seq_rewriter::mk_le_core(expr * l, expr * r, expr_ref & result) {
return BR_FAILED;
// k <= len(x) -> true if k <= 0 // k <= len(x) -> true if k <= 0
rational n; rational n;
if (str().is_length(r) && m_autil.is_numeral(l, n) && n <= 0) { if (str().is_length(r) && m_autil.is_numeral(l, n) && n <= 0) {