From 2503b35dc68a62315cae85c307e5aa4f44560133 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Nov 2025 15:56:44 -0800 Subject: [PATCH] check propagate ineqs setting before applying simplifier --- src/ast/simplifiers/bound_simplifier.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/ast/simplifiers/bound_simplifier.cpp b/src/ast/simplifiers/bound_simplifier.cpp index b5e927961..0fdecef7c 100644 --- a/src/ast/simplifiers/bound_simplifier.cpp +++ b/src/ast/simplifiers/bound_simplifier.cpp @@ -135,6 +135,10 @@ bool bound_simplifier::reduce_arg(expr* arg, expr_ref& result) { } void bound_simplifier::reduce() { + + smt_params_helper sp(p); + if (!sp.bound_simplifier()) + return; bool updated = true, found_bound = false; for (unsigned i = 0; i < 5 && updated; ++i) {