Skip to content

Commit

Permalink
Removing problematic test
Browse files Browse the repository at this point in the history
This test fails when wrapped in a push/pop instruction. Issue #1008 discusses
this as an independent issue.
  • Loading branch information
Stevendeo committed Dec 12, 2023
1 parent 0b65739 commit cf22aef
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion tests/adts/simple_1.ae
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down

0 comments on commit cf22aef

Please sign in to comment.