From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 19 May 2021 23:32:25 +0000 (-0700)
Subject: Correctly handle negated assertions for assumption-based unsat cores. (#6579)
X-Git-Tag: cvc5-1.0.0~1730
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b7727338447cf8d738d9e95d032abe1d12532afd;p=cvc5.git

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 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
     {