From 7b4bf2bd14cae99a4d8086a0b66d9875be1acbab Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 21 May 2019 17:31:13 +0100
Subject: SMT: Use a separate constructor for memory read variables

We want to ensure simplication can treat these separately so we
don't accidentally simplify away dependencies between reads and write
addresses.
---
 test/smt/load_store_dep.sat.sail | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 test/smt/load_store_dep.sat.sail

(limited to 'test')

diff --git a/test/smt/load_store_dep.sat.sail b/test/smt/load_store_dep.sat.sail
new file mode 100644
index 00000000..bb35c6f7
--- /dev/null
+++ b/test/smt/load_store_dep.sat.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+$include <prelude.sail>
+$include "test/arch.sail"
+
+/* Default memory model is as weak as possible, so this is not true */
+$counterexample
+function prop() -> bool = {
+  let _ = arch_load(0b00, 0b01);
+  let _ = arch_store(0b10, 0b00);
+  X(0b01) == X(0b10)
+}
-- 
cgit v1.2.3