From 26b7dbd222e410a2aa12df3eceb48d438bc0adeb Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 31 Jan 2018 12:35:02 +0000
Subject: Find buried set constraints in asserts

---
 test/mono/assert.sail | 27 ++++++++++++++++++++++-----
 1 file changed, 22 insertions(+), 5 deletions(-)

(limited to 'test')

diff --git a/test/mono/assert.sail b/test/mono/assert.sail
index 4b782398..5b4a013a 100644
--- a/test/mono/assert.sail
+++ b/test/mono/assert.sail
@@ -1,8 +1,25 @@
-val f : forall 'n. atom('n) -> unit effect {escape}
+val f : forall 'n 'm. (atom('n), atom('m)) -> unit effect {escape}
 
-function f(n) = {
-    assert(constraint('n in {8,16}));
-    let 'm = 2 * n in
-    let x : bits('m) = replicate_bits(0b0,'m) in
+function f(n,m) = {
+    assert(constraint('n in {8,16} & 'm < 'n));
+    let 'p = 2 * n in
+    let x : bits('p) = replicate_bits(0b0,'p) in
+    ()
+}
+
+val g : forall 'n 'm. (atom('n), atom('m)) -> unit effect {escape}
+
+function g(n,m) = {
+    assert(constraint('n in {8,16}) & 'm < 'n);
+    let 'p = 2 * n in
+    let x : bits('p) = replicate_bits(0b0,'p) in
+    ()
+}
+val h : forall 'n 'm. (atom('n), atom('m)) -> unit effect {escape}
+
+function h(n,m) = {
+    assert(('n == 8 | 'n == 16) & 'm < 'n);
+    let 'p = 2 * n in
+    let x : bits('p) = replicate_bits(0b0,'p) in
     ()
 }
-- 
cgit v1.2.3