From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 9 Sep 2019 17:47:23 +0000 (-0500)
Subject: Fix issue in cegqi related to enum (#3265)
X-Git-Tag: cvc5-1.0.0~3970
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b99e0654867bdc40d9c3d30779c0f800d410ea54;p=cvc5.git

Fix issue in cegqi related to enum (#3265)
---

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 67985527e..104e40d8b 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -77,7 +77,7 @@ CegTermType mkNegateCTT(CegTermType c)
 }
 bool isStrictCTT(CegTermType c)
 {
-  return c == CEG_TT_LOWER_STRICT && c == CEG_TT_UPPER_STRICT;
+  return c == CEG_TT_LOWER_STRICT || c == CEG_TT_UPPER_STRICT;
 }
 bool isLowerBoundCTT(CegTermType c)
 {