mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

#5336

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-16 23:27:26 -05:00
parent d73ceaddc7
commit 9038dfd30d
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/sat/smt/q_solver.cpp
View file

@ -61,8 +61,11 @@ namespace q {
return;
}
if (l.sign() == is_forall(e))
add_clause(~l, skolemize(q));
if (l.sign() == is_forall(e)) {
sat::literal lit = skolemize(q);
add_clause(~l, lit);
ctx.add_root(~l, lit);
}
else {
ctx.push_vec(m_universal, l);
if (ctx.get_config().m_ematching)