From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 25 Jun 2015 12:06:06 +0000 (+0200)
Subject: Do not assert fail for fmf empty domains. Fixes bug 644.
X-Git-Tag: cvc5-1.0.0~6267^2~12
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e4cff69e3b565e928dbf04960249477ce2c9ef6b;p=cvc5.git

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 5cb8cf278..346631889 100644
--- 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;
       }