From d2f702da3b5cc9934f8cd3ea457f93c6ce2b6c12 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 12 Jun 2019 17:25:47 +0100
Subject: Add AST for greater-than and less-than constraints Mostly to make
 constraints sent to the SMT solver and Coq nicer, but also makes it easy to
 remove uninformative constraints in the Coq back-end.

---
 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 9dee4761..1bbbca1e 100644
--- a/src/slice.ml
+++ b/src/slice.ml
@@ -104,7 +104,7 @@ let builtins =
 
 let rec constraint_ids' (NC_aux (aux, _)) =
   match aux with
-  | NC_equal (n1, n2) | NC_bounded_le (n1, n2) | NC_bounded_ge (n1, n2) | NC_not_equal (n1, n2) ->
+  | NC_equal (n1, n2) | NC_bounded_le (n1, n2) | NC_bounded_ge (n1, n2) | NC_bounded_lt (n1, n2) | NC_bounded_gt (n1, n2) | NC_not_equal (n1, n2) ->
      IdSet.union (nexp_ids' n1) (nexp_ids' n2)
   | NC_or (nc1, nc2) | NC_and (nc1, nc2) ->
      IdSet.union (constraint_ids' nc1) (constraint_ids' nc2)
-- 
cgit v1.2.3