mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-04 14:26:10 +00:00
Code Activity

misc edits of work in progress

Browse source
This commit is contained in:
Margus Veanes 2026-06-15 23:00:25 -06:00
parent 8fe488721b
commit a2b73b0ee6
2 changed files with 1 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/seq_regex_bisim.cpp
View file

@ -102,9 +102,7 @@ namespace seq {
expr* e = work.back(); expr* e = work.back();
work.pop_back(); work.pop_back();
expr* c = nullptr, * t = nullptr, * f = nullptr; expr* c = nullptr, * t = nullptr, * f = nullptr;
if (m.is_ite(e, c, t, f) || if (m.is_ite(e, c, t, f)) {
m_util.re.is_union(e, t, f) ||
m_util.re.is_antimirov_union(e, t, f)) {
if (seen.insert_if_not_there(t)) if (seen.insert_if_not_there(t))
work.push_back(t); work.push_back(t);
if (seen.insert_if_not_there(f)) if (seen.insert_if_not_there(f))

1
src/test/main.cpp
View file

@ -114,7 +114,6 @@
X(api_special_relations) \ X(api_special_relations) \
X(arith_rewriter) \ X(arith_rewriter) \
X(range_predicate) \ X(range_predicate) \
X(range_predicate_translator) \
X(regex_range_collapse) \ X(regex_range_collapse) \
X(check_assumptions) \ X(check_assumptions) \
X(smt_context) \ X(smt_context) \