From 51811443eeb7c594b8db9bbffd387dc0fbfeffd3 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 7 Nov 2019 16:16:14 +0000
Subject: Backport fixes to SMT generation from poly_mapping branch

---
 test/smt/revrev_endianness.sail        | 25 -------------------------
 test/smt/revrev_endianness.unsat.sail  | 25 +++++++++++++++++++++++++
 test/smt/revrev_endianness2.sail       | 20 --------------------
 test/smt/revrev_endianness2.unsat.sail | 20 ++++++++++++++++++++
 4 files changed, 45 insertions(+), 45 deletions(-)
 delete mode 100644 test/smt/revrev_endianness.sail
 create mode 100644 test/smt/revrev_endianness.unsat.sail
 delete mode 100644 test/smt/revrev_endianness2.sail
 create mode 100644 test/smt/revrev_endianness2.unsat.sail

(limited to 'test')

diff --git a/test/smt/revrev_endianness.sail b/test/smt/revrev_endianness.sail
deleted file mode 100644
index f792871f..00000000
--- a/test/smt/revrev_endianness.sail
+++ /dev/null
@@ -1,25 +0,0 @@
-default Order dec
-
-$include <reverse_endianness.sail>
-
-$property
-function prop forall 'n, 'n in {8, 16, 32, 64, 128}. (n: int('n), xs: bits('n)) -> bool = {
-  if length(xs) == 8 then {
-    let ys: bits(8) = xs;
-    reverse_endianness(reverse_endianness(ys)) == ys
-  } else if length(xs) == 16 then {
-    let ys: bits(16) = xs;
-    reverse_endianness(reverse_endianness(ys)) == ys
-  } else if length(xs) == 32 then {
-    let ys: bits(32) = xs;
-    reverse_endianness(reverse_endianness(ys)) == ys
-  } else if length(xs) == 64 then {
-    let ys: bits(64) = xs;
-    reverse_endianness(reverse_endianness(ys)) == ys
-  } else if length(xs) == 128 then {
-    let ys: bits(128) = xs;
-    reverse_endianness(reverse_endianness(ys)) == ys
-  } else {
-    true
-  }
-}
diff --git a/test/smt/revrev_endianness.unsat.sail b/test/smt/revrev_endianness.unsat.sail
new file mode 100644
index 00000000..f792871f
--- /dev/null
+++ b/test/smt/revrev_endianness.unsat.sail
@@ -0,0 +1,25 @@
+default Order dec
+
+$include <reverse_endianness.sail>
+
+$property
+function prop forall 'n, 'n in {8, 16, 32, 64, 128}. (n: int('n), xs: bits('n)) -> bool = {
+  if length(xs) == 8 then {
+    let ys: bits(8) = xs;
+    reverse_endianness(reverse_endianness(ys)) == ys
+  } else if length(xs) == 16 then {
+    let ys: bits(16) = xs;
+    reverse_endianness(reverse_endianness(ys)) == ys
+  } else if length(xs) == 32 then {
+    let ys: bits(32) = xs;
+    reverse_endianness(reverse_endianness(ys)) == ys
+  } else if length(xs) == 64 then {
+    let ys: bits(64) = xs;
+    reverse_endianness(reverse_endianness(ys)) == ys
+  } else if length(xs) == 128 then {
+    let ys: bits(128) = xs;
+    reverse_endianness(reverse_endianness(ys)) == ys
+  } else {
+    true
+  }
+}
diff --git a/test/smt/revrev_endianness2.sail b/test/smt/revrev_endianness2.sail
deleted file mode 100644
index 33ba93a2..00000000
--- a/test/smt/revrev_endianness2.sail
+++ /dev/null
@@ -1,20 +0,0 @@
-default Order dec
-
-$include <reverse_endianness.sail>
-
-$property
-function prop forall 'n, 'n in {8, 16, 32, 64, 128}. (n: int('n), xs: bits('n)) -> bool = {
-  if length(xs) == 8 then {
-    reverse_endianness(reverse_endianness(xs)) == xs
-  } else if length(xs) == 16 then {
-    reverse_endianness(reverse_endianness(xs)) == xs
-  } else if length(xs) == 32 then {
-    reverse_endianness(reverse_endianness(xs)) == xs
-  } else if length(xs) == 64 then {
-    reverse_endianness(reverse_endianness(xs)) == xs
-  } else if length(xs) == 128 then {
-    reverse_endianness(reverse_endianness(xs)) == xs
-  } else {
-    true
-  }
-}
diff --git a/test/smt/revrev_endianness2.unsat.sail b/test/smt/revrev_endianness2.unsat.sail
new file mode 100644
index 00000000..33ba93a2
--- /dev/null
+++ b/test/smt/revrev_endianness2.unsat.sail
@@ -0,0 +1,20 @@
+default Order dec
+
+$include <reverse_endianness.sail>
+
+$property
+function prop forall 'n, 'n in {8, 16, 32, 64, 128}. (n: int('n), xs: bits('n)) -> bool = {
+  if length(xs) == 8 then {
+    reverse_endianness(reverse_endianness(xs)) == xs
+  } else if length(xs) == 16 then {
+    reverse_endianness(reverse_endianness(xs)) == xs
+  } else if length(xs) == 32 then {
+    reverse_endianness(reverse_endianness(xs)) == xs
+  } else if length(xs) == 64 then {
+    reverse_endianness(reverse_endianness(xs)) == xs
+  } else if length(xs) == 128 then {
+    reverse_endianness(reverse_endianness(xs)) == xs
+  } else {
+    true
+  }
+}
-- 
cgit v1.2.3