diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-08 20:03:39 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-08 18:03:39 -0700 |
| commit | d0559a21f2ca71e8eaf5978e5c0707d7cf11499f (patch) | |
| tree | 4846f9bc1469e22699c1ec98aa161d17f73453c6 /test | |
| parent | 55acdeb493ee3f9b66ed38f7526670b6e66c46bd (diff) | |
Fix string register extended terms (#2597)
A regress2 benchmark was failing, due to a recent change in our strings rewriter.
The issue is that our string rewriter is now powerful enough to deduce that certain extended terms like `(str.substr (str.++ x "zb") 1 1)` must be non-empty. As a consequence, our emptiness-split `(str.substr (str.++ x "zb") 1 1) = "" OR len( (str.substr (str.++ x "zb") 1 1) ) > 0` is instead a propagation `len( (str.substr (str.++ x "zb") 1 1) ) > 0`. This means that `(str.substr (str.++ x "zb") 1 1)` may not appear in an assertion sent to strings.
The fix is to ensure that extended function terms in any assertions *or shared terms* are registered.
This also simplifies the code so that another (now spurious) call to ExtTheory::registerTermRec is removed.
Diffstat (limited to 'test')
0 files changed, 0 insertions, 0 deletions