From d9c81008606b81fb8f6ef1d3e14fe2479c7efaa2 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 13 Jul 2020 22:11:10 -0700 Subject: 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. --- test/regress/regress0/nl/sin-cos-346-b-chunk-0169.smt2 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test/regress/regress0/nl') 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) -- cgit v1.2.3