From 233ac54348e8ae1dced68a4b574addc5ca543083 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Tue, 8 Oct 2024 11:47:58 +0200
Subject: [PATCH] Remove duplicated tests

---
 tests/issues/854/function.expected |  8 --------
 tests/issues/854/function.smt2     | 13 -------------
 tests/issues/854/original.expected |  7 -------
 tests/issues/854/original.smt2     | 11 -----------
 tests/issues/854/twice_eq.expected |  8 --------
 tests/issues/854/twice_eq.smt2     | 13 -------------
 6 files changed, 60 deletions(-)
 delete mode 100644 tests/issues/854/function.expected
 delete mode 100644 tests/issues/854/function.smt2
 delete mode 100644 tests/issues/854/original.expected
 delete mode 100644 tests/issues/854/original.smt2
 delete mode 100644 tests/issues/854/twice_eq.expected
 delete mode 100644 tests/issues/854/twice_eq.smt2

diff --git a/tests/issues/854/function.expected b/tests/issues/854/function.expected
deleted file mode 100644
index 63577badc..000000000
--- a/tests/issues/854/function.expected
+++ /dev/null
@@ -1,8 +0,0 @@
-
-unknown
-(
-  (define-fun a () Int 0)
-  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref))
-  (define-fun f ((_arg_0 Int)) Int 0)
-  (define-fun a1 () Int 0)
-)
diff --git a/tests/issues/854/function.smt2 b/tests/issues/854/function.smt2
deleted file mode 100644
index 57ef18bcd..000000000
--- a/tests/issues/854/function.smt2
+++ /dev/null
@@ -1,13 +0,0 @@
-(set-logic ALL)
-(set-info :smt-lib-version 2.6)
-(set-option :produce-models true)
-(declare-sort intref 0)
-(declare-fun intrefqtmk (Int) intref)
-(declare-fun a () Int)
-(declare-fun f (Int) Int)
-(define-fun aqtunused ((_x Int)) intref (intrefqtmk (f a)))
-(assert (= (aqtunused 0) (aqtunused 1)))
-(declare-fun a1 () Int)
-(assert (not (and (<= 5 a1) (<= a1 15))))
-(check-sat)
-(get-model)
diff --git a/tests/issues/854/original.expected b/tests/issues/854/original.expected
deleted file mode 100644
index a0ce9f571..000000000
--- a/tests/issues/854/original.expected
+++ /dev/null
@@ -1,7 +0,0 @@
-
-unknown
-(
-  (define-fun a () Int 0)
-  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a3 intref))
-  (define-fun a1 () Int 0)
-)
diff --git a/tests/issues/854/original.smt2 b/tests/issues/854/original.smt2
deleted file mode 100644
index fd66489a1..000000000
--- a/tests/issues/854/original.smt2
+++ /dev/null
@@ -1,11 +0,0 @@
-(set-logic ALL)
-(set-info :smt-lib-version 2.6)
-(set-option :produce-models true)
-(declare-sort intref 0)
-(declare-fun intrefqtmk (Int) intref)
-(declare-fun a () Int)
-(define-fun aqtunused () intref (intrefqtmk a))
-(declare-fun a1 () Int)
-(assert (not (and (<= 5 a1) (<= a1 15))))
-(check-sat)
-(get-model)
diff --git a/tests/issues/854/twice_eq.expected b/tests/issues/854/twice_eq.expected
deleted file mode 100644
index 3488c940f..000000000
--- a/tests/issues/854/twice_eq.expected
+++ /dev/null
@@ -1,8 +0,0 @@
-
-unknown
-(
-  (define-fun a () Int 0)
-  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref))
-  (define-fun another_mk ((_arg_0 Int)) intref (as @a4 intref))
-  (define-fun a1 () Int 0)
-)
diff --git a/tests/issues/854/twice_eq.smt2 b/tests/issues/854/twice_eq.smt2
deleted file mode 100644
index eaac2b8d6..000000000
--- a/tests/issues/854/twice_eq.smt2
+++ /dev/null
@@ -1,13 +0,0 @@
-(set-logic ALL)
-(set-info :smt-lib-version 2.6)
-(set-option :produce-models true)
-(declare-sort intref 0)
-(declare-fun intrefqtmk (Int) intref)
-(declare-fun another_mk (Int) intref)
-(declare-fun a () Int)
-(define-fun aqtunused () intref (intrefqtmk a))
-(assert (= aqtunused (another_mk a)))
-(declare-fun a1 () Int)
-(assert (not (and (<= 5 a1) (<= a1 15))))
-(check-sat)
-(get-model)