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 /src/theory/ext_theory.cpp | |
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 'src/theory/ext_theory.cpp')
-rw-r--r-- | src/theory/ext_theory.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp index 7cc8627eb..589ec45c0 100644 --- a/src/theory/ext_theory.cpp +++ b/src/theory/ext_theory.cpp @@ -427,6 +427,7 @@ void ExtTheory::registerTermRec(Node n) // mark reduced void ExtTheory::markReduced(Node n, bool contextDepend) { + Trace("extt-debug") << "Mark reduced " << n << std::endl; registerTerm(n); Assert(d_ext_func_terms.find(n) != d_ext_func_terms.end()); d_ext_func_terms[n] = false; |