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 50a0084fc..a12fc7ca2 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -1039,7 +1039,7 @@ int QModelBuilderInstGen::getSelectionFormulaScore( Node fn ){ if( fn.getKind()==APPLY_UF ){ Node op = fn.getOperator(); //return total number of terms - return d_qe->getTermDatabase()->d_op_count[op]; + return d_qe->getTermDatabase()->d_op_nonred_count[op]; }else{ int score = 0; for( size_t i=0; i<fn.getNumChildren(); i++ ){ |