diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-07-13 22:11:10 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-13 22:11:10 -0700 |
| commit | d9c81008606b81fb8f6ef1d3e14fe2479c7efaa2 (patch) | |
| tree | a02c6112591acbcbedf953ccb38415fe3d23cd8e /test/regress/regress0 | |
| parent | c313f4d0863eec16618488649e706ff89439449f (diff) | |
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.
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/nl/sin-cos-346-b-chunk-0169.smt2 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/regress0/nl/sin-cos-346-b-chunk-0169.smt2 b/test/regress/regress0/nl/sin-cos-346-b-chunk-0169.smt2 index 65e705fa3..2ec7d76f0 100644 --- a/test/regress/regress0/nl/sin-cos-346-b-chunk-0169.smt2 +++ b/test/regress/regress0/nl/sin-cos-346-b-chunk-0169.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-models +; COMMAND-LINE: --no-check-models --nl-ext-tplanes ; EXPECT: sat (set-info :smt-lib-version 2.6) (set-logic QF_NRA) |