From 5efc7e055c1cc6d8452e6de862398aebb035eb23 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 4 Jun 2018 15:07:17 +0100
Subject: Re-generate aarch64 spec, fixing an issue with Replicate

---
 aarch64/full/spec.sail      | 2 ++
 aarch64/no_vector/spec.sail | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/aarch64/full/spec.sail b/aarch64/full/spec.sail
index f468302b..6920db48 100644
--- a/aarch64/full/spec.sail
+++ b/aarch64/full/spec.sail
@@ -2130,6 +2130,8 @@ val Replicate : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0.
 
 function Replicate x = {
   assert('N % 'M == 0, "((N MOD M) == 0)");
+  let 'O = 'N / 'M;
+  assert(constraint('O * 'M = 'N));
   return(replicate_bits(x, 'N / 'M))
 }
 
diff --git a/aarch64/no_vector/spec.sail b/aarch64/no_vector/spec.sail
index 775800f3..23a41355 100644
--- a/aarch64/no_vector/spec.sail
+++ b/aarch64/no_vector/spec.sail
@@ -2064,6 +2064,8 @@ val Replicate : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0.
 
 function Replicate x = {
   assert('N % 'M == 0, "((N MOD M) == 0)");
+  let 'O = 'N / 'M;
+  assert(constraint('O * 'M = 'N));
   return(replicate_bits(x, 'N / 'M))
 }
 
-- 
cgit v1.2.3