From 894702d6003a70e9c3042bcb81efa31e03ca86d3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 14 Mar 2020 14:42:24 -0700
Subject: [PATCH] fix #3301
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/smt_internalizer.cpp | 6 ++----
1 file changed, 2 insertions(+), 4 deletions(-)
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 44c10f9be..26e0737c5 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1039,10 +1039,8 @@ namespace smt {
\brief Return the literal associated with n.
*/
literal context::get_literal(expr * n) const {
- if (m.is_not(n)) {
- CTRACE("get_literal_bug", !b_internalized(to_app(n)->get_arg(0)), tout << mk_ll_pp(n, m) << "\n";);
- SASSERT(b_internalized(to_app(n)->get_arg(0)));
- return literal(get_bool_var(to_app(n)->get_arg(0)), true);
+ if (m.is_not(n, n)) {
+ return ~get_literal(n);
}
else if (m.is_true(n)) {
return true_literal;