From 7cfbabc2bfba4f7d2ba0d3f91c7068ac3b1a84d1 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Sat, 13 Apr 2019 17:47:26 +0100
Subject: SMT: Add count_leading_zeros and more builtins

---
 src/property.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'src/property.ml')

diff --git a/src/property.ml b/src/property.ml
index 37212098..871011e7 100644
--- a/src/property.ml
+++ b/src/property.ml
@@ -78,9 +78,10 @@ let add_property_guards props (Defs defs) =
           | _, constraints ->
              let add_constraints_to_funcl (FCL_aux (FCL_Funcl (id, Pat_aux (pexp, pexp_aux)), fcl_aux)) =
                let add_guard exp =
-                 let exp' = mk_exp (E_if (mk_exp (E_constraint (nc_not (List.fold_left nc_and nc_true constraints))),
-                                          mk_lit_exp L_true,
-                                          strip_exp exp)) in
+                 (* FIXME: Use an assert *)
+                 let exp' = mk_exp (E_if (mk_exp (E_constraint (List.fold_left nc_and nc_true constraints)),
+                                          strip_exp exp,
+                                          mk_lit_exp L_true)) in
                  try Type_check.check_exp (env_of exp) exp' (typ_of exp) with
                  | Type_error (_, l, err) ->
                     let msg =
-- 
cgit v1.2.3