Add test from issue 1008

This commit adds a test suggested by Basile in issue OCamlPro#1008.
Halbaroth · Aug 16, 2024 · 48803a5 · 48803a5
1 parent 0d6300e
commit 48803a5
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 0 deletions.
diff --git a/tests/issues/1008.expected b/tests/issues/1008.expected
@@ -0,0 +1,2 @@
+
+unsat
diff --git a/tests/issues/1008.smt2 b/tests/issues/1008.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+(declare-datatype t ((A) (B (i Int))))
+
+(declare-const e t)
+
+(assert ((_ is B) e))
+(assert (forall ((n Int)) (distinct e (B n))))
+(check-sat)