mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-15 08:44:10 +00:00
Code Activity

Bug

Browse source
This commit is contained in:
CEisenhofer 2026-04-07 09:33:14 +02:00
parent 2a32aa0204
commit 3e24cb7c10
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/seq/seq_nielsen.cpp
View file

@ -295,10 +295,10 @@ namespace seq {
mem.m_dep = m_graph.dep_mgr().mk_join(mem.m_dep, s.m_dep);
}
}
if (s.m_var->get_expr() && !sg.get_seq_util().is_seq(s.m_var->get_expr()) && !sg.get_seq_util().is_re(s.m_var->get_expr())) {
if (s.is_char_subst()) {
expr* v = s.m_var->get_expr();
expr* repl = s.m_replacement->get_expr();
expr* eq = sg.get_manager().mk_eq(v, repl);
add_constraint(constraint(eq, s.m_dep, sg.get_manager()));
}