diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-03-26 08:52:40 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-03-26 08:52:40 -0700 |
| commit | 11c698936c10321db68131eb95e8648a20051e3a (patch) | |
| tree | f81a21dda693780d3211881448323ecc57f1bf3e /test/unit/Makefile.am | |
| parent | f7e0adeae28bae50632edef3ed2325df67a7ee7a (diff) | |
Rewrites for substr of strings of length one (#1712)
This commit adds a rewrite for substrings of strings of length one to
the empty string if it can be shown that it is not possible that the
start position and the length are both greater than zero:
```
(str.substr "A" x y) --> "" if x = 0 |= 0 >= y
```
The commit introduces a set of functions to check such entailments
with assumptions.
Diffstat (limited to 'test/unit/Makefile.am')
| -rw-r--r-- | test/unit/Makefile.am | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 3d5f2702d..b445583ac 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -7,14 +7,15 @@ UNIT_TESTS = \ if WHITE_AND_BLACK_TESTS UNIT_TESTS += \ theory/logic_info_white \ - theory/theory_engine_white \ - theory/theory_black \ - theory/theory_white \ theory/theory_arith_white \ - theory/theory_bv_white \ + theory/theory_black \ theory/theory_bv_bvgauss_white \ + theory/theory_bv_white \ + theory/theory_engine_white \ theory/theory_quantifiers_bv_instantiator_white \ theory/theory_quantifiers_bv_inverter_white \ + theory/theory_strings_rewriter_white \ + theory/theory_white \ theory/type_enumerator_white \ expr/node_white \ expr/node_black \ |