From 9d98228dba7f5b13e3b66d42f8354594651d43c6 Mon Sep 17 00:00:00 2001
From: Shaobo <polarishehn@gmail.com>
Date: Thu, 21 Sep 2017 11:42:02 -0600
Subject: [PATCH] Fixed regression tests bits/interleave_bits_*.c

The old loop unrolling bound (32) in the two files was unnecessarily large.
I reduced it to the proper value (16). Corral flags and time limits are
also adjusted accordingly.
---
 test/bits/config.yml             | 2 +-
 test/bits/interleave_bits_fail.c | 6 +++---
 test/bits/interleave_bits_true.c | 6 +++---
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/test/bits/config.yml b/test/bits/config.yml
index f9e8814e0..c1ce00c1a 100644
--- a/test/bits/config.yml
+++ b/test/bits/config.yml
@@ -1,2 +1,2 @@
 flags: [--bit-precise]
-time-limit: 600
+time-limit: 90
diff --git a/test/bits/interleave_bits_fail.c b/test/bits/interleave_bits_fail.c
index 740ccfaff..f68d840b1 100644
--- a/test/bits/interleave_bits_fail.c
+++ b/test/bits/interleave_bits_fail.c
@@ -1,8 +1,8 @@
 /* https://graphics.stanford.edu/~seander/bithacks.html#InterleaveTableObvious */
 #include "smack.h"
 
-// @flag --loop-limit=33
-// @flag --unroll=33
+// @flag --loop-limit=17
+// @flag --unroll=17
 // @expect error
 
 int main()
@@ -19,7 +19,7 @@ int main()
     unsigned int z = 0; /* z gets the resulting Morton Number. */
     unsigned int i = 0;
 
-    while (i < 32U) {
+    while (i < sizeof(x) * 8) {
         z |= ((x & (1U << i)) << i) | ((y & (1U << i)) << (i + 1));
         i += 1U;
     }
diff --git a/test/bits/interleave_bits_true.c b/test/bits/interleave_bits_true.c
index 8a1c30f08..6067a6850 100644
--- a/test/bits/interleave_bits_true.c
+++ b/test/bits/interleave_bits_true.c
@@ -1,8 +1,8 @@
 /* https://graphics.stanford.edu/~seander/bithacks.html#InterleaveTableObvious */
 #include "smack.h"
 
-// @flag --loop-limit=33
-// @flag --unroll=33
+// @flag --loop-limit=17
+// @flag --unroll=17
 // @expect verified
 
 int main()
@@ -19,7 +19,7 @@ int main()
     unsigned int z = 0; /* z gets the resulting Morton Number. */
     unsigned int i = 0;
 
-    while (i < 32U) {
+    while (i < sizeof(x) * 8) {
         z |= ((x & (1U << i)) << i) | ((y & (1U << i)) << (i + 1));
         i += 1U;
     }