From 51ac678ccdce4a265991dc5e037dd9c7fc72edd7 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 4 Jul 2021 00:06:42 -0400 Subject: [PATCH] trivial helper --- src/base/Base_types.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/base/Base_types.ml b/src/base/Base_types.ml index 50ed9d7b..9b077a6c 100644 --- a/src/base/Base_types.ml +++ b/src/base/Base_types.ml @@ -839,6 +839,7 @@ module Term : sig val gt : store -> t -> t -> t val eq : store -> t -> t -> t val neq : store -> t -> t -> t + val var : store -> t -> t end (** Obtain unsigned version of [t], + the sign as a boolean *) @@ -971,6 +972,7 @@ end = struct let gt st a b : t = lra st (LRA_pred (Gt, a, b)) let eq st a b : t = lra st (LRA_pred (Eq, a, b)) let neq st a b : t = lra st (LRA_pred (Neq, a, b)) + let var st a : t = lra st (LRA_simplex_var a) end let const_undefined_fun store id ty : t =