From 43106313622c0f147459bef44d25025335b6b4a5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 22 Jun 2021 11:51:07 -0500 Subject: [PATCH] Fix type enumeration for non first-class sorts in FMF (#6719) Fixes #6690. --- src/theory/quantifiers/fmf/full_model_check.cpp | 5 +++-- test/regress/CMakeLists.txt | 1 + test/regress/regress1/fmf/issue6690-re-enum.smt2 | 5 +++++ 3 files changed, 9 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress1/fmf/issue6690-re-enum.smt2 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) -- 2.30.2