From 41e6fe10e7d28193fa62711fcdad797b1f0103a0 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 13 May 2019 18:03:35 +0100
Subject: Add feature that allows functions to require type variables are
 constant

can now write e.g.

forall (constant 'n : Int) rather than forall ('n: Int)

which requires 'n to be a constant integer value whenever the function
is called. I added this to the 'addrsize variable on memory
reads/writes to absolutely guarantee in the SMT generation that we
don't have to worry about the address being a variable length
bitvector.
---
 src/slice.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/slice.ml')

diff --git a/src/slice.ml b/src/slice.ml
index fa574b7f..78009059 100644
--- a/src/slice.ml
+++ b/src/slice.ml
@@ -217,7 +217,7 @@ let add_def_to_graph graph def =
   let scan_quant_item self (QI_aux (aux, _)) =
     match aux with
     | QI_id _ -> ()
-    | QI_const nc ->
+    | QI_constraint nc ->
        IdSet.iter (fun id -> graph := G.add_edge' self (Type id) !graph) (constraint_ids nc)
   in
 
-- 
cgit v1.2.3