More preparation for CASC proofs. Minor fix for sort inference (rewrite new assertions). Bug fix for ambqi : simplify correctly for multi-sorted case. Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real.

1 files changed, 3 insertions, 1 deletions

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 0f3e53827..63df56392 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -61,7 +61,7 @@ bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) {
         return true;
       }
     }
-    if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !c[index].getType().isInteger() ){
+    if( c[index].getType().isSort() ){
       //for star: check if all children are defined and have generalizations
       if( c[index]==st ){     ///options::fmfFmcCoverSimplify()
         //check if all children exist and are complete
@@ -537,7 +537,9 @@ void FullModelChecker::initializeType( FirstOrderModelFmc * fm, TypeNode tn ){
     }else{
       mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn);
     }
+    Trace("fmc") << "Get used rep for " << mbn << std::endl;
     Node mbnr = fm->getUsedRepresentative( mbn );
+    Trace("fmc") << "...got  " << mbnr << std::endl;
     fm->d_model_basis_rep[tn] = mbnr;
     Trace("fmc") << "Add model basis for type " << tn << " : " << mbn << " " << mbnr << std::endl;
   }