diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-02 14:25:07 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-12-02 14:25:07 -0600 |
| commit | c3c8d013d2a879eaa1d205e57af32a7f8bb8c0b7 (patch) | |
| tree | f4a8372d8cd693df5f33e8d49cea53dbb418349e /src/theory/theory_model.cpp | |
| parent | 623e701247ed08e3f59d57b18ebe42f4d4db221e (diff) | |
Bug fixes and refactoring of parametric datatypes, add some regressions.
Diffstat (limited to 'src/theory/theory_model.cpp')
| -rw-r--r-- | src/theory/theory_model.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 71d82d5e4..8579ad55f 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -819,7 +819,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) bool isCorecursive = false; if( t.isDatatype() ){ const Datatype& dt = ((DatatypeType)(t).toType()).getDatatype(); - isCorecursive = dt.isCodatatype() && ( !dt.isFinite() || dt.isRecursiveSingleton() ); + isCorecursive = dt.isCodatatype() && ( !dt.isFinite( t.toType() ) || dt.isRecursiveSingleton( t.toType() ) ); } #ifdef CVC4_ASSERTIONS bool isUSortFiniteRestricted = false; |