mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

z3str3: assert precondition for regex linearity axiom

Browse source
This commit is contained in:
Murphy Berzish 2020-02-13 14:43:09 -05:00 • committed by Nikolaj Bjorner
parent 0146259ea4
commit 85fd139c7f
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_str_regex.cpp
View file

@ -93,7 +93,8 @@ namespace smt {
// generate new length constraint
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(_top_level_length_constraint, m);
expr_ref premise(str_in_re, m);
expr_ref top_level_length_constraint(m.mk_implies(premise, _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;);