diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-06-22 11:51:07 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-22 16:51:07 +0000 |
| commit | 43106313622c0f147459bef44d25025335b6b4a5 (patch) | |
| tree | 2b323d61fef3e542cac5cbdf537381f72a1c9acd | |
| parent | 6b9ff0509824bc6faf1dd95981189410a4fa60e4 (diff) | |
Fix type enumeration for non first-class sorts in FMF (#6719)
Fixes #6690.
| -rw-r--r-- | src/theory/quantifiers/fmf/full_model_check.cpp | 5 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/fmf/issue6690-re-enum.smt2 | 5 |
3 files changed, 9 insertions, 2 deletions
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) |