summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2019-09-09 12:47:23 -0500
committerGitHub <noreply@github.com>2019-09-09 12:47:23 -0500
commitb99e0654867bdc40d9c3d30779c0f800d410ea54 (patch)
treee1328dcd11f6a1a75b4a0a0ca5fb5578e57cee46 /src/theory/quantifiers/cegqi/ceg_instantiator.cpp
parent1c09572e0e2031519a103caa2a4af0d9bd34a9c5 (diff)
Fix issue in cegqi related to enum (#3265)
Diffstat (limited to 'src/theory/quantifiers/cegqi/ceg_instantiator.cpp')
-rw-r--r--src/theory/quantifiers/cegqi/ceg_instantiator.cpp2
1 files changed, 1 insertions, 1 deletions
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)
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback