From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 23 Aug 2019 15:15:43 +0000 (-0500)
Subject: Minor update to term util (#3208)
X-Git-Tag: cvc5-1.0.0~4000
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fd385efcc6b1e55431430af4213172594781e05f;p=cvc5.git

Minor update to term util (#3208)
---

diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 1243d8d4a..94bc2c3f8 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -612,14 +612,21 @@ bool TermUtil::containsUninterpretedConstant( Node n ) {
   return n.getAttribute(ContainsUConstAttribute())!=0;
 }
 
-Node TermUtil::simpleNegate( Node n ){
+Node TermUtil::simpleNegate(Node n)
+{
+  Assert(n.getType().isBoolean());
+  NodeManager* nm = NodeManager::currentNM();
   if( n.getKind()==OR || n.getKind()==AND ){
     std::vector< Node > children;
     for (const Node& cn : n)
     {
       children.push_back(simpleNegate(cn));
     }
-    return NodeManager::currentNM()->mkNode( n.getKind()==OR ? AND : OR, children );
+    return nm->mkNode(n.getKind() == OR ? AND : OR, children);
+  }
+  else if (n.isConst())
+  {
+    return nm->mkConst(!n.getConst<bool>());
   }
   return n.negate();
 }