3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00

return negated literal when expression is "not"

This commit is contained in:
Nikolaj Bjorner 2022-01-31 12:00:00 -08:00
parent 7ddfc54250
commit 4392b88718

View file

@ -805,6 +805,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
sat::literal internalize(expr* n, bool redundant) override {
bool is_not = m.is_not(n, n);
flet<bool> _top(m_top_level, false);
unsigned sz = m_result_stack.size();
(void)sz;
@ -820,6 +821,9 @@ struct goal2sat::imp : public sat::sat_internalizer {
m_map.insert(n, result.var());
m_solver.set_external(result.var());
}
if (is_not)
result.neg();
return result;
}