From 3629cd9447d7d72391e8e1e5907e40651ecb277d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Apr 2026 11:42:50 -0700 Subject: [PATCH] regression fixes Signed-off-by: Nikolaj Bjorner --- src/smt/seq/seq_nielsen.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 5d69f1faf..7352813a8 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -251,7 +251,8 @@ namespace seq { bool nielsen_node::add_constraint(constraint const &c) { if (graph().get_manager().is_and(c.fml)) { for (const auto f : *to_app(c.fml)) { - add_constraint(constraint(f, c.dep, graph().get_manager())); + if (!add_constraint(constraint(f, c.dep, graph().get_manager()))) + return false; } return true; } @@ -1141,8 +1142,8 @@ namespace seq { expr_ref d(rw.mk_derivative(mem.m_regex->get_expr()), m); // Extract the inner char expression from seq.unit(?inner) - expr *unit_expr = tok->arg(0)->get_expr(), *inner_char; - + expr *inner_char = tok->arg(0)->get_expr(); + // substitute the inner char for the derivative variable in d var_subst vs(m); d = vs(d, inner_char);