From ff1b35663ba3bb7ed3b222851d8c295dde6ab94d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 12 Apr 2021 09:32:03 -0700
Subject: [PATCH] revert rewriting of OP_LE, OP_GE as it breaks axioms

---
 src/ast/rewriter/seq_rewriter.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 4d01a0601..15b44de5b 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -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) {
 
+    return BR_FAILED;
+
     // k <= len(x) -> true  if k <= 0
     rational n;
     if (str().is_length(r) && m_autil.is_numeral(l, n) && n <= 0) {