diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-23 14:28:29 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-23 14:28:29 -0500 |
| commit | b13d2f7921a65b8921ef37b38a2d4579f7c911a2 (patch) | |
| tree | df7e49fb4318fe58631ca4c4305125dd4fc32afe /src/theory/theory_model.cpp | |
| parent | c254649c8dadd9f0d94f09bf46b21f93b2c67c07 (diff) | |
Fix related to parametric sorts whose interpretation is finite due to uninterpreted sorts + FMF. Generalizes previous fix in term registration visitor.
Diffstat (limited to 'src/theory/theory_model.cpp')
| -rw-r--r-- | src/theory/theory_model.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index fa7e497e2..6889d1002 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -832,6 +832,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF); Node n; if (t.getCardinality().isInfinite()) { + // if (!t.isInterpretedFinite()) { bool success; do{ Trace("model-builder-debug") << "Enumerate term of type " << t << std::endl; |