testcase for #33

share/pulse/examples/bug-reports/Bug33.fst

@@ -0,0 +1,29 @@
+(*
+   Copyright 2023 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+
+module Bug33
+
+open Pulse.Lib.Pervasives
+
+```pulse
+fn test (z:int)
+  requires emp
+  returns _:unit
+  ensures (exists* (x:int). emp)
+{
+  admit();
+}
+```