From b7727338447cf8d738d9e95d032abe1d12532afd Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 19 May 2021 16:32:25 -0700
Subject: [PATCH] Correctly handle negated assertions for assumption-based
 unsat cores. (#6579)

---
 src/prop/prop_engine.cpp | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 63591e74b..b71c728e7 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -271,9 +271,15 @@ void PropEngine::assertInternal(
   {
     if (input)
     {
-      Assert(!negated);
       d_cnfStream->ensureLiteral(node);
-      d_assumptions.push_back(node);
+      if (negated)
+      {
+        d_assumptions.push_back(node.notNode());
+      }
+      else
+      {
+        d_assumptions.push_back(node);
+      }
     }
     else
     {
-- 
2.30.2