projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: d9bff0c)
Fix mk type const (#1776)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 15 Apr 2018 15:18:34 +0000 (10:18 -0500)
committerAndres Noetzli <andres.noetzli@gmail.com>
Sun, 15 Apr 2018 15:18:34 +0000 (08:18 -0700)
This was a new utility, only used so far by the extended rewriter in EqChain simplification.

src/theory/quantifiers/term_util.cpp patch | blob | history

diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index a8abd41eb782903adaf138ac18c7941a70725782..7cebf0e1edd3422174338172e47233296bbce784 100644 (file)
--- 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)