mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-04 10:20:23 +00:00
Code Activity

disable regex length constraint generation as it currently makes unsound axioms

Browse source
This commit is contained in:
Murphy Berzish 2018-01-17 13:32:44 -05:00
parent 26ab91a448
commit c0ed683882
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_str.cpp
View file

@ -9609,6 +9609,8 @@ namespace smt {
continue; continue;
} }
// DISABLED due to bug -- star-over-union (and possibly others) results in unsound constraints
/*
if (!regex_terms_with_length_constraints.contains(str_in_re)) { if (!regex_terms_with_length_constraints.contains(str_in_re)) {
if (current_assignment == l_true && check_regex_length_linearity(re)) { if (current_assignment == l_true && check_regex_length_linearity(re)) {
TRACE("str", tout << "regex length constraints expected to be linear -- generating and asserting them" << std::endl;); TRACE("str", tout << "regex length constraints expected to be linear -- generating and asserting them" << std::endl;);
@ -9654,6 +9656,7 @@ namespace smt {
regex_axiom_add = true; regex_axiom_add = true;
} }
} // re not in regex_terms_with_length_constraints } // re not in regex_terms_with_length_constraints
*/
rational exact_length_value; rational exact_length_value;
if (get_len_value(str, exact_length_value)) { if (get_len_value(str, exact_length_value)) {