diff options
| -rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.cpp | 2 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 7 |
2 files changed, 8 insertions, 1 deletions
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index ef6926bcb..cafa4a749 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -275,7 +275,7 @@ void BoundedIntegers::process( Node q, Node n, bool pol, bool BoundedIntegers::needsCheck(Theory::Effort e) { - return e == Theory::EFFORT_FULL; + return e == Theory::EFFORT_LAST_CALL; } void BoundedIntegers::check(Theory::Effort e, QEffort quant_e) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 71a0ef63a..d6d137eb7 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3891,6 +3891,13 @@ void TheoryStrings::registerTerm( Node n, int effort ) { Trace("strings-assert") << "(assert " << lem << ")" << std::endl; d_out->lemma(lem); } + else if (n.getKind() == STRING_STRIDOF) + { + Node lem = nm->mkNode(OR, nm->mkNode(EQUAL, n, d_neg_one), nm->mkNode(GEQ, n, n[2])); + Trace("strings-lemma") << "Strings::Lemma STRIDOF : " << lem << std::endl; + Trace("strings-assert") << "(assert " << lem << ")" << std::endl; + d_out->lemma(lem); + } } void TheoryStrings::sendInternalInference(std::vector<Node>& exp, |