diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 9e14d6a3f..5b7c38361 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -264,6 +264,9 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) // assert the (relevant) portion of the equality engine to the model if (!m->assertEqualityEngine(&d_equalityEngine, &termSet)) { + Unreachable() + << "TheoryStrings::collectModelInfo: failed to assert equality engine" + << std::endl; return false; } @@ -423,6 +426,8 @@ bool TheoryStrings::collectModelInfoType( uint32_t currLen = lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt(); std::unique_ptr<SEnumLen> sel; + Trace("strings-model") << "Cardinality of alphabet is " + << utils::getAlphabetCardinality() << std::endl; if (tn.isString()) { sel.reset(new StringEnumLen( @@ -474,7 +479,10 @@ bool TheoryStrings::collectModelInfoType( Node spl = nm->mkNode(OR, sl, sl.negate()); ++(d_statistics.d_lemmasCmiSplit); d_out->lemma(spl); + Trace("strings-lemma") + << "Strings::CollectModelInfoSplit: " << spl << std::endl; } + // we added a lemma, so can return here return false; } c = sel->getCurrent(); @@ -491,6 +499,11 @@ bool TheoryStrings::collectModelInfoType( processed[eqc] = c; if (!m->assertEquality(eqc, c, true)) { + // this should never happen due to the model soundness argument + // for strings + Unreachable() + << "TheoryStrings::collectModelInfoType: Inconsistent equality" + << std::endl; return false; } } @@ -534,6 +547,12 @@ bool TheoryStrings::collectModelInfoType( processed[nodes[i]] = cc; if (!m->assertEquality(nodes[i], cc, true)) { + // this should never happen due to the model soundness argument + // for strings + + Unreachable() << "TheoryStrings::collectModelInfoType: " + "Inconsistent equality (unprocessed eqc)" + << std::endl; return false; } } |