diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 3 | ||||
| -rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 2 |
2 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 027a4573b..018a0c3e0 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -574,6 +574,7 @@ Node FirstOrderModelFmc::getUsedRepresentative(Node n, bool strict) { Trace("fmc-warn") << "WARNING : no representative for " << n << std::endl; } } +/* Node r = getRepresentative(n); if( d_model_basis_rep.find(tn)!=d_model_basis_rep.end() ){ if (r==d_model_basis_rep[tn]) { @@ -581,6 +582,8 @@ Node FirstOrderModelFmc::getUsedRepresentative(Node n, bool strict) { } } return r; +*/ + return getRepresentative(n); } } diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 02c6bbba8..f0858f4e9 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -436,6 +436,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ Node ri = fm->getUsedRepresentative( c[i]); if( !ri.getType().isSort() && !ri.isConst() ){ Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << std::endl; + Assert( false ); } children.push_back(ri); if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){ @@ -451,6 +452,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ Node nv = fm->getUsedRepresentative( v ); if( !nv.getType().isSort() && !nv.isConst() ){ Trace("fmc-warn") << "Warning : model has non-constant value in model " << nv << std::endl; + Assert( false ); } Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children ); if( std::find(conds.begin(), conds.end(), n )==conds.end() ){ |