From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sun, 15 Apr 2018 15:18:34 +0000 (-0500)
Subject: Fix mk type const (#1776)
X-Git-Tag: cvc5-1.0.0~5149
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c22c31b0dfab057cd41cd276852d27d905274c9a;p=cvc5.git

Fix mk type const (#1776)

This was a new utility, only used so far by the extended rewriter in EqChain simplification.
---

diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index a8abd41eb..7cebf0e1e 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -919,7 +919,7 @@ Node TermUtil::getTypeValueOffset(TypeNode tn,
 
 Node TermUtil::mkTypeConst(TypeNode tn, bool pol)
 {
-  return pol ? mkTypeValue(tn, 0) : mkTypeMaxValue(tn);
+  return pol ? mkTypeMaxValue(tn) : mkTypeValue(tn, 0);
 }
 
 bool TermUtil::isAntisymmetric(Kind k, Kind& dk)