diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-22 15:48:25 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-22 20:48:25 +0000 |
| commit | 4929b5dcfaba1e051309a0debfeaf9f8bf8e2d8b (patch) | |
| tree | 467f72854fdc931f1d2ffc9124ab2fa841874d93 /src/theory | |
| parent | b3774c9758b6a23c8ef5d98eaa0879a814114674 (diff) | |
Add more abduction regressions (#7461)
Fixes #5848.
This also fixes an issue leftover from #6605 where a spurious assertion failure was thrown.
Also introduces subfolder regress/regress1/abduction.
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/builtin/theory_builtin_type_rules.cpp b/src/theory/builtin/theory_builtin_type_rules.cpp index f3c595720..1888069bc 100644 --- a/src/theory/builtin/theory_builtin_type_rules.cpp +++ b/src/theory/builtin/theory_builtin_type_rules.cpp @@ -42,7 +42,8 @@ typedef expr::Attribute<GroundTermAttributeId, Node> GroundTermAttribute; Node SortProperties::mkGroundTerm(TypeNode type) { - Assert(type.getKind() == kind::SORT_TYPE); + // we typically use this method for sorts, although there are other types + // where it is used as well, e.g. arrays that are not closed enumerable. GroundTermAttribute gta; if (type.hasAttribute(gta)) { |