From eeb1c18aa4b62401a75a460a446dc900ccb46c07 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 6 Aug 2025 17:40:38 -0700 Subject: [PATCH] more untangle params Signed-off-by: Lev Nachmanson --- src/smt/theory_seq.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 21e1944f8..bcce4241e 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3078,7 +3078,8 @@ void theory_seq::assign_eh(bool_var v, bool is_true) { f = m_sk.mk_suffix_inv(se1, se2); f = mk_concat(f, se1); propagate_eq(lit, f, se2, true); - propagate_eq(lit, mk_len(f), mk_len(se2), false); + auto p0 = mk_len(f); + propagate_eq(lit, p0, mk_len(se2), false); } else { propagate_not_suffix(e); @@ -3098,7 +3099,8 @@ void theory_seq::assign_eh(bool_var v, bool is_true) { expr_ref f2 = m_sk.mk_contains_right(se1, se2); f = mk_concat(f1, se2, f2); propagate_eq(lit, f, e1, true); - propagate_eq(lit, mk_len(f), mk_len(e1), false); + auto p0 = mk_len(f); + propagate_eq(lit, p0, mk_len(e1), false); } else { propagate_non_empty(lit, se2);