summaryrefslogtreecommitdiff
path: root/src/theory/theory_model.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_model.cpp')
-rw-r--r--src/theory/theory_model.cpp2
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback