diff options
| -rw-r--r-- | src/theory/strings/term_registry.cpp | 4 | ||||
| -rw-r--r-- | src/theory/strings/term_registry.h | 4 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue5374-proxy-i.smt2 | 15 |
4 files changed, 19 insertions, 5 deletions
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index 2b5daa476..76230bcff 100644 --- 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 06993aa97..a713cc60f 100644 --- 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 cd99823f1..98fde9847 100644 --- 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 index 000000000..89b2d007b --- /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) |