Add test from issue 1008 (#1211)

* Add tests from issue 1008 This commit adds tests suggested by Basile in issue #1008.
OCamlPro · Aug 20, 2024 · dbfb6ad · dbfb6ad
1 parent 77e01eb
commit dbfb6ad
Show file tree

Hide file tree

Showing 4 changed files with 20 additions and 0 deletions.
diff --git a/tests/issues/1008/adt.expected b/tests/issues/1008/adt.expected
@@ -0,0 +1,2 @@
+
+unsat
diff --git a/tests/issues/1008/adt.smt2 b/tests/issues/1008/adt.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)
diff --git a/tests/issues/1008/record.expected b/tests/issues/1008/record.expected
@@ -0,0 +1,2 @@
+
+unknown
diff --git a/tests/issues/1008/record.smt2 b/tests/issues/1008/record.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+(declare-datatype t ((B (i Int))))
+
+(declare-const e t)
+
+(assert ((_ is B) e))
+(assert (forall ((n Int)) (distinct e (B n))))
+(check-sat)