mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix solve_concat_eq_str() case 4: prefixStr should have been suffixStr

Browse source
This commit is contained in:
Murphy Berzish 2015-09-29 17:52:19 -04:00
parent 2320b6dc48
commit 191c50b529
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_str.cpp
View file

@ -622,7 +622,7 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) {
expr_ref arg1_eq (ctx.mk_eq_atom(arg1, prefixAst), m);
and_items[and_count++] = ctx.mk_eq_atom(xorAst, arg1_eq);
expr_ref suffixAst(m_strutil.mk_string(prefixStr), m);
expr_ref suffixAst(m_strutil.mk_string(suffixStr), m);
expr_ref arg2_eq (ctx.mk_eq_atom(arg2, suffixAst), m);
and_items[and_count++] = ctx.mk_eq_atom(xorAst, arg2_eq);
}