Correctly handle negated assertions for assumption-based unsat cores. (#6579)

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 63591e74bce8e4569ffb043186571769a6980c22..b71c728e7e49f40f201f347b3ba6c14bd4454552 100644 (file)
--- 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
     {