summaryrefslogtreecommitdiff
path: root/src/theory/subs_minimize.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/subs_minimize.cpp')
-rw-r--r--src/theory/subs_minimize.cpp3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/subs_minimize.cpp b/src/theory/subs_minimize.cpp
index 21862a251..e5e6e392e 100644
--- a/src/theory/subs_minimize.cpp
+++ b/src/theory/subs_minimize.cpp
@@ -17,6 +17,7 @@
#include "expr/node_algorithm.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/rewriter.h"
+#include "theory/strings/word.h"
using namespace std;
using namespace CVC4::kind;
@@ -448,7 +449,7 @@ bool SubstitutionMinimize::isSingularArg(Node n, Kind k, unsigned arg)
if ((arg == 1 && k == STRING_STRCTN) || (arg == 0 && k == STRING_SUBSTR))
{
// empty string
- if (n.getConst<String>().size() == 0)
+ if (strings::Word::getLength(n) == 0)
{
return true;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback