From da118da3e590fbea4e880121837da2ee938837f6 Mon Sep 17 00:00:00 2001
From: Sidney Congard
Date: Thu, 23 Jun 2022 15:43:49 +0200
Subject: adapt to new LLBC (without OperandConstantValue)

---
 tests/misc/Constants.fst | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

(limited to 'tests/misc')

diff --git a/tests/misc/Constants.fst b/tests/misc/Constants.fst
index 9611c778..28a9ace7 100644
--- a/tests/misc/Constants.fst
+++ b/tests/misc/Constants.fst
@@ -117,3 +117,22 @@ let get_z2_fwd : result i32 =
     end
   end
 
+(** [constants::S1] *)
+let s1_fwd : result u32 = Return 6
+
+(** [constants::S2] *)
+let s2_fwd : result u32 =
+  begin match s1_fwd with
+  | Fail -> Fail
+  | Return i ->
+    begin match incr_fwd i with | Fail -> Fail | Return i0 -> Return i0 end
+  end
+
+(** [constants::S3] *)
+let s3_fwd : result (pair_t u32 u32) =
+  begin match p3_fwd with | Fail -> Fail | Return p -> Return p end
+
+(** [constants::S4] *)
+let s4_fwd : result (pair_t u32 u32) =
+  begin match mk_pair1_fwd 7 8 with | Fail -> Fail | Return p -> Return p end
+
-- 
cgit v1.2.3