From d9c81008606b81fb8f6ef1d3e14fe2479c7efaa2 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
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/CMakeLists.txt                        |  2 ++
 .../regress0/nl/sin-cos-346-b-chunk-0169.smt2      |  2 +-
 test/regress/regress1/strings/issue4735.smt2       | 27 ++++++++++++++++++++++
 test/regress/regress1/strings/issue4735_2.smt2     |  8 +++++++
 4 files changed, 38 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress1/strings/issue4735.smt2
 create mode 100644 test/regress/regress1/strings/issue4735_2.smt2

(limited to 'test/regress')

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 18bf6d104..5072e5a17 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1801,6 +1801,8 @@ set(regress_1_tests
   regress1/strings/issue3657-unexpectedUnsatCVC4.smt2
   regress1/strings/issue4379.smt2
   regress1/strings/issue4608-re-derive.smt2
+  regress1/strings/issue4735.smt2
+  regress1/strings/issue4735_2.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2
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)
diff --git a/test/regress/regress1/strings/issue4735.smt2 b/test/regress/regress1/strings/issue4735.smt2
new file mode 100644
index 000000000..d0c9aeedc
--- /dev/null
+++ b/test/regress/regress1/strings/issue4735.smt2
@@ -0,0 +1,27 @@
+; COMMAND-LINE: --strings-fmf
+; EXPECT: sat
+(set-logic QF_S)
+(declare-fun a () String)
+(declare-fun b () Int)
+(declare-fun c () String)
+(declare-fun d () String)
+(declare-fun e () String)
+(declare-fun f () String)
+(declare-fun g () String)
+(declare-fun h () String)
+(declare-fun i () Bool)
+(declare-fun j () String)
+(declare-fun k () String)
+(assert (= e "0000000000"))
+(assert (distinct a d))
+(assert
+ (ite (distinct b 0)
+ (and (= (str.++ d e) (str.++ c j))
+  (= (str.len c) 2)
+  (= j (str.++ f k))
+  (= f (str.++ g h))
+  (str.in_re g (str.to_re "A")))
+ (str.in_re j (str.to_re ""))))
+(assert (distinct i (= b 0)))
+(assert i)
+(check-sat)
diff --git a/test/regress/regress1/strings/issue4735_2.smt2 b/test/regress/regress1/strings/issue4735_2.smt2
new file mode 100644
index 000000000..2c92a5150
--- /dev/null
+++ b/test/regress/regress1/strings/issue4735_2.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --strings-fmf
+; EXPECT: sat
+(set-logic QF_S)
+(declare-fun a () String)
+(declare-fun b () String)
+(assert (distinct b (str.++ a a)))
+(assert (str.in_re (str.++ b "\x2f" b) (re.++ (re.opt re.allchar) (str.to_re "\x2f\x65") re.all)))
+(check-sat)
-- 
cgit v1.2.3