diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2018-10-31 16:10:04 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2018-10-31 16:10:04 -0500 |
| commit | 92dfe34ca1537391328f441ecb8e86f41f55edd4 (patch) | |
| tree | 41bee6fcaaec4b14dfd220ad7b77b82fa05e2d1f /src | |
| parent | 808a3acef1d21c0fd4fdb99d13ab9341d46a56a1 (diff) | |
Fix
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/quantifiers/extended_rewrite.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index afe5595e0..656eceac9 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -2681,7 +2681,7 @@ int ExtendedRewriter::bitVectorSubsume(Node a, Node b, bool strict, bool tryNot) //--------------recurse extract if (ak == BITVECTOR_EXTRACT && bk == BITVECTOR_EXTRACT - && a.getOperator() == b.getOperator()) + && a.getOperator() == b.getOperator() && a[0].getType()==b[0].getType()) { return bitVectorSubsume(a[0], b[0], strict); } |