From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 22 Jun 2021 16:51:07 +0000 (-0500)
Subject: Fix type enumeration for non first-class sorts in FMF (#6719)
X-Git-Tag: cvc5-1.0.0~1573
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=43106313622c0f147459bef44d25025335b6b4a5;p=cvc5.git

Fix type enumeration for non first-class sorts in FMF (#6719)

Fixes #6690.
---

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 808db7aec..c6f38f298 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -941,8 +941,9 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
   else if( n.getNumChildren()==0 ){
     Node r = n;
     if( !n.isConst() ){
-      if( !fm->hasTerm(n) ){
-        r = getSomeDomainElement(fm, n.getType() );
+      TypeNode tn = n.getType();
+      if( !fm->hasTerm(n) && tn.isFirstClass() ){
+        r = getSomeDomainElement(fm, tn );
       }
       r = fm->getRepresentative( r );
     }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 444e4c7f6..ca281af7b 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1590,6 +1590,7 @@ set(regress_1_tests
   regress1/fmf/issue4068-si-qf.smt2
   regress1/fmf/issue4225-univ-fun.smt2
   regress1/fmf/issue5738-dt-interp-finite.smt2
+  regress1/fmf/issue6690-re-enum.smt2
   regress1/fmf/issue916-fmf-or.smt2
   regress1/fmf/jasmin-cdt-crash.smt2
   regress1/fmf/loopy_coda.smt2
diff --git a/test/regress/regress1/fmf/issue6690-re-enum.smt2 b/test/regress/regress1/fmf/issue6690-re-enum.smt2
new file mode 100644
index 000000000..35c8eabc7
--- /dev/null
+++ b/test/regress/regress1/fmf/issue6690-re-enum.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status unsat)
+(set-option :finite-model-find true)
+(assert (forall ((a String)) (forall ((b String)) (str.in_re a (re.++ re.allchar (str.to_re b))))))
+(check-sat)