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

na

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-27 09:31:04 -07:00
parent 78571b9a51
commit a71b4fab23
1 changed files with 2 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/sat/smt/dt_solver.cpp
View file

@ -717,10 +717,8 @@ namespace dt {
}
sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
if (!visit_rec(m, e, sign, root, redundant)) {
TRACE("dt", tout << mk_pp(e, m) << "\n";);
return sat::null_literal;
}
if (!visit_rec(m, e, sign, root, redundant))
return sat::null_literal;
auto lit = ctx.expr2literal(e);
if (sign)
lit.neg();