From cf22aefdd82d7ffd5fad1da2cc0124a94ed5328f Mon Sep 17 00:00:00 2001
From: Steven de Oliveira <de.oliveira.steven@gmail.com>
Date: Tue, 12 Dec 2023 10:42:30 +0100
Subject: [PATCH] Removing problematic test

This test fails when wrapped in a push/pop instruction. Issue #1008 discusses
this as an independent issue.
---
 tests/adts/simple_1.ae | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/tests/adts/simple_1.ae b/tests/adts/simple_1.ae
index cc82d2f240..fa271f926b 100644
--- a/tests/adts/simple_1.ae
+++ b/tests/adts/simple_1.ae
@@ -49,13 +49,15 @@ goal g_valid_4_2:
   e ? B ->
   false
 
-(**)
+(* Isse 1008: this goal fail when encapsulated by a push/pop. *)
+(*
 goal g_valid_5_1:
   forall n : int.
   n >= 0 -> (* just here for E-matching *)
   not (e ? A) ->
   not (e ? B) ->
   exists x : int[x]. e = C(x)
+*)
 
 goal g_valid_5_2:
   forall n : int.