diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sets/finite-type/bug3663.smt2 | 8 |
2 files changed, 9 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index aeca8e720..20272de2b 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1598,6 +1598,7 @@ set(regress_1_tests regress1/sets/comp-pos-member.smt2 regress1/sets/copy_check_heap_access_33_4.smt2 regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 + regress1/sets/finite-type/bug3663.smt2 regress1/sets/finite-type/sets-card-arrcolor.smt2 regress1/sets/finite-type/sets-card-arrunit.smt2 regress1/sets/finite-type/sets-card-bool-1.smt2 diff --git a/test/regress/regress1/sets/finite-type/bug3663.smt2 b/test/regress/regress1/sets/finite-type/bug3663.smt2 new file mode 100644 index 000000000..5aef5d15d --- /dev/null +++ b/test/regress/regress1/sets/finite-type/bug3663.smt2 @@ -0,0 +1,8 @@ +;EXIT: 1 +;EXPECT: (error "The cardinality beth[0] of the finite type a is not supported yet.") +(set-logic ALL) +(set-option :fmf-fun true) +(declare-sort a 0) +(declare-const b (Set a)) +(assert (= (card b) 0)) +(check-sat) |