Merge branch 'smt_experiments' into sail2

25 files changed, 585 insertions, 102 deletions

diff --git a/language/jib.ott b/language/jib.ott
index 447b25e3..dfda3bbc 100644
--- a/language/jib.ott
+++ b/language/jib.ott
@@ -58,6 +58,8 @@ name :: '' ::=
 
 op :: '' ::=
   | not               :: :: bnot
+  | or                :: :: bor
+  | and               :: :: band
   | hd                :: :: list_hd
   | tl                :: :: list_tl
   | bit_to_bool       :: :: bit_to_bool
diff --git a/lib/flow.sail b/lib/flow.sail
index 5c69a128..dd917b55 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -61,4 +61,6 @@ function __id forall 'n. (x: int('n)) -> int('n) = x
 
 overload __size = {__id}
 
+val __deref = "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+
 $endif
diff --git a/lib/mapping.sail b/lib/mapping.sail
new file mode 100644
index 00000000..6cbb7585
--- /dev/null
+++ b/lib/mapping.sail
@@ -0,0 +1,84 @@
+$ifndef _MAPPING
+$define _MAPPING
+
+$include <arith.sail>
+$include <option.sail>
+
+val string_take = "string_take" : (string, nat) -> string
+val string_drop = "string_drop" : (string, nat) -> string
+val string_length = "string_length" : string -> nat
+val string_append = {c: "concat_str", _: "string_append"} : (string, string) -> string
+val string_startswith = "string_startswith" : (string, string) -> bool
+
+val n_leading_spaces : string -> nat
+function n_leading_spaces s =
+  match s {
+    "" => 0,
+    _ => match string_take(s, 1) {
+      " " => 1 + n_leading_spaces(string_drop(s, 1)),
+      _ => 0
+    }
+  }
+
+val spc     : unit <-> string
+val opt_spc : unit <-> string
+val def_spc : unit <-> string
+
+val spc_forwards : unit -> string
+function spc_forwards () = " "
+val spc_backwards : string -> unit
+function spc_backwards s = ()
+val spc_matches_prefix : string -> option((unit, nat))
+function spc_matches_prefix s = {
+  let n = n_leading_spaces(s);
+  match n {
+    0 => None(),
+    _ => Some((), n)
+  }
+}
+
+val opt_spc_forwards : unit -> string
+function opt_spc_forwards () = ""
+val opt_spc_backwards : string -> unit
+function opt_spc_backwards s = ()
+val opt_spc_matches_prefix : string -> option((unit, nat))
+function opt_spc_matches_prefix s =
+  Some((), n_leading_spaces(s))
+
+val def_spc_forwards : unit -> string
+function def_spc_forwards () = " "
+val def_spc_backwards : string -> unit
+function def_spc_backwards s = ()
+val def_spc_matches_prefix : string -> option((unit, nat))
+function def_spc_matches_prefix s = opt_spc_matches_prefix(s)
+
+val sep : unit <-> string
+mapping sep : unit <-> string = {
+  ()     <-> opt_spc() ^ "," ^ def_spc()
+}
+
+$ifdef _DEFAULT_DEC
+$include <vector_dec.sail>
+
+val hex_bits_20 : bits(20) <-> string
+val hex_bits_20_forwards = "decimal_string_of_bits" : bits(20) -> string
+val hex_bits_20_forwards_matches : bits(20) -> bool
+function hex_bits_20_forwards_matches bv = true
+val "hex_bits_20_matches_prefix" : string -> option((bits(20), nat))
+val hex_bits_20_backwards_matches : string -> bool
+function hex_bits_20_backwards_matches s = match s {
+  s if match hex_bits_20_matches_prefix(s) {
+    Some (_, n) if n == string_length(s) => true,
+    _ => false
+  } => true,
+  _ => false
+}
+val hex_bits_20_backwards : string -> bits(20)
+function hex_bits_20_backwards s =
+  match hex_bits_20_matches_prefix(s) {
+      Some (bv, n) if n == string_length(s) => bv
+  }
+
+$endif
+
+$endif
diff --git a/lib/real.sail b/lib/real.sail
index 47d3f9bd..cd63a622 100644
--- a/lib/real.sail
+++ b/lib/real.sail
@@ -1,5 +1,5 @@
-$ifndef __REAL
-$define __REAL
+$ifndef _REAL
+$define _REAL
 
 val "neg_real" : real -> real
 
diff --git a/lib/string.sail b/lib/string.sail
index 3fe74eb5..87e4da57 100644
--- a/lib/string.sail
+++ b/lib/string.sail
@@ -5,6 +5,8 @@ $include <arith.sail>
 
 val eq_string = {lem: "eq", coq: "generic_eq", _: "eq_string"} : (string, string) -> bool
 
+overload operator == = {eq_string}
+
 infixl 9 ^-^
 
 val concat_str = {lem: "stringAppend", _: "concat_str"} : (string, string) -> string
diff --git a/src/initial_check.ml b/src/initial_check.ml
index ad52751b..522faab7 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -425,7 +425,8 @@ and to_ast_exp ctx (P.E_aux(exp,l) : P.exp) =
          E_internal_return(to_ast_exp ctx exp)
        else
          raise (Reporting.err_general l "Internal return construct found without -dmagic_hash")
-    | _ -> raise (Reporting.err_unreachable l __POS__ "Unparsable construct in to_ast_exp")
+    | P.E_deref exp ->
+       E_app (Id_aux (Id "__deref", l), [to_ast_exp ctx exp])
     ), (l,()))
 
 and to_ast_measure ctx (P.Measure_aux(m,l)) : unit internal_loop_measure =
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 086d4d11..7f622f85 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -67,6 +67,8 @@ let opt_ignore_overflow = ref false
 
 let opt_auto = ref false
 
+let opt_debug_graphs = ref false
+
 module EventMap = Map.Make(Event)
 
 (* Note that we have to use x : ty ref rather than mutable x : ty, to
@@ -91,7 +93,7 @@ type ctx = {
     (* When generating SMT for an instruction pathcond will contain
        the global path conditional of the containing block in the
        control flow graph *)
-    pathcond : smt_exp;
+    pathcond : smt_exp Lazy.t;
     (* Set if we need to use strings *)
     use_string : bool ref;
     use_real : bool ref
@@ -116,7 +118,7 @@ let initial_ctx () = {
     arg_stack = Stack.create ();
     ast = Defs [];
     events = ref EventMap.empty;
-    pathcond = Bool_lit true;
+    pathcond = lazy (Bool_lit true);
     use_string = ref false;
     use_real = ref false;
   }
@@ -278,6 +280,10 @@ let rec smt_cval ctx cval =
      Fn ("=", [smt_cval ctx cval; Bin "1"])
   | V_call (Bnot, [cval]) ->
      Fn ("not", [smt_cval ctx cval])
+  | V_call (Band, cvals) ->
+     smt_conj (List.map (smt_cval ctx) cvals)
+  | V_call (Bor, cvals) ->
+     smt_disj (List.map (smt_cval ctx) cvals)
   | V_ctor_kind (union, ctor_id, unifiers, _) ->
      Fn ("not", [Tester (zencode_ctor ctor_id unifiers, smt_cval ctx union)])
   | V_ctor_unwrap (ctor_id, union, unifiers, _) ->
@@ -320,7 +326,10 @@ let rec smt_cval ctx cval =
 
 let add_event ctx ev smt =
   let stack = event_stack ctx ev in
-  Stack.push (Fn ("=>", [ctx.pathcond; smt])) stack
+  Stack.push (Fn ("=>", [Lazy.force ctx.pathcond; smt])) stack
+
+let add_pathcond_event ctx ev =
+  Stack.push (Lazy.force ctx.pathcond) (event_stack ctx ev)
 
 let overflow_check ctx smt =
   if not !opt_ignore_overflow then (
@@ -903,6 +912,16 @@ let builtin_compare_bits fn ctx v1 v2 ret_ctyp =
 
   | _ -> builtin_type_error ctx fn [v1; v2] (Some ret_ctyp)
 
+(* ***** String operations: lib/real.sail ***** *)
+
+let builtin_decimal_string_of_bits ctx v =
+  begin match cval_ctyp v with
+  | CT_fbits (n, _) ->
+     Fn ("int.to.str", [Fn ("bv2nat", [smt_cval ctx v])])
+
+  | _ -> builtin_type_error ctx "decimal_string_of_bits" [v] None
+  end
+
 (* ***** Real number operations: lib/real.sail ***** *)
 
 let builtin_sqrt_real ctx root v =
@@ -986,6 +1005,7 @@ let smt_builtin ctx name args ret_ctyp =
   (* string builtins *)
   | "concat_str", [v1; v2], CT_string -> ctx.use_string := true; Fn ("str.++", [smt_cval ctx v1; smt_cval ctx v2])
   | "eq_string", [v1; v2], CT_bool -> ctx.use_string := true; Fn ("=", [smt_cval ctx v1; smt_cval ctx v2])
+  | "decimal_string_of_bits", [v], CT_string -> ctx.use_string := true; builtin_decimal_string_of_bits ctx v
 
   (* lib/real.sail *)
   (* Note that sqrt_real is special and is handled by smt_instr. *)
@@ -1002,6 +1022,23 @@ let smt_builtin ctx name args ret_ctyp =
 
   | _ -> failwith ("Unknown builtin " ^ name ^ " " ^ Util.string_of_list ", " string_of_ctyp (List.map cval_ctyp args) ^ " -> " ^ string_of_ctyp ret_ctyp)
 
+(* Memory reads and writes as defined in lib/regfp.sail *)
+let writes = ref (-1)
+
+let builtin_write_mem ctx wk addr_size addr data_size data =
+  incr writes;
+  let name = "W" ^ string_of_int !writes in
+  [Write_mem (name, smt_cval ctx wk, smt_cval ctx addr, smt_cval ctx data)],
+  Var name
+
+let reads = ref (-1)
+
+let builtin_read_mem ctx rk addr_size addr data_size ret_ctyp =
+  incr reads;
+  let name = "R" ^ string_of_int !reads in
+  [Read_mem (name, smt_ctyp ctx ret_ctyp, smt_cval ctx rk, smt_cval ctx addr)],
+  Var name
+
 let rec smt_conversion ctx from_ctyp to_ctyp x =
   match from_ctyp, to_ctyp with
   | _, _ when ctyp_equal from_ctyp to_ctyp -> x
@@ -1214,7 +1251,7 @@ let push_smt_defs stack smt_defs =
 (* When generating SMT when we encounter joins between two or more
    blocks such as in the example below, we have to generate a muxer
    that chooses the correct value of v_n or v_m to assign to v_o. We
-   use the pi nodes that contain the global path condition for each
+   use the pi nodes that contain the path condition for each
    block to generate an if-then-else for each phi function. The order
    of the arguments to each phi function is based on the graph node
    index for the predecessor nodes.
@@ -1249,11 +1286,7 @@ let smt_ssanode ctx cfg preds =
      let pis = List.map get_pi (IntSet.elements preds) in
      let mux =
        List.fold_right2 (fun pi id chain ->
-           let pathcond =
-             match pi with
-             | [cval] -> smt_cval ctx cval
-             | _ -> Fn ("and", List.map (smt_cval ctx) pi)
-           in
+           let pathcond = smt_conj (List.map (smt_cval ctx) pi) in
            match chain with
            | Some smt ->
               Some (Ite (pathcond, Var (zencode_name id), smt))
@@ -1266,12 +1299,68 @@ let smt_ssanode ctx cfg preds =
      | Some mux ->
         [Define_const (zencode_name id, smt_ctyp ctx ctyp, mux)]
 
-let rec get_pathcond ctx fns =
+(* The pi condition are computed by traversing the dominator tree,
+   with each node having a pi condition defined as the conjunction of
+   all guards between it and the start node in the dominator
+   tree. This is imprecise because we have situations like:
+
+      1
+     / \
+    2   3
+    |   |
+    |   4
+    |   |\
+    5   6 9
+     \ /  |
+      7   10
+      |
+      8
+
+   where 8 = match_failure, 1 = start and 10 = return.
+   2, 3, 6 and 9 are guards as they come directly after a control flow
+   split, which always follows a conditional jump.
+
+   Here the path through the dominator tree for the match_failure is
+   1->7->8 which contains no guards so the pi condition would be empty.
+   What we do now is walk backwards (CFG must be acyclic at this point)
+   until we hit the join point prior to where we require a path
+   condition. We then take the disjunction of the pi conditions for the
+   join point's predecessors, so 5 and 6 in this case. Which gives us a
+   path condition of 2 | (3 & 6) as the dominator chains are 1->2->5 and
+   1->3->4->6.
+
+   This should work as any split in the control flow must have been
+   caused by a conditional jump followed by distinct guards, so each of
+   the nodes immediately prior to a join point must be dominated by at
+   least one unique guard. It also explains why the pi conditions are
+   sufficient to choose outcomes of phi functions above.
+
+   If we hit a guard before a join (such as 9 for return's path
+   conditional) we just return the pi condition for that guard, i.e.
+   (3 & 9) for 10. If we reach start then the path condition is simply
+   true.
+*)
+let rec get_pathcond n cfg ctx =
   let open Jib_ssa in
-  match fns with
-  | [] | Pi [] :: _ -> Bool_lit true
-  | Pi cvals :: _ -> Fn ("and", List.map (smt_cval ctx) cvals)
-  | Phi _ :: fns -> get_pathcond ctx fns
+  let get_pi m =
+    match get_vertex cfg m with
+    | Some ((ssanodes, _), _, _) ->
+       V_call (Band, List.concat (List.map (function Pi guards -> guards | _ -> []) ssanodes))
+    | None -> failwith "Node does not exist"
+  in
+  match get_vertex cfg n with
+  | Some ((_, CF_guard cond), _, _) ->
+     smt_cval ctx (get_pi n)
+  | Some (_, preds, succs) ->
+     if IntSet.cardinal preds = 0 then
+       Bool_lit true
+     else if IntSet.cardinal preds = 1 then
+       get_pathcond (IntSet.min_elt preds) cfg ctx
+     else
+       let pis = List.map get_pi (IntSet.elements preds) in
+       smt_cval ctx (V_call (Bor, pis))
+
+  | None -> assert false (* Should never be called for a non-existent node *)
 
 (* For any complex l-expression we need to turn it into a
    read-modify-write in the SMT solver. The SSA transform turns CL_id
@@ -1323,6 +1412,19 @@ let rmw_modify smt = function
      end
   | _ -> assert false
 
+let smt_terminator ctx =
+  let open Jib_ssa in
+  function
+  | T_end id ->
+     add_event ctx Return (Var (zencode_name id));
+     []
+
+  | T_match_failure ->
+     add_pathcond_event ctx Match;
+     []
+
+  | T_undefined _ | T_goto _ | T_jump _ | T_label _ | T_none -> []
+
 (* For a basic block (contained in a control-flow node / cfnode), we
    turn the instructions into a sequence of define-const and
    declare-const expressions. Because we are working with a SSA graph,
@@ -1340,6 +1442,24 @@ let smt_instr ctx =
          | _ ->
             Reporting.unreachable l __POS__ "Bad arguments for sqrt_real"
          end
+       (* See lib/regfp.sail *)
+       else if name = "platform_write_mem" then
+         begin match args with
+         | [wk; addr_size; addr; data_size; data] ->
+            let mem_event, var = builtin_write_mem ctx wk addr_size addr data_size data in
+            mem_event @ [define_const ctx id ret_ctyp var]
+         | _ ->
+            Reporting.unreachable l __POS__ "Bad arguments for __write_mem"
+         end
+       else if name = "platform_read_mem" then
+         begin match args with
+         | [rk; addr_size; addr; data_size] ->
+            let mem_event, var = builtin_read_mem ctx rk addr_size addr data_size ret_ctyp in
+            mem_event @ [define_const ctx id ret_ctyp var]
+                                                   
+         | _ ->
+            Reporting.unreachable l __POS__ "Bad arguments for __read_mem"
+         end
        else
          let value = smt_builtin ctx name args ret_ctyp in
          [define_const ctx id ret_ctyp value]
@@ -1401,21 +1521,11 @@ let smt_instr ctx =
      end;
      [declare_const ctx id ctyp]
 
-  | I_aux (I_end id, _) ->
-     add_event ctx Return (Var (zencode_name id));
-     []
-
   | I_aux (I_clear _, _) -> []
 
-  | I_aux (I_match_failure, _) ->
-     add_event ctx Match (Bool_lit false);
-     []
-
-  | I_aux (I_undefined ctyp, _) -> []
-
-  (* I_jump and I_goto will only appear as terminators for basic blocks. *)
-  | I_aux ((I_jump _ | I_goto _), _) -> []
-
+  (* Should only appear as terminators for basic blocks. *)
+  | I_aux ((I_jump _ | I_goto _ | I_end _ | I_match_failure | I_undefined _), (_, l)) ->
+     Reporting.unreachable l __POS__ "SMT: Instruction should only appear as block terminator"
 
   | instr ->
      failwith ("Cannot translate: " ^ Pretty_print_sail.to_string (pp_instr instr))
@@ -1431,9 +1541,10 @@ let smt_cfnode all_cdefs ctx ssanodes =
        | _ -> declare_const ctx id ctyp
      in
      smt_reg_decs @ List.map smt_start (NameMap.bindings inits)
-  | CF_block instrs ->
-     let ctx = { ctx with pathcond = get_pathcond ctx ssanodes } in
-     List.concat (List.map (smt_instr ctx) instrs)
+  | CF_block (instrs, terminator) ->
+     let smt_instrs = List.map (smt_instr ctx) instrs in
+     let smt_term = smt_terminator ctx terminator in
+     List.concat (smt_instrs @ [smt_term])
   (* We can ignore any non basic-block/start control-flow nodes *)
   | _ -> []
 
@@ -1486,6 +1597,12 @@ let optimize_smt stack =
        end
     | (Declare_datatypes _ | Declare_tuple _) as def ->
        Stack.push def stack'
+    | Write_mem (_, wk, addr, data) as def ->
+       uses_in_exp wk; uses_in_exp addr; uses_in_exp data;
+       Stack.push def stack'
+    | Read_mem (_, _, rk, addr) as def ->
+       uses_in_exp rk; uses_in_exp addr;
+       Stack.push def stack'
     | Assert exp as def ->
        uses_in_exp exp;
        Stack.push def stack'
@@ -1507,6 +1624,10 @@ let optimize_smt stack =
           Queue.add (Define_const (var, typ, simp_smt_exp vars exp)) queue
        | None -> assert false
        end
+    | Write_mem (name, wk, addr, data) ->
+       Queue.add (Write_mem (name, simp_smt_exp vars wk, simp_smt_exp vars addr, simp_smt_exp vars data)) queue
+    | Read_mem (name, typ, rk, addr) ->
+       Queue.add (Read_mem (name, typ, simp_smt_exp vars rk, simp_smt_exp vars addr)) queue
     | Assert exp ->
        Queue.add (Assert (simp_smt_exp vars exp)) queue
     | (Declare_datatypes _ | Declare_tuple _) as def ->
@@ -1582,16 +1703,6 @@ let expand_reg_deref ctx = function
      end
   | instr -> instr
 
-let smt_conj = function
-  | [] -> Bool_lit true
-  | [x] -> x
-  | xs -> Fn ("and", xs)
-
-let smt_disj = function
-  | [] -> Bool_lit false
-  | [x] -> x
-  | xs -> Fn ("or", xs)
-
 let rec smt_query ctx = function
   | Q_all ev ->
      let stack = event_stack ctx ev in
@@ -1606,6 +1717,12 @@ let rec smt_query ctx = function
   | Q_or qs ->
      Fn ("or", List.map (smt_query ctx) qs)
 
+let dump_graph function_id cfg =
+  let gv_file = string_of_id function_id ^ ".gv" in
+  let out_chan = open_out gv_file in
+  Jib_ssa.make_dot out_chan cfg;
+  close_out out_chan
+
 let smt_cdef props lets name_file ctx all_cdefs = function
   | CDEF_spec (function_id, arg_ctyps, ret_ctyp) when Bindings.mem function_id props ->
      begin match find_function [] function_id all_cdefs with
@@ -1641,14 +1758,13 @@ let smt_cdef props lets name_file ctx all_cdefs = function
         let visit_order =
           try topsort cfg with
           | Not_a_DAG n ->
-             let gv_file = string_of_id function_id ^ ".gv" in
-             let out_chan = open_out gv_file in
-             make_dot out_chan cfg;
-             close_out out_chan;
+             dump_graph function_id cfg;
              raise (Reporting.err_general pragma_l
-                      (Printf.sprintf "$%s %s: control flow graph is not acyclic (node %d is in cycle)\nWrote graph to %s"
-                         prop_type (string_of_id function_id) n gv_file))
+                      (Printf.sprintf "$%s %s: control flow graph is not acyclic (node %d is in cycle)\nWrote graph to %s.gv"
+                         prop_type (string_of_id function_id) n (string_of_id function_id)))
         in
+        if !opt_debug_graphs then
+          dump_graph function_id cfg;
 
         List.iter (fun n ->
             begin match get_vertex cfg n with
@@ -1657,6 +1773,7 @@ let smt_cdef props lets name_file ctx all_cdefs = function
                let muxers =
                  ssanodes |> List.map (smt_ssanode ctx cfg preds) |> List.concat
                in
+               let ctx = { ctx with pathcond = lazy (get_pathcond n cfg ctx) } in
                let basic_block = smt_cfnode all_cdefs ctx ssanodes cfnode in
                push_smt_defs stack muxers;
                push_smt_defs stack basic_block;
@@ -1671,12 +1788,14 @@ let smt_cdef props lets name_file ctx all_cdefs = function
         if prop_type = "counterexample" then
           output_string out_chan "(set-option :produce-models true)\n";
 
+        let header = smt_header ctx all_cdefs in
+        
         if !(ctx.use_string) || !(ctx.use_real) then
           output_string out_chan "(set-logic ALL)\n"
         else
           output_string out_chan "(set-logic QF_AUFBVDT)\n";
 
-        List.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") (smt_header ctx all_cdefs);
+        List.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") header;
 
         let queue = optimize_smt stack in
         Queue.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") queue;
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index 9a9a3361..0f0f582e 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -53,6 +53,7 @@ open Jib
 open Jib_util
 
 module IntSet = Set.Make(struct type t = int let compare = compare end)
+module IntMap = Map.Make(struct type t = int let compare = compare end)
 
 (**************************************************************************)
 (* 1. Mutable graph type                                                  *)
@@ -60,14 +61,24 @@ module IntSet = Set.Make(struct type t = int let compare = compare end)
 
 type 'a array_graph = {
     mutable next : int;
-    mutable nodes : ('a * IntSet.t * IntSet.t) option array
+    mutable nodes : ('a * IntSet.t * IntSet.t) option array;
+    mutable next_cond : int;
+    mutable conds : cval IntMap.t
   }
 
 let make ~initial_size () = {
     next = 0;
-    nodes = Array.make initial_size None
+    nodes = Array.make initial_size None;
+    next_cond = 1;
+    conds = IntMap.empty
   }
 
+let get_cond graph n =
+  if n >= 0 then
+    IntMap.find n graph.conds
+  else
+    V_call (Bnot, [IntMap.find (abs n) graph.conds])
+     
 let get_vertex graph n = graph.nodes.(n)
 
 let iter_graph f graph =
@@ -77,6 +88,12 @@ let iter_graph f graph =
     | None -> ()
   done
 
+let add_cond cval graph =
+  let n = graph.next_cond in
+  graph.conds <- IntMap.add n cval graph.conds;
+  graph.next_cond <- n + 1;
+  n
+
 (** Add a vertex to a graph, returning the node index *)
 let add_vertex data graph =
   let n = graph.next in
@@ -187,12 +204,32 @@ let prune visited graph =
 (* 2. Mutable control flow graph                                          *)
 (**************************************************************************)
 
+type terminator =
+  | T_undefined of ctyp
+  | T_match_failure
+  | T_end of name
+  | T_goto of string
+  | T_jump of int * string
+  | T_label of string
+  | T_none
+
 type cf_node =
   | CF_label of string
-  | CF_block of instr list
-  | CF_guard of cval
+  | CF_block of instr list * terminator
+  | CF_guard of int
   | CF_start of ctyp NameMap.t
 
+let to_terminator graph = function
+  | I_label label -> T_label label
+  | I_goto label -> T_goto label
+  | I_jump (cval, label) ->
+     let n = add_cond cval graph in
+     T_jump (n, label)
+  | I_end name -> T_end name
+  | I_match_failure -> T_match_failure
+  | I_undefined ctyp -> T_undefined ctyp
+  | _ -> assert false
+
 (* For now we only generate CFGs for flat lists of instructions *)
 let control_flow_graph instrs =
   let module StringMap = Map.Make(String) in
@@ -209,46 +246,42 @@ let control_flow_graph instrs =
 
   let cf_split (I_aux (aux, _)) =
     match aux with
-    | I_block _ | I_label _ | I_goto _ | I_jump _ | I_if _ | I_end _ | I_match_failure | I_undefined _ -> true
+    | I_label _ | I_goto _ | I_jump _ | I_end _ | I_match_failure | I_undefined _ -> true
     | _ -> false
   in
 
   let rec cfg preds instrs =
     let before, after = instr_split_at cf_split instrs in
-    let last = match after with
-      | I_aux (I_label _, _) :: _ -> []
-      | instr :: _ -> [instr]
-      | _ -> []
+    let terminator, after = match after with
+      | I_aux (instr, _) :: after -> to_terminator graph instr, after
+      | [] -> T_none, []
     in
-    let preds = match before @ last with
-      | [] -> preds
-      | instrs ->
-         let n = add_vertex ([], CF_block instrs) graph in
+    let preds = match before, terminator with
+      | [], (T_none | T_label _) -> preds
+      | instrs, _ ->
+         let n = add_vertex ([], CF_block (instrs, terminator)) graph in
          List.iter (fun p -> add_edge p n graph) preds;
          [n]
     in
-    match after with
-    | I_aux ((I_end _ | I_match_failure | I_undefined _), _) :: after ->
+    match terminator with
+    | T_end _ | T_match_failure | T_undefined _ ->
        cfg [] after
 
-    | I_aux (I_goto label, _) :: after ->
+    | T_goto label ->
        List.iter (fun p -> add_edge p (StringMap.find label !labels) graph) preds;
        cfg [] after
 
-    | I_aux (I_jump (cval, label), _) :: after ->
-       let t = add_vertex ([], CF_guard cval) graph in
-       let f = add_vertex ([], CF_guard (V_call (Bnot, [cval]))) graph in
+    | T_jump (cond, label) ->
+       let t = add_vertex ([], CF_guard cond) graph in
+       let f = add_vertex ([], CF_guard (- cond)) graph in
        List.iter (fun p -> add_edge p t graph; add_edge p f graph) preds;
        add_edge t (StringMap.find label !labels) graph;
        cfg [f] after
 
-    | I_aux (I_label label, _) :: after ->
+    | T_label label ->
        cfg (StringMap.find label !labels :: preds) after
 
-    | I_aux (_, (_, l)) :: after ->
-       Reporting.unreachable l __POS__ "Could not add instruction to control-flow graph"
-
-    | [] -> preds
+    | T_none -> preds
   in
 
   let start = add_vertex ([], CF_start NameMap.empty) graph in
@@ -422,7 +455,7 @@ let place_phi_functions graph df =
 
   let orig_A n =
     match graph.nodes.(n) with
-    | Some ((_, CF_block instrs), _, _) ->
+    | Some ((_, CF_block (instrs, _)), _, _) ->
        let vars = List.fold_left NameCTSet.union NameCTSet.empty (List.map instr_typed_writes instrs) in
        let vars = NameCTSet.diff vars (all_decls instrs) in
        all_vars := NameCTSet.union vars !all_vars;
@@ -542,21 +575,32 @@ let rename_variables graph root children =
          counts := NameMap.add id i !counts;
          push_stack id i;
          I_init (ctyp, ssa_name i id, cval)
-      | I_jump (cval, label) ->
-         I_jump (fold_cval cval, label)
-      | I_end id ->
-         let i = top_stack id in
-         I_end (ssa_name i id)
       | instr -> instr
     in
     I_aux (aux, annot)
   in
 
+  let ssa_terminator = function
+    | T_jump (cond, label) ->
+       begin match IntMap.find_opt cond graph.conds with
+       | Some cval ->
+          graph.conds <- IntMap.add cond (fold_cval cval) graph.conds;
+          T_jump (cond, label)
+       | None -> assert false
+       end
+    | T_end id ->
+       let i = top_stack id in
+       T_end (ssa_name i id)
+    | terminator -> terminator
+  in
+
   let ssa_cfnode = function
     | CF_start inits -> CF_start inits
-    | CF_block instrs -> CF_block (List.map ssa_instr instrs)
+    | CF_block (instrs, terminator) ->
+       let instrs = List.map ssa_instr instrs in
+       CF_block (instrs, ssa_terminator terminator)
     | CF_label label -> CF_label label
-    | CF_guard cval -> CF_guard (fold_cval cval)
+    | CF_guard cond -> CF_guard cond
   in
 
   let ssa_ssanode = function
@@ -612,7 +656,12 @@ let rename_variables graph root children =
 
 let place_pi_functions graph start idom children =
   let get_guard = function
-    | CF_guard guard -> [guard]
+    | CF_guard cond ->
+       begin match IntMap.find_opt (abs cond) graph.conds with
+       | Some guard when cond > 0 -> [guard]
+       | Some guard -> [V_call (Bnot, [guard])]
+       | None -> assert false
+       end
     | _ -> []
   in
   let get_pi_contents ssanodes =
@@ -681,9 +730,9 @@ let string_of_phis = function
 
 let string_of_node = function
   | (phis, CF_label label) -> string_of_phis phis ^ label
-  | (phis, CF_block instrs) -> string_of_phis phis ^ Util.string_of_list "\\l" (fun instr -> String.escaped (Pretty_print_sail.to_string (pp_instr ~short:true instr))) instrs
+  | (phis, CF_block (instrs, terminator)) -> string_of_phis phis ^ Util.string_of_list "\\l" (fun instr -> String.escaped (Pretty_print_sail.to_string (pp_instr ~short:true instr))) instrs
   | (phis, CF_start inits) -> string_of_phis phis ^ "START"
-  | (phis, CF_guard cval) -> string_of_phis phis ^ (String.escaped (Pretty_print_sail.to_string (pp_cval cval)))
+  | (phis, CF_guard cval) -> string_of_phis phis ^ string_of_int cval
 
 let vertex_color = function
   | (_, CF_start _) -> "peachpuff"
diff --git a/src/jib/jib_ssa.mli b/src/jib/jib_ssa.mli
index 759e1ccb..dadb20fd 100644
--- a/src/jib/jib_ssa.mli
+++ b/src/jib/jib_ssa.mli
@@ -60,6 +60,8 @@ val make : initial_size:int -> unit -> 'a array_graph
 
 module IntSet : Set.S with type elt = int
 
+val get_cond : 'a array_graph -> int -> Jib.cval
+     
 val get_vertex : 'a array_graph -> int -> ('a * IntSet.t * IntSet.t) option
 
 val iter_graph : ('a -> IntSet.t -> IntSet.t -> unit) -> 'a array_graph -> unit
@@ -77,10 +79,19 @@ exception Not_a_DAG of int
 
 val topsort : 'a array_graph -> int list
 
+type terminator =
+  | T_undefined of Jib.ctyp
+  | T_match_failure
+  | T_end of Jib.name
+  | T_goto of string
+  | T_jump of int * string
+  | T_label of string
+  | T_none
+
 type cf_node =
   | CF_label of string
-  | CF_block of Jib.instr list
-  | CF_guard of Jib.cval
+  | CF_block of Jib.instr list * terminator
+  | CF_guard of int
   | CF_start of Jib.ctyp NameMap.t
 
 val control_flow_graph : Jib.instr list -> int * int list * ('a list * cf_node) array_graph
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index 378f5fae..3326d4ad 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -278,6 +278,8 @@ let string_of_name ?deref_current_exception:(dce=true) ?zencode:(zencode=true) =
 
 let string_of_op = function
   | Bnot -> "@not"
+  | Band -> "@and"
+  | Bor -> "@or"
   | List_hd -> "@hd"
   | List_tl -> "@tl"
   | Bit_to_bool -> "@bit_to_bool"
@@ -896,6 +898,8 @@ let rec infer_call op vs =
   match op, vs with
   | Bit_to_bool, _ -> CT_bool
   | Bnot, _ -> CT_bool
+  | Band, _ -> CT_bool
+  | Bor, _ -> CT_bool
   | List_hd, [v] ->
      begin match cval_ctyp v with
      | CT_list ctyp -> ctyp
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 55928e06..37e99662 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -920,8 +920,7 @@ let doc_lit (L_aux(lit,l)) =
       let denom = Big_int.pow_int_positive 10 (String.length f) in
       (Big_int.add (Big_int.mul (Big_int.of_string i) denom) (Big_int.of_string f), denom)
     | _ ->
-      raise (Reporting.Fatal_error
-        (Reporting.Err_syntax_locn (l, "could not parse real literal"))) in
+      raise (Reporting.err_syntax_loc l "could not parse real literal") in
     parens (separate space (List.map string [
       "realFromFrac"; Big_int.to_string num; Big_int.to_string denom]))
 
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index ae86a0fd..89830d38 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -423,8 +423,7 @@ let doc_lit_lem (L_aux(lit,l)) =
       let denom = Big_int.pow_int_positive 10 (String.length f) in
       (Big_int.add (Big_int.mul (Big_int.of_string i) denom) (Big_int.of_string f), denom)
     | _ ->
-      raise (Reporting.Fatal_error
-        (Reporting.Err_syntax_locn (l, "could not parse real literal"))) in
+      raise (Reporting.err_syntax_loc l "could not parse real literal") in
     parens (separate space (List.map string [
       "realFromFrac"; Big_int.to_string num; Big_int.to_string denom]))
 
diff --git a/src/property.mli b/src/property.mli
index 3789fa63..f84a85e3 100644
--- a/src/property.mli
+++ b/src/property.mli
@@ -90,6 +90,8 @@ val rewrite : tannot defs -> tannot defs
 
 type event = Overflow | Assertion | Assumption | Match | Return
 
+val string_of_event : event -> string
+
 module Event : sig
   type t = event
   val compare : event -> event -> int
diff --git a/src/reporting.ml b/src/reporting.ml
index c85f20ff..9387ee6b 100644
--- a/src/reporting.ml
+++ b/src/reporting.ml
@@ -133,7 +133,7 @@ type error =
   | Err_unreachable of Parse_ast.l * (string * int * int * int) * string
   | Err_todo of Parse_ast.l * string
   | Err_syntax of Lexing.position * string
-  | Err_syntax_locn of Parse_ast.l * string
+  | Err_syntax_loc of Parse_ast.l * string
   | Err_lex of Lexing.position * string
   | Err_type of Parse_ast.l * string
 
@@ -145,7 +145,7 @@ let dest_err = function
      (Printf.sprintf "Internal error: Unreachable code (at \"%s\" line %d)" file line, Loc l, m ^ issues)
   | Err_todo (l, m) -> ("Todo" ^ m, Loc l, "")
   | Err_syntax (p, m) -> ("Syntax error", Pos p, m)
-  | Err_syntax_locn (l, m) -> ("Syntax error", Loc l, m)
+  | Err_syntax_loc (l, m) -> ("Syntax error", Loc l, m)
   | Err_lex (p, s) -> ("Lexical error", Pos p, s)
   | Err_type (l, m) -> ("Type error", Loc l, m)
 
@@ -156,6 +156,7 @@ let err_todo l m = Fatal_error (Err_todo (l, m))
 let err_unreachable l ocaml_pos m = Fatal_error (Err_unreachable (l, ocaml_pos, m))
 let err_general l m = Fatal_error (Err_general (l, m))
 let err_typ l m = Fatal_error (Err_type (l,m))
+let err_syntax_loc l m = Fatal_error (Err_syntax_loc (l, m))
 
 let unreachable l pos msg =
   raise (err_unreachable l pos msg)
diff --git a/src/reporting.mli b/src/reporting.mli
index 86399e84..28f2a799 100644
--- a/src/reporting.mli
+++ b/src/reporting.mli
@@ -93,7 +93,7 @@ type error =
   | Err_todo of Parse_ast.l * string
 
   | Err_syntax of Lexing.position * string
-  | Err_syntax_locn of Parse_ast.l * string
+  | Err_syntax_loc of Parse_ast.l * string
   | Err_lex of Lexing.position * string
   | Err_type of Parse_ast.l * string
 
@@ -111,6 +111,9 @@ val err_unreachable : Parse_ast.l -> (string * int * int * int) -> string -> exn
 (** [err_typ l m] is an abreviatiation for [Fatal_error (Err_type (l, m))] *)
 val err_typ : Parse_ast.l -> string -> exn
 
+(** [err_syntax_loc] is an abbreviation for [Fatal_error (Err_syntax_loc (l, m))] *)
+val err_syntax_loc : Parse_ast.l -> string -> exn
+  
 val unreachable : Parse_ast.l -> (string * int * int * int) -> string -> 'a
 
 val print_error : error -> unit
diff --git a/src/sail.ml b/src/sail.ml
index 13fea6f2..eff90fa3 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -321,6 +321,9 @@ let options = Arg.align ([
   ( "-ddump_flow_graphs",
     Arg.Set Jib_compile.opt_debug_flow_graphs,
     " (debug) dump flow analysis for Sail functions when compiling to C");
+  ( "-ddump_smt_graphs",
+    Arg.Set Jib_smt.opt_debug_graphs,
+    " (debug) dump flow analysis for properties when generating SMT");
   ( "-dtc_verbose",
     Arg.Int (fun verbosity -> Type_check.opt_tc_debug := verbosity),
     "<verbosity> (debug) verbose typechecker output: 0 is silent");
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 83d58178..13ed491b 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -193,6 +193,10 @@ let sint = function
 
 let add_int (x, y) = Big_int.add x y
 let sub_int (x, y) = Big_int.sub x y
+let sub_nat (x, y) =
+  let z = Big_int.sub x y in
+  if Big_int.less z Big_int.zero then Big_int.zero else z
+
 let mult (x, y) = Big_int.mul x y
 
 (* This is euclidian division from lem *)
diff --git a/src/smtlib.ml b/src/smtlib.ml
index 7f485447..ab6ebf55 100644
--- a/src/smtlib.ml
+++ b/src/smtlib.ml
@@ -100,6 +100,16 @@ type smt_exp =
   | Extract of int * int * smt_exp
   | Tester of string * smt_exp
 
+let smt_conj = function
+  | [] -> Bool_lit true
+  | [x] -> x
+  | xs -> Fn ("and", xs)
+
+let smt_disj = function
+  | [] -> Bool_lit false
+  | [x] -> x
+  | xs -> Fn ("or", xs)
+
 let extract i j x = Extract (i, j, x)
 
 let bvnot x    = Fn ("bvnot", [x])
@@ -172,6 +182,8 @@ type smt_def =
   | Define_fun of string * (string * smt_typ) list * smt_typ * smt_exp
   | Declare_const of string * smt_typ
   | Define_const of string * smt_typ * smt_exp
+  | Write_mem of string * smt_exp * smt_exp * smt_exp
+  | Read_mem of string * smt_typ * smt_exp * smt_exp
   | Declare_datatypes of string * (string * (string * smt_typ) list) list
   | Declare_tuple of int
   | Assert of smt_exp
@@ -232,6 +244,12 @@ let pp_smt_def =
   | Define_const (name, ty, exp) ->
      pp_sfun "define-const" [string name; pp_smt_typ ty; pp_smt_exp exp]
 
+  | Write_mem (name, wk, addr, data) ->
+     pp_sfun "declare-const" [string name; pp_smt_typ Bool]
+
+  | Read_mem (name, ty, rk, addr) ->
+     pp_sfun "declare-const" [string name; pp_smt_typ ty]
+
   | Declare_datatypes (name, ctors) ->
      let pp_ctor (ctor_name, fields) =
        match fields with
diff --git a/src/type_check.ml b/src/type_check.ml
index 2ce6ea94..2be68ade 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -903,7 +903,7 @@ end = struct
     try
       Bindings.find id env.top_val_specs
     with
-    | Not_found -> typ_error env (id_loc id) ("No val spec found for " ^ string_of_id id)
+    | Not_found -> typ_error env (id_loc id) ("No type signature found for " ^ string_of_id id)
 
   let get_val_spec id env =
     try
diff --git a/src/value.ml b/src/value.ml
index 2760b220..6c2e0839 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -350,11 +350,8 @@ let value_sub_int = function
   | _ -> failwith "value sub"
 
 let value_sub_nat = function
-  | [v1; v2] -> V_int (
-                    let n = Sail_lib.sub_int (coerce_int v1, coerce_int v2) in
-                    if Big_int.less_equal n Big_int.zero then Big_int.zero else n
-                  )
-  | _ -> failwith "value sub_int"
+  | [v1; v2] -> V_int (Sail_lib.sub_nat (coerce_int v1, coerce_int v2))
+  | _ -> failwith "value sub_nat"
 
 let value_negate = function
   | [v1] -> V_int (Sail_lib.negate (coerce_int v1))
diff --git a/test/smt/assembly_mapping.sat.sail b/test/smt/assembly_mapping.sat.sail
new file mode 100644
index 00000000..a7b0bec5
--- /dev/null
+++ b/test/smt/assembly_mapping.sat.sail
@@ -0,0 +1,64 @@
+default Order dec
+
+$include <prelude.sail>
+$include <string.sail>
+$include <mapping.sail>
+
+type regbits  = bits(5)
+
+val reg_name : bits(5) <-> string
+mapping reg_name = {
+  0b00000 <-> "zero",
+  0b00001 <-> "ra",
+  0b00010 <-> "sp",
+  0b00011 <-> "gp",
+  0b00100 <-> "tp",
+  0b00101 <-> "t0",
+  0b00110 <-> "t1",
+  0b00111 <-> "t2",
+  0b01000 <-> "fp",
+  0b01001 <-> "s1",
+  0b01010 <-> "a0",
+  0b01011 <-> "a1",
+  0b01100 <-> "a2",
+  0b01101 <-> "a3",
+  0b01110 <-> "a4",
+  0b01111 <-> "a5",
+  0b10000 <-> "a6",
+  0b10001 <-> "a7",
+  0b10010 <-> "s2",
+  0b10011 <-> "s3",
+  0b10100 <-> "s4",
+  0b10101 <-> "s5",
+  0b10110 <-> "s6",
+  0b10111 <-> "s7",
+  0b11000 <-> "s8",
+  0b11001 <-> "s9",
+  0b11010 <-> "s10",
+  0b11011 <-> "s11",
+  0b11100 <-> "t3",
+  0b11101 <-> "t4",
+  0b11110 <-> "t5",
+  0b11111 <-> "t6"
+}
+
+enum uop = RISCV_LUI | RISCV_AUIPC
+
+mapping utype_mnemonic : uop <-> string = {
+  RISCV_LUI   <-> "lui",
+  RISCV_AUIPC <-> "auipc"
+}
+
+val assembly : ast <-> string
+
+scattered union ast
+
+union clause ast = UTYPE : (bits(20), regbits, uop)
+
+mapping clause assembly = UTYPE(imm, rd, op)
+  <-> utype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_20(imm)
+
+$counterexample
+function prop(x: string) -> bool = {
+  not_bool(assembly(UTYPE(0x00000, 0b00000, RISCV_LUI)) == x)
+}
diff --git a/test/smt/encdec.sat.sail b/test/smt/encdec.sat.sail
new file mode 100644
index 00000000..d34f3629
--- /dev/null
+++ b/test/smt/encdec.sat.sail
@@ -0,0 +1,64 @@
+default Order dec
+
+$include <prelude.sail>
+$include <string.sail>
+$include <mapping.sail>
+
+type regbits  = bits(5)
+
+val reg_name : bits(5) <-> string
+mapping reg_name = {
+  0b00000 <-> "zero",
+  0b00001 <-> "ra",
+  0b00010 <-> "sp",
+  0b00011 <-> "gp",
+  0b00100 <-> "tp",
+  0b00101 <-> "t0",
+  0b00110 <-> "t1",
+  0b00111 <-> "t2",
+  0b01000 <-> "fp",
+  0b01001 <-> "s1",
+  0b01010 <-> "a0",
+  0b01011 <-> "a1",
+  0b01100 <-> "a2",
+  0b01101 <-> "a3",
+  0b01110 <-> "a4",
+  0b01111 <-> "a5",
+  0b10000 <-> "a6",
+  0b10001 <-> "a7",
+  0b10010 <-> "s2",
+  0b10011 <-> "s3",
+  0b10100 <-> "s4",
+  0b10101 <-> "s5",
+  0b10110 <-> "s6",
+  0b10111 <-> "s7",
+  0b11000 <-> "s8",
+  0b11001 <-> "s9",
+  0b11010 <-> "s10",
+  0b11011 <-> "s11",
+  0b11100 <-> "t3",
+  0b11101 <-> "t4",
+  0b11110 <-> "t5",
+  0b11111 <-> "t6"
+}
+
+enum uop = RISCV_LUI | RISCV_AUIPC
+
+mapping utype_mnemonic : uop <-> string = {
+  RISCV_LUI   <-> "lui",
+  RISCV_AUIPC <-> "auipc"
+}
+
+val assembly : ast <-> string
+
+scattered union ast
+
+union clause ast = UTYPE : (bits(20), regbits, uop)
+
+mapping clause assembly = UTYPE(imm, rd, op)
+  <-> utype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_20(imm)
+
+$counterexample
+function prop(x: string) -> bool = {
+  not_bool(utype_mnemonic(RISCV_LUI) == x)
+}
diff --git a/test/smt/run_tests.py b/test/smt/run_tests.py
index c9cadec3..f59bdba9 100755
--- a/test/smt/run_tests.py
+++ b/test/smt/run_tests.py
@@ -23,7 +23,7 @@ def test_smt(name, solver, sail_opts):
             tests[filename] = os.fork()
             if tests[filename] == 0:
                 step('sail {} -smt {} -o {}'.format(sail_opts, filename, basename))
-                step('timeout 20s {} {}_prop.smt2 1> {}.out'.format(solver, basename, basename))
+                step('timeout 300s {} {}_prop.smt2 1> {}.out'.format(solver, basename, basename))
                 if re.match('.+\.sat\.sail$', filename):
                     step('grep -q ^sat$ {}.out'.format(basename))
                 else:
diff --git a/test/smt/rv_add_0.unsat.sail b/test/smt/rv_add_0.unsat.sail
index 87c55487..ed45112e 100644
--- a/test/smt/rv_add_0.unsat.sail
+++ b/test/smt/rv_add_0.unsat.sail
@@ -145,7 +145,7 @@ function clause execute (ITYPE (imm, rs1, rd, RISCV_ADDI)) =
 
 function clause decode _ = None()
 
-$counterexample
+$property
 function prop(imm:  bits(12), rs1: regbits, rd: regbits, v: xlenbits) -> bool = {
   X(rs1) = v;
   match decode(imm @ rs1 @ 0b000 @ rd @ 0b0010011) {
diff --git a/test/smt/store_load.sat.sail b/test/smt/store_load.sat.sail
new file mode 100644
index 00000000..810bbfbb
--- /dev/null
+++ b/test/smt/store_load.sat.sail
@@ -0,0 +1,55 @@
+default Order dec
+
+$include <prelude.sail>
+$include <regfp.sail>
+
+register x0 : bits(32)
+register x1 : bits(32)
+register x2 : bits(32)
+register x3 : bits(32)
+
+function wX(r: bits(2), v: bits(32)) -> unit = {
+  match r {
+    0b00 => x0 = v,
+    0b01 => x1 = v,
+    0b10 => x2 = v,
+    0b11 => x3 = v
+  }
+}
+
+function rX(r: bits(2)) -> bits(32) = {
+  match r {
+    0b00 => x0,
+    0b01 => x1,
+    0b10 => x2,
+    0b11 => x3
+  }
+}
+
+overload X = {rX, wX}
+
+scattered union ast
+
+val execute : ast -> bool
+
+union clause ast = LOAD : (bits(2), bits(2))
+
+function clause execute(LOAD(rd, rs)) = {
+  X(rd) = __read_mem(Read_plain, 32, X(rs), 4);
+  true
+}
+
+union clause ast = STORE : (bits(2), bits(2))
+
+function clause execute(STORE(rd, rs)) = {
+  let addr = X(rd);
+  __write_mem(Write_plain, 32, addr, 4, X(rs))
+}
+
+/* Default memory model is as weak as possible, so this is not true */
+$counterexample
+function prop() -> bool = {
+  let _ = execute(STORE(0b01, 0b10));
+  let _ = execute(LOAD(0b00, 0b01));
+  X(0b00) == X(0b10)
+}