diff options
Diffstat (limited to 'src/theory/quantifiers/model_builder.cpp')
| -rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index a5ec16e3a..090f2735a 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -674,7 +674,7 @@ int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ std::vector< Node > tr_terms; if( lit.getKind()==APPLY_UF ){ //only match predicates that are contrary to this one, use literal matching - Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false ); + Node eq = NodeManager::currentNM()->mkNode( EQUAL, lit, !phase ? fm->d_true : fm->d_false ); tr_terms.push_back( eq ); }else if( lit.getKind()==EQUAL ){ //collect trigger terms |