mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

fix theory_str::check_length_concat_concat to actually assert the conflict axiom

Browse source
This commit is contained in:
Murphy Berzish 2016-07-28 17:18:56 -04:00
parent 244b611f1c
commit 6f67e9cdda
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/theory_str.cpp
View file

@ -4261,6 +4261,7 @@ bool theory_str::check_length_concat_concat(expr * n1, expr * n2) {
if (conflict) { if (conflict) {
TRACE("t_str_detail", tout << "inconsistent length detected in concat <==> concat" << std::endl;); TRACE("t_str_detail", tout << "inconsistent length detected in concat <==> concat" << std::endl;);
assert_axiom(toAssert);
return false; return false;
} }
return true; return true;