Fix bug in fmc mbqi where modelscomputed for mbqi could involve non-constant values. Add regression.

4 files changed, 34 insertions, 1 deletions

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 027a4573b..018a0c3e0 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -574,6 +574,7 @@ Node FirstOrderModelFmc::getUsedRepresentative(Node n, bool strict) {
         Trace("fmc-warn") << "WARNING : no representative for " << n << std::endl;
       }
     }
+/*
     Node r = getRepresentative(n);
     if( d_model_basis_rep.find(tn)!=d_model_basis_rep.end() ){
       if (r==d_model_basis_rep[tn]) {
@@ -581,6 +582,8 @@ Node FirstOrderModelFmc::getUsedRepresentative(Node n, bool strict) {
       }
     }
     return r;
+*/
+    return getRepresentative(n);
   }
 }
 
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 02c6bbba8..f0858f4e9 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -436,6 +436,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
           Node ri = fm->getUsedRepresentative( c[i]);
           if( !ri.getType().isSort() && !ri.isConst() ){
             Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << std::endl;
+            Assert( false );
           }
           children.push_back(ri);
           if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){
@@ -451,6 +452,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
         Node nv = fm->getUsedRepresentative( v );
         if( !nv.getType().isSort() && !nv.isConst() ){
           Trace("fmc-warn") << "Warning : model has non-constant value in model " << nv << std::endl;
+          Assert( false );
         }
         Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );
         if( std::find(conds.begin(), conds.end(), n )==conds.end() ){
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index d262d624f..8b7202906 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -47,7 +47,8 @@ TESTS =	\
 	fd-false.smt2 \
 	tail_rec.smt2 \
 	jasmin-cdt-crash.smt2 \
-	loopy_coda.smt2
+	loopy_coda.smt2 \
+	fmc_unsound_model.smt2
 
 
 EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/fmf/fmc_unsound_model.smt2 b/test/regress/regress0/fmf/fmc_unsound_model.smt2
new file mode 100644
index 000000000..813f89732
--- /dev/null
+++ b/test/regress/regress0/fmf/fmc_unsound_model.smt2
@@ -0,0 +1,27 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+; this problem produced a model where incorrectly card(a)=1 due to --mbqi=fmc
+(set-logic ALL_SUPPORTED)
+
+(declare-sort a 0)
+(declare-datatypes () ((tree (Leaf (lab a)))))
+
+(declare-sort alpha 0)
+(declare-fun alphabet (tree a) Bool)
+(declare-fun g1 (alpha) tree)
+(declare-fun g2 (alpha) a)
+
+(assert
+ (forall ((x alpha))
+    (=>
+     (= (lab (g1 x)) (g2 x))
+     (alphabet (g1 x) (g2 x)))))
+
+(declare-fun x () a)
+(declare-fun y () a)
+; (assert (= x y))
+(assert
+  (and
+   (exists ((b alpha)) (and (= (Leaf y) (g1 b)) (= x (g2 b))))
+   (not (alphabet (Leaf y) x))))
+(check-sat)