Do not assert fail for fmf empty domains. Fixes bug 644.

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 5cb8cf27806f6965c59f72672e7015cd8f22d674..3466318897d7a3a2563a1776e8237ffb721c57ce 100644 (file)
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -675,10 +675,11 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
       //check if it is a constant introduced as a representative not existing in the model's equality engine
       if( !d_rep_set.hasRep( tn, v ) ){
         if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && !d_rep_set.d_type_reps[ tn ].empty() ){
-          //see full_model_check.cpp line 366
           v = d_rep_set.d_type_reps[tn][ d_rep_set.d_type_reps[tn].size()-1 ];
         }else{
-          Assert( false );
+          //can happen for types not involved in quantified formulas
+          Trace("fmc-model-func") << "No type rep for " << tn << std::endl;
+          v = d_qe->getTermDatabase()->getEnumerateTerm( tn, 0 );
         }
         Trace("fmc-model-func") << "No term, assign " << v << std::endl;
       }