From 48803a55be55d92fe63cfdde143c321265645362 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Fri, 16 Aug 2024 18:04:22 +0200
Subject: [PATCH] Add test from issue 1008

This commit adds a test suggested by Basile in issue #1008.
---
 tests/issues/1008.expected | 2 ++
 tests/issues/1008.smt2     | 8 ++++++++
 2 files changed, 10 insertions(+)
 create mode 100644 tests/issues/1008.expected
 create mode 100644 tests/issues/1008.smt2

diff --git a/tests/issues/1008.expected b/tests/issues/1008.expected
new file mode 100644
index 000000000..6f99ff0f4
--- /dev/null
+++ b/tests/issues/1008.expected
@@ -0,0 +1,2 @@
+
+unsat
diff --git a/tests/issues/1008.smt2 b/tests/issues/1008.smt2
new file mode 100644
index 000000000..b9540ba7f
--- /dev/null
+++ 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)