diff options
Diffstat (limited to 'src/theory/strings/base_solver.cpp')
| -rw-r--r-- | src/theory/strings/base_solver.cpp | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 128893cf0..af0e7cc37 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -35,7 +35,6 @@ BaseSolver::BaseSolver(context::Context* c, d_emptyString = NodeManager::currentNM()->mkConst(::CVC4::String("")); d_false = NodeManager::currentNM()->mkConst(false); d_cardSize = utils::getAlphabetCardinality(); - d_type = NodeManager::currentNM()->stringType(); } BaseSolver::~BaseSolver() {} @@ -254,7 +253,7 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti, if (!n.isNull()) { // construct the constant - Node c = utils::mkNConcat(vecc, d_type); + Node c = utils::mkNConcat(vecc, n.getType()); if (!d_state.areEqual(n, c)) { if (Trace.isOn("strings-debug")) |