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 /test/regress | |
parent | 6b9ff0509824bc6faf1dd95981189410a4fa60e4 (diff) |
Fix type enumeration for non first-class sorts in FMF (#6719)
Fixes #6690.
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress1/fmf/issue6690-re-enum.smt2 | 5 |
2 files changed, 6 insertions, 0 deletions
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) |