diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-06-23 20:23:30 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-23 23:23:30 +0000 |
| commit | 14f613c36fd55b662ce29eeae54a4bc2f26322a4 (patch) | |
| tree | 357b0674d0c996531c2ba6411a5d6f75a116e62b /test/regress/regress0 | |
| parent | 228d35b578404b4931c6b4b9c9a0a199a0a9236e (diff) | |
[hol] Disable bound fmf when HOL (#6792)
Fixes #6536
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/ho/issue6536.smt2 | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/test/regress/regress0/ho/issue6536.smt2 b/test/regress/regress0/ho/issue6536.smt2 new file mode 100644 index 000000000..ed4d453a6 --- /dev/null +++ b/test/regress/regress0/ho/issue6536.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: unknown +(set-logic HO_ALL) +(declare-datatypes ((a 0) (b 0)) (((c) (d)) ((h (j b)) (e)))) +(declare-fun f () b) +(declare-fun k (a) b) +(declare-fun g (b b) b) +(assert (forall ((i a)) (distinct (k i) (ite ((_ is c) i) e (ite ((_ is d) i) (h (g (k i) (k i))) f))))) +(check-sat) |