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

z3str3: pass correct subterm to negative regex model construction

Browse source
This commit is contained in:
Murphy Berzish 2020-02-09 12:52:57 -05:00 committed by Nikolaj Bjorner
parent fd3c3a2599
commit 524434cfbb
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_str_mc.cpp
View file

@ -906,7 +906,7 @@ namespace smt {
} else if (u.str.is_in_re(subterm)) { } else if (u.str.is_in_re(subterm)) {
TRACE("str_fl", tout << "reduce negative regex membership: " << mk_pp(f, m) << std::endl;); TRACE("str_fl", tout << "reduce negative regex membership: " << mk_pp(f, m) << std::endl;);
expr_ref cex_clause(m); expr_ref cex_clause(m);
expr_ref re(f, m); expr_ref re(subterm, m);
if (!fixed_length_reduce_regex_membership(subsolver, re, cex_clause, false)) { if (!fixed_length_reduce_regex_membership(subsolver, re, cex_clause, false)) {
assert_axiom(cex_clause); assert_axiom(cex_clause);
add_persisted_axiom(cex_clause); add_persisted_axiom(cex_clause);