From f66a082de9e51205b42a910a0640a73172aa5eeb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 18 Feb 2023 14:10:58 -0800
Subject: [PATCH] fix #6595
---
.gitignore | 1 +
src/ast/rewriter/bv_bounds_base.h | 3 ++-
2 files changed, 3 insertions(+), 1 deletion(-)
diff --git a/.gitignore b/.gitignore
index 936f977aa..b0c19a432 100644
--- a/.gitignore
+++ b/.gitignore
@@ -22,6 +22,7 @@ ocamlz3
# Directories with generated code and documentation
release/*
build/*
+trace/*
build-dist/*
dist/*
src/out/*
diff --git a/src/ast/rewriter/bv_bounds_base.h b/src/ast/rewriter/bv_bounds_base.h
index 840cf6e3e..8542e5921 100644
--- a/src/ast/rewriter/bv_bounds_base.h
+++ b/src/ast/rewriter/bv_bounds_base.h
@@ -185,7 +185,7 @@ namespace bv {
m_args.push_back(arg);
continue;
}
- if (!m_bv.is_extract(arg) && m_bound.find(arg, b)) {
+ if (!m_bv.is_extract(arg) && m_bound.find(arg, b) && b.lo() <= b.hi()) {
unsigned num_bits = b.hi().get_num_bits();
unsigned bv_size = m_bv.get_bv_size(arg);
if (0 < num_bits && num_bits < bv_size) {
@@ -202,6 +202,7 @@ namespace bv {
if (simplified) {
result = m.mk_app(to_app(t)->get_decl(), m_args);
+ TRACE("bv", tout << mk_pp(t, m) << " -> " << result << "\n");
return true;
}