Fix caching in TheoryEngine::getExplanation() (#4736)
authorAndres Noetzli <andres.noetzli@gmail.com>
Tue, 14 Jul 2020 05:11:10 +0000 (22:11 -0700)
committerGitHub <noreply@github.com>
Tue, 14 Jul 2020 05:11:10 +0000 (22:11 -0700)
commitd9c81008606b81fb8f6ef1d3e14fe2479c7efaa2
treea02c6112591acbcbedf953ccb38415fe3d23cd8e
parentc313f4d0863eec16618488649e706ff89439449f
Fix caching in TheoryEngine::getExplanation() (#4736)

Commit 64a7db86206aa0993f75446a3e7f77f3c0c023c6 introduced a caching
mechanism in `TheoryEngine::getExplanation()`. However, there seem to be
issues related to the timestamps of the explanations. This commit fixes
the issue by making the timestamp part of the cache. The change ensures
that explanations for a certain node never rely on other explanations
for that node with a later timestamp.
src/theory/theory_engine.cpp
test/regress/CMakeLists.txt
test/regress/regress0/nl/sin-cos-346-b-chunk-0169.smt2
test/regress/regress1/strings/issue4735.smt2 [new file with mode: 0644]
test/regress/regress1/strings/issue4735_2.smt2 [new file with mode: 0644]