Update strings proxy variable map to be context independent (#5377)

This makes strings proxy variables map to be context-independent. They should be context independent since we are using attributes to mark proxy variables, which are context-independent. This led to the crash reported on #5374 since proxy variables would persist across multiple user contexts, but would be missing in the user-context dependent map.

This fixes #5374.

diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 2b5daa476103a958a7ee95f433f59c938d7d8cf4..76230bcffb0812a80c23b2d20ebbd9aec8291198 100644 (file)
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -49,8 +49,6 @@ TermRegistry::TermRegistry(SolverState& s,
       d_preregisteredTerms(s.getUserContext()),
       d_registeredTerms(s.getUserContext()),
       d_registeredTypes(s.getUserContext()),
-      d_proxyVar(s.getUserContext()),
-      d_proxyVarToLength(s.getUserContext()),
       d_lengthLemmaTermsCache(s.getUserContext()),
       d_epg(pnm ? new EagerProofGenerator(
                       pnm,
@@ -567,7 +565,7 @@ Node TermRegistry::getSymbolicDefinition(Node n, std::vector<Node>& exp) const
 
 Node TermRegistry::getProxyVariableFor(Node n) const
 {
-  NodeNodeMap::const_iterator it = d_proxyVar.find(n);
+  std::map<Node, Node>::const_iterator it = d_proxyVar.find(n);
   if (it != d_proxyVar.end())
   {
     return (*it).second;

diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h
index 06993aa975953b1b6878aadf6bfb6ba631a8dc2d..a713cc60f3bfdaa62948ecc6295e67a90acd2477 100644 (file)
--- a/src/theory/strings/term_registry.h
+++ b/src/theory/strings/term_registry.h
@@ -249,12 +249,12 @@ class TermRegistry
    * which rewrites to 3 = 3.
    * In the above example, we store "ABC" -> v_{"ABC"} in this map.
    */
-  NodeNodeMap d_proxyVar;
+  std::map<Node, Node> d_proxyVar;
   /**
    * Map from proxy variables to their normalized length. In the above example,
    * we store "ABC" -> 3.
    */
-  NodeNodeMap d_proxyVarToLength;
+  std::map<Node, Node> d_proxyVarToLength;
   /** List of terms that we have register length for */
   NodeSet d_lengthLemmaTermsCache;
   /** Proof generator, manages proofs for lemmas generated by this class */

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index cd99823f1b42b2fa87c19047b2e0385393288132..98fde98470a82108e033a29df18b33289576e373 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1844,6 +1844,7 @@ set(regress_1_tests
   regress1/strings/issue4735.smt2
   regress1/strings/issue4735_2.smt2
   regress1/strings/issue4759-comp-delta.smt2
+  regress1/strings/issue5374-proxy-i.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2

diff --git a/test/regress/regress1/strings/issue5374-proxy-i.smt2 b/test/regress/regress1/strings/issue5374-proxy-i.smt2
new file mode 100644 (file)
index 0000000..89b2d00
--- /dev/null
+++ b/test/regress/regress1/strings/issue5374-proxy-i.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: -i
+; EXPECT: sat
+(set-logic QF_UFSLIA)
+(set-option :strings-lazy-pp false)
+(declare-fun str0 () String)
+(declare-fun str4 () String)
+(declare-fun str15 () String)
+(push 1)
+(assert (str.in_re (str.replace str0 "gpQrbuIlpcirZXw" "") (str.to_re "")))
+(push 1)
+(check-sat)
+(pop 1)
+(pop 1)
+(assert (distinct str15 str4 (str.replace str0 "gpQrbuIlpcirZXw" "") ""))
+(push 1)