Merge branch 'smt_experiments' into sail2

1 files changed, 4 insertions, 0 deletions

diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 83d58178..13ed491b 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -193,6 +193,10 @@ let sint = function
 
 let add_int (x, y) = Big_int.add x y
 let sub_int (x, y) = Big_int.sub x y
+let sub_nat (x, y) =
+  let z = Big_int.sub x y in
+  if Big_int.less z Big_int.zero then Big_int.zero else z
+
 let mult (x, y) = Big_int.mul x y
 
 (* This is euclidian division from lem *)