summaryrefslogtreecommitdiff
path: root/src/theory/strings
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings')
-rw-r--r--src/theory/strings/theory_strings.cpp4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 9fad39b6b..7d10cbadc 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -4112,7 +4112,9 @@ void TheoryStrings::registerTerm( Node n, int effort ) {
Node len = utils::mkNLength(n[0]);
Node lem = nm->mkNode(AND,
nm->mkNode(GEQ, n, nm->mkConst(Rational(-1))),
- nm->mkNode(LT, n, len));
+ nm->mkNode(LEQ, n, len));
+ Trace("strings-lemma") << "Strings::Lemma IDOF range : " << lem
+ << std::endl;
d_out->lemma(lem);
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback