From 2503b35dc68a62315cae85c307e5aa4f44560133 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Nov 2025 15:56:44 -0800 Subject: [PATCH 1/2] 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) { From 11fb5c7dc49d879cdc2a3c3c4a732cd3c39749c5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Nov 2025 16:11:58 -0800 Subject: [PATCH 2/2] comment out parameter check Signed-off-by: Nikolaj Bjorner --- src/ast/simplifiers/bound_simplifier.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ast/simplifiers/bound_simplifier.cpp b/src/ast/simplifiers/bound_simplifier.cpp index 0fdecef7c..3ae3a1a01 100644 --- a/src/ast/simplifiers/bound_simplifier.cpp +++ b/src/ast/simplifiers/bound_simplifier.cpp @@ -136,10 +136,11 @@ bool bound_simplifier::reduce_arg(expr* arg, expr_ref& result) { void bound_simplifier::reduce() { + #if 0 smt_params_helper sp(p); if (!sp.bound_simplifier()) return; - + #endif bool updated = true, found_bound = false; for (unsigned i = 0; i < 5 && updated; ++i) { updated = false;