From 4392b8871850ac797ed676f620f8798e903993fa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 31 Jan 2022 12:00:00 -0800 Subject: [PATCH] return negated literal when expression is "not" --- src/sat/tactic/goal2sat.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 30d73a21a..faaee95f8 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -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 _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; }