From 27794bcd48ff5095b18b9b4c58f8611f6e41b980 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Tue, 8 Oct 2024 18:20:58 +0200
Subject: [PATCH] pew pew

---
 tests/models/issues/719.err.expected |  3 ---
 tests/models/issues/719.err.smt2     | 19 -------------------
 2 files changed, 22 deletions(-)
 delete mode 100644 tests/models/issues/719.err.expected
 delete mode 100644 tests/models/issues/719.err.smt2

diff --git a/tests/models/issues/719.err.expected b/tests/models/issues/719.err.expected
deleted file mode 100644
index 1b1ed6e84..000000000
--- a/tests/models/issues/719.err.expected
+++ /dev/null
@@ -1,3 +0,0 @@
-
-unsat
-(error "No model produced.")
diff --git a/tests/models/issues/719.err.smt2 b/tests/models/issues/719.err.smt2
deleted file mode 100644
index 66c07f37c..000000000
--- a/tests/models/issues/719.err.smt2
+++ /dev/null
@@ -1,19 +0,0 @@
-(set-logic ALL)
-(set-option :produce-models true)
-(declare-const a (Array Int Int))
-(declare-const s Int)
-(assert (and (<= 0 s) (<= s 10)))
-(assert (forall ((k Int)) (=> (and (<= 0 k) (< k s)) (<= (select a k) (select a s)))))
-(assert (forall ((k Int)) (=> (and (< s k) (<= k 10)) (<= (select a s) (select a k)))))
-(assert (
-  forall ((p Int) (q Int))
-    (=> (and (<= 0 p) (< p q) (<= q (- s 1))) (<= (select a p) (select a q)))))
-(assert (
-  forall ((p Int) (q Int))
-    (=> (and (<= (+ s 1) p) (< p q) (<= q 10)) (<= (select a p) (select a q)))))
-(assert (not (
-  forall ((p Int) (q Int))
-    (=> (and (<= 0 p) (< p q) (<= q 10)) (<= (select a p) (select a q))))))
-(check-sat)
-(get-model)
-; (get-model) should fail because the problem is UNSAT.
\ No newline at end of file