diff options
| author | ayveejay <41393247+ayveejay@users.noreply.github.com> | 2018-08-01 03:25:51 +0100 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-07-31 19:25:51 -0700 |
| commit | ad61299aa24a83f935daedab32440d25006e18bb (patch) | |
| tree | 82540951afd070cc43f3e7ea87fc9b8c8e9311b8 /test/system/Makefile.am | |
| parent | 049bc7acdb7ecc50719175652028a51a8f996502 (diff) | |
Improvements and tests for the API around separation logic (#2229)
- Introduces a system that validating that, when not using THEORY_SEP, that it is not possible to
obtain the separation logic heap/nil (validate_exception())
- Introduces a system test demonstrating how to use the separation logic theory, and then how
to use the "getters" to obtain and interrogate the heap/nil expressions (validate_getters())
- Refactors the original getters to avoid duplicate code
- Add a check as part of the getters to ensure that THEORY_SEP is in use
Diffstat (limited to 'test/system/Makefile.am')
| -rw-r--r-- | test/system/Makefile.am | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test/system/Makefile.am b/test/system/Makefile.am index 1be242e3d..ed52b0232 100644 --- a/test/system/Makefile.am +++ b/test/system/Makefile.am @@ -6,7 +6,8 @@ CPLUSPLUS_TESTS = \ reset_assertions \ two_smt_engines \ smt2_compliance \ - statistics + statistics \ + sep_log_api if CVC4_BUILD_LIBCOMPAT #CPLUSPLUS_TESTS += \ |