diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-10 14:09:10 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-10 14:09:10 -0600 |
| commit | 032bee9200bf64af0851832c97ce20b87a6f8e0f (patch) | |
| tree | a170018d996d85fc865e339c699147568afd10b2 /src/CMakeLists.txt | |
| parent | 8ddc6b6a49f81e0390f311b1a9a894c26fa9cc30 (diff) | |
Make mkGroundTerm deterministic (#5347)
This ensures mkGroundTerm is deterministic using attributes.
This was uncovered by failures in the proof checker for datatypes.
Diffstat (limited to 'src/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 7f89b4de3..1a06e9366 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -475,6 +475,7 @@ libcvc4_add_sources( theory/builtin/theory_builtin.h theory/builtin/theory_builtin_rewriter.cpp theory/builtin/theory_builtin_rewriter.h + theory/builtin/theory_builtin_type_rules.cpp theory/builtin/theory_builtin_type_rules.h theory/builtin/type_enumerator.cpp theory/builtin/type_enumerator.h |