mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-13 10:44:43 +00:00
Code Activity

add documentation to initial selection of tactics

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-12-05 20:04:58 -08:00
parent f1a65d9642
commit 5a5758baaa
5 changed files with 229 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/simplifiers/solve_context_eqs.cpp
View file

@ -279,7 +279,7 @@ namespace euf {
}
else if (m.is_not(f, f))
todo.push_back({ !s, depth, f });
else if (!s && 1 == depth % 2) {
else if (!s && 1 <= depth) {
for (extract_eq* ex : m_solve_eqs.m_extract_plugins) {
ex->set_allow_booleans(false);
ex->get_eqs(dependent_expr(m, f, df.dep()), eqs);