mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-02 17:30:23 +00:00
Code Activity

always rewrite regex length constraints as they are sometimes malformed

Browse source
This commit is contained in:
Murphy Berzish 2018-01-25 15:52:57 -05:00
parent 852e0e0892
commit 5c3f35dc44
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_str.cpp
View file

@ -9787,7 +9787,10 @@ namespace smt {
} else { } else {
// generate new length constraint // generate new length constraint
expr_ref_vector extra_length_vars(m); expr_ref_vector extra_length_vars(m);
expr_ref top_level_length_constraint = infer_all_regex_lengths(mk_strlen(str), re, extra_length_vars); expr_ref _top_level_length_constraint = infer_all_regex_lengths(mk_strlen(str), re, extra_length_vars);
expr_ref top_level_length_constraint(_top_level_length_constraint, m);
th_rewriter rw(m);
rw(top_level_length_constraint);
TRACE("str", tout << "top-level length constraint: " << mk_pp(top_level_length_constraint, m) << std::endl;); TRACE("str", tout << "top-level length constraint: " << mk_pp(top_level_length_constraint, m) << std::endl;);
// assert and track length constraint // assert and track length constraint
assert_axiom(top_level_length_constraint); assert_axiom(top_level_length_constraint);