SMT: Add property and counterexample directive

Rather than generating SMT from a function called check_sat, now find
any function with a $property directive and generate SMT for it, e.g.

$property
function prop_cap_round_trip(cap: bits(128)) -> bool = {
  let cap_rt = capToBits(capBitsToCapability(true, cap));
  cap == cap_rt
}

$property
function prop_base_lteq_top(capbits: bits(128)) -> bool = {
  let c = capBitsToCapability(true, capbits);
  let (base, top) = getCapBounds(c);
  let e = unsigned(c.E);
  e >= 51 | base <= top
}

The file property.ml has a function for gathering all the properties
in a file, as well as a rewrite-pass for properties with type
quantifiers, which allows us to handle properties like

function prop forall 'n, 'n <= 100. (bv: bits('n)) -> bool = exp

by rewriting to (conceptually)

function prop(bv: bits(MAX_BIT_WIDTH)) -> bool =
  if length(bv) > 100 then true else exp

The function return is now automatically negated (i.e. always true =
unsat, sometimes false = sat), which makes sense for quickcheck-type
properties.

58 files changed, 479 insertions, 203 deletions

diff --git a/editors/sail-mode.el b/editors/sail-mode.el
index af336d7a..a0d98429 100644
--- a/editors/sail-mode.el
+++ b/editors/sail-mode.el
@@ -45,7 +45,7 @@
 
 (defconst sail2-special
   '("_prove" "_not_prove" "create" "kill" "convert" "undefined"
-    "$define" "$include" "$ifdef" "$ifndef" "$else" "$endif" "$option" "$optimize" "$latex"))
+    "$define" "$include" "$ifdef" "$ifndef" "$else" "$endif" "$option" "$optimize" "$latex" "$property" "$counterexample"))
 
 (defconst sail2-font-lock-keywords
   `((,(regexp-opt sail2-keywords 'symbols) . font-lock-keyword-face)
diff --git a/src/error_format.ml b/src/error_format.ml
index 8e00c2b7..672373a2 100644
--- a/src/error_format.ml
+++ b/src/error_format.ml
@@ -50,7 +50,10 @@ let underline_double_from color cnum_from eol =
   Util.(String.make cnum_from ' ' ^ clear (color ("^" ^ String.make (eol - cnum_from - 1) '-')))
 
 let underline_double_to color cnum_to =
-  Util.(clear (color (String.make (cnum_to - 1) '-' ^ "^")))
+  if cnum_to = 0 then
+    Util.(clear (color "^"))
+  else
+    Util.(clear (color (String.make (cnum_to - 1) '-' ^ "^")))
 
 let format_code_double' fname in_chan lnum_from cnum_from lnum_to cnum_to contents ppf =
   skip_lines in_chan (lnum_from - 1);
@@ -85,7 +88,7 @@ let format_code_double fname lnum_from cnum_from lnum_to cnum_to contents ppf =
     begin
       try format_code_double' fname in_chan lnum_from cnum_from lnum_to cnum_to contents ppf; close_in in_chan
       with
-      | _ -> close_in_noerr in_chan; ()
+      | exn -> close_in_noerr in_chan; ()
     end
   with
   | _ -> ()
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 23ea6706..af2c7284 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -847,7 +847,7 @@ let smt_instr env =
      let checks =
        Stack.fold (fun checks -> function (Define_const (name, _, _) as def) -> (name, def) :: checks | _ -> assert false) [] overflow_checks
      in
-     List.map snd checks @ [Assert (Fn ("and", Var (zencode_name id) :: List.map (fun check -> Var (fst check)) checks))]
+     List.map snd checks @ [Assert (Fn ("and", Fn ("not", [Var (zencode_name id)]) :: List.map (fun check -> Var (fst check)) checks))]
 
   | I_aux (I_clear _, _) -> []
 
@@ -879,60 +879,6 @@ let rec find_function id = function
      find_function id cdefs
   | [] -> None
 
-let smt_cdef stack env all_cdefs = function
-  | CDEF_spec (function_id, arg_ctyps, ret_ctyp)
-       when string_of_id function_id = "check_sat" ->
-     begin match find_function function_id all_cdefs with
-     | Some (None, args, instrs) ->
-        let open Jib_ssa in
-        let smt_args =
-          List.map2 (fun id ctyp -> declare_const (Name (id, 0)) ctyp) args arg_ctyps
-        in
-        push_smt_defs stack smt_args;
-
-        let instrs =
-          let open Jib_optimize in
-          instrs
-          (* |> optimize_unit *)
-          |> inline all_cdefs (fun _ -> true)
-          |> flatten_instrs
-          |> remove_pointless_goto
-        in
-
-        let str = Pretty_print_sail.to_string PPrint.(separate_map hardline Jib_util.pp_instr instrs) in
-        prerr_endline str;
-
-        let start, cfg = ssa instrs in
-        let chan = open_out "smt_ssa.gv" in
-        make_dot chan cfg;
-        close_out chan;
-
-        let visit_order = topsort cfg in
-
-        List.iter (fun n ->
-            begin match get_vertex cfg n with
-            | None -> ()
-            | Some ((ssanodes, cfnode), preds, succs) ->
-               let muxers =
-                 ssanodes |> List.map (smt_ssanode env cfg preds) |> List.concat
-               in
-               let basic_block = smt_cfnode all_cdefs env cfnode in
-               push_smt_defs stack muxers;
-               push_smt_defs stack basic_block;
-            end
-          ) visit_order
-
-     | _ -> failwith "Bad function body"
-     end
-  | _ -> ()
-
-let rec smt_cdefs stack env ast =
-  function
-  | cdef :: cdefs ->
-     smt_cdef stack env ast cdef;
-     smt_cdefs stack env ast cdefs
-  | [] -> ()
-
 let optimize_smt stack =
   let stack' = Stack.create () in
   let uses = Hashtbl.create (Stack.length stack) in
@@ -998,7 +944,92 @@ let optimize_smt stack =
   Stack.iter constant_propagate stack';
   queue
 
-let generate_smt out_chan env ast =
+(** [smt_header stack cdefs] pushes all the type declarations required
+   for cdefs onto the SMT stack *)
+let smt_header stack cdefs =
+  push_smt_defs stack
+    [declare_datatypes (mk_enum "Unit" ["unit"]);
+     Declare_tuple 2;
+     Declare_tuple 3;
+     Declare_tuple 4;
+     Declare_tuple 5;
+     declare_datatypes (mk_record "Bits" [("len", Bitvec !lbits_index);
+                                          ("contents", Bitvec (lbits_size ()))])
+
+    ];
+  let smt_type_defs = List.concat (generate_ctype_defs cdefs) in
+  push_smt_defs stack smt_type_defs
+
+let smt_cdef props name_file env 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
+     | Some (None, args, instrs) ->
+        let prop_type, prop_args, pragma_l, vs = Bindings.find function_id props in
+
+        let stack = Stack.create () in
+
+        smt_header stack all_cdefs;
+        let smt_args =
+          List.map2 (fun id ctyp -> declare_const (Name (id, 0)) ctyp) args arg_ctyps
+        in
+        push_smt_defs stack smt_args;
+
+        let instrs =
+          let open Jib_optimize in
+          instrs
+          (* |> optimize_unit *)
+          |> inline all_cdefs (fun _ -> true)
+          |> flatten_instrs
+          |> remove_pointless_goto
+        in
+
+        (* let str = Pretty_print_sail.to_string PPrint.(separate_map hardline Jib_util.pp_instr instrs) in
+        prerr_endline str; *)
+
+        let open Jib_ssa in
+        let start, cfg = ssa instrs in
+        (* let chan = open_out "smt_ssa.gv" in
+        make_dot chan cfg;
+        close_out chan; *)
+
+        let visit_order = topsort cfg in
+
+        List.iter (fun n ->
+            begin match get_vertex cfg n with
+            | None -> ()
+            | Some ((ssanodes, cfnode), preds, succs) ->
+               let muxers =
+                 ssanodes |> List.map (smt_ssanode env cfg preds) |> List.concat
+               in
+               let basic_block = smt_cfnode all_cdefs env cfnode in
+               push_smt_defs stack muxers;
+               push_smt_defs stack basic_block;
+            end
+          ) visit_order;
+
+        let out_chan = open_out (name_file (string_of_id function_id)) in
+        output_string out_chan "(set-logic QF_AUFBVDT)\n";
+
+        (* let stack' = Stack.create () in
+        Stack.iter (fun def -> Stack.push def stack') stack;
+        Stack.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") stack'; *)
+        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;
+
+        output_string out_chan "(check-sat)\n"
+
+     | _ -> failwith "Bad function body"
+     end
+  | _ -> ()
+
+let rec smt_cdefs props name_file env ast =
+  function
+  | cdef :: cdefs ->
+     smt_cdef props name_file env ast cdef;
+     smt_cdefs props name_file env ast cdefs
+  | [] -> ()
+
+let generate_smt props name_file env ast =
   try
     let open Jib_compile in
     let ctx =
@@ -1011,33 +1042,7 @@ let generate_smt out_chan env ast =
     let cdefs, ctx = compile_ast { ctx with specialize_calls = true; ignore_64 = true } ast in
     Profile.finish "Compiling to Jib IR" t;
 
-    let stack = Stack.create () in
-
-    (* output_string out_chan "(set-option :produce-models true)\n"; *)
-    output_string out_chan "(set-logic QF_AUFBVDT)\n";
-    push_smt_defs stack
-      [declare_datatypes (mk_enum "Unit" ["unit"]);
-       Declare_tuple 2;
-       Declare_tuple 3;
-       Declare_tuple 4;
-       Declare_tuple 5;
-       declare_datatypes (mk_record "Bits" [("len", Bitvec !lbits_index);
-                                            ("contents", Bitvec (lbits_size ()))])
-
-      ];
-
-    let smt_type_defs = List.concat (generate_ctype_defs cdefs) in
-    push_smt_defs stack smt_type_defs;
-
-    smt_cdefs stack env cdefs cdefs;
-
-    (* let stack' = Stack.create () in
-    Stack.iter (fun def -> Stack.push def stack') stack;
-    Stack.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") stack'; *)
-    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;
-
-    output_string out_chan "(check-sat)\n"
+    smt_cdefs props name_file env cdefs cdefs
   with
   | Type_check.Type_error (_, l, err) ->
      raise (Reporting.err_typ l (Type_error.string_of_type_error err));
diff --git a/src/property.ml b/src/property.ml
new file mode 100644
index 00000000..37212098
--- /dev/null
+++ b/src/property.ml
@@ -0,0 +1,121 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open Ast
+open Ast_util
+
+let find_properties (Defs defs) =
+  let rec find_prop acc = function
+    | DEF_pragma (("property" | "counterexample") as prop_type, command, l) :: defs ->
+       begin match Util.find_next (function DEF_spec _ -> true | _ -> false) defs with
+       | _, Some (DEF_spec vs, defs) ->
+          find_prop ((prop_type, command, l, vs) :: acc) defs
+       | _, _ ->
+          raise (Reporting.err_general l "Property is not attached to any function signature")
+       end
+    | def :: defs -> find_prop acc defs
+    | [] -> acc
+  in
+  find_prop [] defs
+  |> List.map (fun ((_, _, _, vs) as prop) -> (id_of_val_spec vs, prop))
+  |> List.fold_left (fun m (id, prop) -> Bindings.add id prop m) Bindings.empty
+
+let add_property_guards props (Defs defs) =
+  let open Type_check in
+  let rec add_property_guards' acc = function
+    | (DEF_fundef (FD_aux (FD_function (r_opt, t_opt, e_opt, funcls), fd_aux) as fdef) as def) :: defs ->
+       begin match Bindings.find_opt (id_of_fundef fdef) props with
+       | Some (_, _, pragma_l, VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (quant, _), _), _, _, _), _)) ->
+          begin match quant_split quant with
+          | _, [] -> add_property_guards' (def :: acc) defs
+          | _, constraints ->
+             let add_constraints_to_funcl (FCL_aux (FCL_Funcl (id, Pat_aux (pexp, pexp_aux)), fcl_aux)) =
+               let add_guard exp =
+                 let exp' = mk_exp (E_if (mk_exp (E_constraint (nc_not (List.fold_left nc_and nc_true constraints))),
+                                          mk_lit_exp L_true,
+                                          strip_exp exp)) in
+                 try Type_check.check_exp (env_of exp) exp' (typ_of exp) with
+                 | Type_error (_, l, err) ->
+                    let msg =
+                      "\nType error when generating guard for a property.\n\
+                       When generating guards we convert type quantifiers from the function signature\n\
+                       into runtime checks so it must be possible to reconstruct the quantifier from\n\
+                       the function arguments. For example:\n\n\
+                       \
+                       function f : forall 'n, 'n <= 100. (x: int('n)) -> bool\n\n\
+                       \
+                       would cause the runtime check x <= 100 to be added to the function body.\n\
+                       To fix this error, ensure that all quantifiers have corresponding function arguments.\n"
+                    in
+                    raise (Reporting.err_typ pragma_l (Type_error.string_of_type_error err ^ msg))
+               in
+               let mk_funcl p = FCL_aux (FCL_Funcl (id, Pat_aux (p, pexp_aux)), fcl_aux) in
+               match pexp with
+               | Pat_exp (pat, exp) ->
+                  mk_funcl (Pat_exp (pat, add_guard exp))
+               | Pat_when (pat, guard, exp) ->
+                  mk_funcl (Pat_when (pat, guard, add_guard exp))
+             in
+
+             let funcls = List.map add_constraints_to_funcl funcls in
+             let fdef = FD_aux (FD_function (r_opt, t_opt, e_opt, funcls), fd_aux) in
+
+             add_property_guards' (DEF_fundef fdef :: acc) defs
+          end
+       | None -> add_property_guards' (def :: acc) defs
+       end
+
+    | def :: defs -> add_property_guards' (def :: acc) defs
+    | [] -> List.rev acc
+  in
+  Defs (add_property_guards' [] defs)
+
+let rewrite defs =
+  add_property_guards (find_properties defs) defs
diff --git a/src/property.mli b/src/property.mli
new file mode 100644
index 00000000..fa24377a
--- /dev/null
+++ b/src/property.mli
@@ -0,0 +1,89 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+(** This file implements utilities for dealing with $property and
+   $counterexample pragmas. *)
+
+open Ast
+open Ast_util
+open Type_check
+
+(** [find_properties defs] returns a mapping from ids to of 4-tuples of the form
+   (prop_type, command, loc, val_spec), which contains the information
+   from any pragmas of the form
+
+   $prop_type command
+   ...
+   val <val_spec>
+
+   where prop_type is either "counterexample" or "property" and the
+   location loc is the location that was attached to the pragma
+*)
+val find_properties : 'a defs -> (string * string * l * 'a val_spec) Bindings.t
+
+(** For a property
+
+   $prop_type val f : forall X, C. T -> bool
+
+   find the function body for id:
+
+   function f(args) = exp
+
+   and rewrite the function body to
+
+   function f(args) = if constraint(not(C)) then true else exp
+
+   The reason we do this is that the type information in T constrained
+   by C might be lost when translating to Jib, as Jib types are
+   simpler and less precise. If we then do random test
+   generation/proving we want to ensure that inputs outside the
+   constraints of the function are ignored.
+*)
+val rewrite : tannot defs -> tannot defs
diff --git a/src/reporting.ml b/src/reporting.ml
index 20e44c57..c85f20ff 100644
--- a/src/reporting.ml
+++ b/src/reporting.ml
@@ -117,14 +117,14 @@ let rec simp_loc = function
   | Parse_ast.Generated l -> simp_loc l
   | Parse_ast.Range (p1, p2) -> Some (p1, p2)
   | Parse_ast.Documented (_, l) -> simp_loc l
-  
+
 let short_loc_to_string l =
   match simp_loc l with
   | None -> "unknown location"
   | Some (p1, p2) ->
      Printf.sprintf "%s %d:%d - %d:%d"
        p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) p2.pos_lnum (p2.pos_cnum - p2.pos_bol)
-  
+
 let print_err l m1 m2 =
   print_err_internal (Loc l) m1 m2
 
diff --git a/src/rewrites.ml b/src/rewrites.ml
index b9276f93..f7544a7c 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -4754,7 +4754,8 @@ let all_rewrites = [
     ("overload_cast", Basic_rewriter rewrite_overload_cast);
     ("top_sort_defs", Basic_rewriter (fun _ -> top_sort_defs));
     ("constant_fold", Basic_rewriter (fun _ -> Constant_fold.rewrite_constant_function_calls));
-    ("split", String_rewriter (fun str -> Basic_rewriter (rewrite_split_fun_ctor_pats str)))
+    ("split", String_rewriter (fun str -> Basic_rewriter (rewrite_split_fun_ctor_pats str)));
+    ("properties", Basic_rewriter (fun _ -> Property.rewrite));
   ]
 
 let rewrites_lem = [
@@ -4922,7 +4923,7 @@ let rewrites_target tgt =
   | "ocaml" -> rewrites_ocaml
   | "c" -> rewrites_c
   | "ir" -> rewrites_c
-  | "smt" -> rewrites_c
+  | "smt" -> rewrites_c @ [("properties", [])]
   | "sail" -> []
   | "latex" -> []
   | "interpreter" -> rewrites_interpreter
diff --git a/src/sail.ml b/src/sail.ml
index 95da54b0..179c1a67 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -412,17 +412,18 @@ let target name out_name ast type_envs =
      if close then close_out output_chan else ()
 
   | Some "smt" ->
+     let open Ast_util in
+     let props = Property.find_properties ast in
+     Bindings.bindings props |> List.map fst |> IdSet.of_list |> Specialize.add_initial_calls;
      let ast_smt, type_envs = Specialize.(specialize typ_ord_specialization ast type_envs) in
      (* let ast_smt, type_envs = Specialize.(specialize' 1 int_specialization_with_externs ast_smt type_envs) in *)
-     let close, output_chan =
+     let name_file =
        match !opt_file_out with
-       | Some f -> Util.opt_colors := false; (true, open_out (f ^ ".smt2"))
-       | None -> false, stdout
+       | Some f -> fun str -> f ^ "_" ^ str ^ ".smt2"
+       | None -> fun str -> str ^ ".smt2"
      in
      Util.opt_warnings := true;
-     Jib_smt.generate_smt output_chan type_envs ast_smt;
-     flush output_chan;
-     if close then close_out output_chan else ()
+     Jib_smt.generate_smt props name_file type_envs ast_smt;
 
   | Some "lem" ->
      output "" (Lem_out (!opt_libs_lem)) [(out_name, type_envs, ast)]
diff --git a/src/specialize.ml b/src/specialize.ml
index 1da7208a..3063e4d5 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -485,7 +485,6 @@ let specialize_id_overloads instantiations id (Defs defs) =
 
 let initial_calls = ref (IdSet.of_list
   [ mk_id "main";
-    mk_id "check_sat";
     mk_id "__SetConfig";
     mk_id "__ListConfig";
     mk_id "execute";
diff --git a/src/util.ml b/src/util.ml
index 5ef9686d..6a2fb9bb 100644
--- a/src/util.ml
+++ b/src/util.ml
@@ -386,6 +386,14 @@ let rec take_drop f = function
      let (ys, zs) = take_drop f xs in
      (x :: ys, zs)
 
+let find_next f xs =
+  let rec find_next' f acc = function
+    | x :: xs when f x -> List.rev acc, Some (x, xs)
+    | x :: xs -> find_next' f (x :: acc) xs
+    | [] -> List.rev acc, None
+  in
+  find_next' f [] xs
+
 let is_none opt = not (is_some opt)
 
 let rec take n xs = match n, xs with
diff --git a/src/util.mli b/src/util.mli
index 06fd5eff..ddc5347f 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -194,6 +194,8 @@ val drop : int -> 'a list -> 'a list
 
 val take_drop : ('a -> bool) -> 'a list -> ('a list * 'a list)
 
+val find_next : ('a -> bool) -> 'a list -> ('a list * ('a * 'a list) option)
+
 val list_init : int -> (int -> 'a) -> 'a list
 
 (** {2 Files} *)
diff --git a/test/smt/basic_1.sat.sail b/test/smt/basic_1.sat.sail
index d40c5a59..a4c79660 100644
--- a/test/smt/basic_1.sat.sail
+++ b/test/smt/basic_1.sat.sail
@@ -15,7 +15,8 @@ struct S = {
 register R1 : bits(16)
 register R2 : bits(8)
 
-function check_sat(x: bool) -> bool = {
+$property
+function prop(x: bool) -> bool = {
   if x then {
     R1 = 0x007F
   } else {
diff --git a/test/smt/basic_1.unsat.sail b/test/smt/basic_1.unsat.sail
index cf469d75..9ce19539 100644
--- a/test/smt/basic_1.unsat.sail
+++ b/test/smt/basic_1.unsat.sail
@@ -15,11 +15,12 @@ struct S = {
 register R1 : bits(16)
 register R2 : bits(8)
 
-function check_sat(x: bool) -> bool = {
+$property
+function prop(x: bool) -> bool = {
   if false then {
     R1 = 0x007F
   } else {
     R1 = 0xFFFF
   };
-  R1 == sail_zero_extend(R2, 16)
+  not_bool(R1 == sail_zero_extend(R2, 16))
 }
diff --git a/test/smt/basic_2.sat.sail b/test/smt/basic_2.sat.sail
index 73b18446..132c92ba 100644
--- a/test/smt/basic_2.sat.sail
+++ b/test/smt/basic_2.sat.sail
@@ -15,7 +15,8 @@ struct S = {
 register R1 : bits(16)
 register R2 : bits(8)
 
-function check_sat(x: bool) -> bool = {
+$property
+function prop(x: bool) -> bool = {
   if x then {
     R1 = 0x00FF
   } else {
diff --git a/test/smt/basic_2.unsat.sail b/test/smt/basic_2.unsat.sail
index 1f3d8488..e87beec2 100644
--- a/test/smt/basic_2.unsat.sail
+++ b/test/smt/basic_2.unsat.sail
@@ -15,11 +15,12 @@ struct S = {
 register R1 : bits(16)
 register R2 : bits(8)
 
-function check_sat(x: bool) -> bool = {
+$property
+function prop(x: bool) -> bool = {
   if x then {
     R1 = 0x01FF
   } else {
     R1 = 0xFFFF
   };
-  R1 == sail_zero_extend(R2, 16)
+  R1 != sail_zero_extend(R2, 16)
 }
diff --git a/test/smt/ccheri_regression1.unsat.sail b/test/smt/ccheri_regression1.unsat.sail
index 808759cd..7b846a02 100644
--- a/test/smt/ccheri_regression1.unsat.sail
+++ b/test/smt/ccheri_regression1.unsat.sail
@@ -13,10 +13,11 @@ function operator <_u forall 'n, 'n >= 0. (x: bits('n), y: bits('n)) -> bool =
 
 overload ~ = {not_bool}
 
-function check_sat() -> bool = {
+$property
+function prop() -> bool = {
   let i1 = 0b110 == truncate(shiftr(0x531E02A72708B000, 11), 3);
   let i2 = 0b000 == truncateLSB(0b00001010000011, 3);
   let i3 = 0b101 == sub_vec(0b110, 0b001);
   let i4 = false == operator <_u(0b110, 0b101);
-  ~(i1 & i2 & i3 & i4)
+  i1 & i2 & i3 & i4
 }
\ No newline at end of file
diff --git a/test/smt/concat_prop.unsat.sail b/test/smt/concat_prop.unsat.sail
index 417152d5..857f7f33 100644
--- a/test/smt/concat_prop.unsat.sail
+++ b/test/smt/concat_prop.unsat.sail
@@ -5,7 +5,8 @@ $include <prelude.sail>
 register R1 : bits(32)
 register R2 : bits(32)
 
-function check_sat('sz: range(0, 32)) -> bool = {
+$property
+function prop('sz: range(0, 32)) -> bool = {
   let z: bits('sz) = sail_zeros(sz);
   let x: bits('sz + 32) = R1 @ z;
   let y: bits(32 + 'sz) = R2 @ z;
@@ -14,5 +15,5 @@ function check_sat('sz: range(0, 32)) -> bool = {
   // A and B must be equal
   let A = x @ y;
   let B = or_vec(sail_shiftleft(padding @ x, length(y)), padding @ y);
-  not_bool(A == B)
+  A == B
 }
diff --git a/test/smt/concat_prop128.unsat.sail b/test/smt/concat_prop128.unsat.sail
index 3d8ea45f..4205db10 100644
--- a/test/smt/concat_prop128.unsat.sail
+++ b/test/smt/concat_prop128.unsat.sail
@@ -5,7 +5,8 @@ $include <prelude.sail>
 register R1 : bits(64)
 register R2 : bits(64)
 
-function check_sat('sz: range(0, 64)) -> bool = {
+$property
+function prop('sz: range(0, 64)) -> bool = {
   let z: bits('sz) = sail_zeros(sz);
   let x: bits('sz + 64) = R1 @ z;
   let y: bits(64 + 'sz) = R2 @ z;
@@ -14,5 +15,5 @@ function check_sat('sz: range(0, 64)) -> bool = {
   // A and B must be equal
   let A = x @ y;
   let B = or_vec(sail_shiftleft(padding @ x, length(y)), padding @ y);
-  not_bool(A == B)
+  A == B
 }
diff --git a/test/smt/exception.unsat.sail b/test/smt/exception.unsat.sail
index e2455425..cd9f64d8 100644
--- a/test/smt/exception.unsat.sail
+++ b/test/smt/exception.unsat.sail
@@ -7,11 +7,12 @@ union exception = {
   E_unit : unit
 }
 
-function check_sat((): unit) -> bool = {
+$property
+function prop((): unit) -> bool = {
   try {
-    throw(E_bool(false))
+    throw(E_bool(true))
   } catch {
     E_bool(b) => b,
-    E_unit() => true
+    E_unit() => false
   }
 }
diff --git a/test/smt/exception_2.unsat.sail b/test/smt/exception_2.unsat.sail
index 0a540341..795aa867 100644
--- a/test/smt/exception_2.unsat.sail
+++ b/test/smt/exception_2.unsat.sail
@@ -9,15 +9,16 @@ union exception = {
 
 register R : bool
 
-function check_sat((): unit) -> bool = {
+$property
+function prop((): unit) -> bool = {
   try {
     if R then {
-       throw(E_bool(false))
+       throw(E_bool(true))
     } else {
-       false
+       true
     }
   } catch {
     E_bool(b) => b,
-    E_unit() => true
+    E_unit() => false
   }
 }
diff --git a/test/smt/exception_3.unsat.sail b/test/smt/exception_3.unsat.sail
index f0f71945..b0dd37db 100644
--- a/test/smt/exception_3.unsat.sail
+++ b/test/smt/exception_3.unsat.sail
@@ -9,16 +9,17 @@ union exception = {
 
 register R : bool
 
-function check_sat((): unit) -> bool = {
+$property
+function prop((): unit) -> bool = {
   try {
     if R then {
-       throw(E_bool(false))
+       throw(E_bool(true))
     } else {
-       return(false);
-       true
+       return(true);
+       false
     }
   } catch {
     E_bool(b) => b,
-    E_unit() => true
+    E_unit() => false
   }
 }
diff --git a/test/smt/lt_int_irrefl.unsat.sail b/test/smt/lt_int_irrefl.unsat.sail
index 984793be..371208b4 100644
--- a/test/smt/lt_int_irrefl.unsat.sail
+++ b/test/smt/lt_int_irrefl.unsat.sail
@@ -2,6 +2,7 @@ default Order dec
 
 $include <prelude.sail>
 
-function check_sat(x: int) -> bool = {
-  x < x
+$property
+function prop(x: int) -> bool = {
+  not_bool(x < x)
 }
\ No newline at end of file
diff --git a/test/smt/lt_int_trans.unsat.sail b/test/smt/lt_int_trans.unsat.sail
index efd930b3..289839a7 100644
--- a/test/smt/lt_int_trans.unsat.sail
+++ b/test/smt/lt_int_trans.unsat.sail
@@ -2,6 +2,7 @@ default Order dec
 
 $include <prelude.sail>
 
-function check_sat(x: int, y: int, z: int) -> bool = {
-  if (x < y & y < z) then not_bool(x < z) else false
+$property
+function prop(x: int, y: int, z: int) -> bool = {
+  if (x < y & y < z) then x < z else true
 }
\ No newline at end of file
diff --git a/test/smt/lteq_int_antisym.unsat.sail b/test/smt/lteq_int_antisym.unsat.sail
index 1730f417..3c6dc028 100644
--- a/test/smt/lteq_int_antisym.unsat.sail
+++ b/test/smt/lteq_int_antisym.unsat.sail
@@ -2,6 +2,7 @@ default Order dec
 
 $include <prelude.sail>
 
-function check_sat(x: int, y: int) -> bool = {
-  if x <= y & y <= x then not_bool(x == y) else false
+$property
+function prop(x: int, y: int) -> bool = {
+  if x <= y & y <= x then x == y else true
 }
\ No newline at end of file
diff --git a/test/smt/lteq_int_def.unsat.sail b/test/smt/lteq_int_def.unsat.sail
index db3bf1f0..11859019 100644
--- a/test/smt/lteq_int_def.unsat.sail
+++ b/test/smt/lteq_int_def.unsat.sail
@@ -2,6 +2,7 @@ default Order dec
 
 $include <prelude.sail>
 
-function check_sat(x: int, y: int) -> bool = {
-  if x <= y then not_bool(x < y | x == y) else not_bool(y < x)
+$property
+function prop(x: int, y: int) -> bool = {
+  if x <= y then x < y | x == y else y < x
 }
\ No newline at end of file
diff --git a/test/smt/lteq_int_refl.unsat.sail b/test/smt/lteq_int_refl.unsat.sail
index eeb7e0d9..0417ae6e 100644
--- a/test/smt/lteq_int_refl.unsat.sail
+++ b/test/smt/lteq_int_refl.unsat.sail
@@ -2,6 +2,7 @@ default Order dec
 
 $include <prelude.sail>
 
-function check_sat(x: int) -> bool = {
-  not_bool(x <= x)
+$property
+function prop(x: int) -> bool = {
+  x <= x
 }
\ No newline at end of file
diff --git a/test/smt/lteq_int_trans.unsat.sail b/test/smt/lteq_int_trans.unsat.sail
index e7a8a3d7..d95ccb8e 100644
--- a/test/smt/lteq_int_trans.unsat.sail
+++ b/test/smt/lteq_int_trans.unsat.sail
@@ -2,6 +2,7 @@ default Order dec
 
 $include <prelude.sail>
 
-function check_sat(x: int, y: int, z: int) -> bool = {
-  if (x <= y & y <= z) then not_bool(x <= z) else false
+$property
+function prop(x: int, y: int, z: int) -> bool = {
+  if (x <= y & y <= z) then x <= z else true
 }
\ No newline at end of file
diff --git a/test/smt/order.unsat.sail b/test/smt/order.unsat.sail
index c25762c9..0d96967f 100644
--- a/test/smt/order.unsat.sail
+++ b/test/smt/order.unsat.sail
@@ -4,7 +4,8 @@ $include <prelude.sail>
 
 overload ~ = {not_bool}
 
-function check_sat(x: int, y: int, z: int) -> bool = {
+$property
+function prop(x: int, y: int, z: int) -> bool = {
   let lteq_refl    = x <= x;
   let lteq_trans   = (if x <= y & y <= z then x <= z else true);
   let lteq_antisym = (if x <= y & y <= x then x == y else true);
@@ -26,7 +27,7 @@ function check_sat(x: int, y: int, z: int) -> bool = {
   let lt_negate = (if x > 0 then negate(x) < x else true);
   let gt_negate = (if x < 0 then negate(x) > x else true);
 
-  ~(lteq_refl & lteq_trans & lteq_antisym & lt_irrefl & lt_trans & lt_implies_lteq
+  lteq_refl & lteq_trans & lteq_antisym & lt_irrefl & lt_trans & lt_implies_lteq
   & gteq_refl & gteq_trans & gteq_antisym & gt_irrefl & gt_trans & gt_implies_gteq
-  & lt_negate & gt_negate)
+  & lt_negate & gt_negate
 }
diff --git a/test/smt/run_tests.py b/test/smt/run_tests.py
index 097c0672..fb5a0ebd 100755
--- a/test/smt/run_tests.py
+++ b/test/smt/run_tests.py
@@ -19,10 +19,11 @@ def test_smt(name, solver, sail_opts):
         tests = {}
         for filename in filenames:
             basename = os.path.splitext(os.path.basename(filename))[0]
+            basename = basename.replace('.', '_')
             tests[filename] = os.fork()
             if tests[filename] == 0:
                 step('sail {} -smt {} -o {}'.format(sail_opts, filename, basename))
-                step('{} {}.smt2 1> {}.out'.format(solver, basename, basename))
+                step('{} {}_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.sat.sail b/test/smt/rv_add_0.sat.sail
index f1c86c4d..d0e8a5f5 100644
--- a/test/smt/rv_add_0.sat.sail
+++ b/test/smt/rv_add_0.sat.sail
@@ -143,13 +143,14 @@ function clause execute (ITYPE (imm, rs1, rd, RISCV_ADDI)) =
 
 function clause decode _ = None()
 
-function check_sat(imm:  bits(12), rs1: regbits, rd: regbits, v: xlenbits) -> bool = {
+$property
+function prop(imm:  bits(12), rs1: regbits, rd: regbits, v: xlenbits) -> bool = {
   X(rs1) = v;
   match decode(imm @ rs1 @ 0b000 @ rd @ 0b0010011) {
     Some(instr) => {
       execute(instr);
-      not_bool(X(rd) == v + sail_sign_extend(imm, sizeof(xlen)) | rd == 0)
+      X(rd) == v + sail_sign_extend(imm, sizeof(xlen)) | rd == 0
     },
-    _ => true
+    _ => false
   }
 }
diff --git a/test/smt/rv_add_0.unsat.sail b/test/smt/rv_add_0.unsat.sail
index daa2996d..cddc5c7a 100644
--- a/test/smt/rv_add_0.unsat.sail
+++ b/test/smt/rv_add_0.unsat.sail
@@ -143,13 +143,14 @@ function clause execute (ITYPE (imm, rs1, rd, RISCV_ADDI)) =
 
 function clause decode _ = None()
 
-function check_sat(imm:  bits(12), rs1: regbits, rd: regbits, v: xlenbits) -> bool = {
+$property
+function prop(imm:  bits(12), rs1: regbits, rd: regbits, v: xlenbits) -> bool = {
   X(rs1) = v;
   match decode(imm @ rs1 @ 0b000 @ rd @ 0b0010011) {
     Some(instr) => {
       execute(instr);
-      not_bool(X(rd) == v + sail_sign_extend(imm, sizeof(xlen)) | rd == 0 | rs1 == 0)
+      X(rd) == v + sail_sign_extend(imm, sizeof(xlen)) | rd == 0 | rs1 == 0
     },
-    _ => true
+    _ => false
   }
 }
diff --git a/test/smt/rv_add_1.sat.sail b/test/smt/rv_add_1.sat.sail
index b2a562c4..d9c1c127 100644
--- a/test/smt/rv_add_1.sat.sail
+++ b/test/smt/rv_add_1.sat.sail
@@ -143,13 +143,14 @@ function clause execute (ITYPE (imm, rs1, rd, RISCV_ADDI)) =
 
 function clause decode _ = None()
 
-function check_sat(imm:  bits(12), rs1: regbits, rd: regbits) -> bool = {
+$property
+function prop(imm:  bits(12), rs1: regbits, rd: regbits) -> bool = {
   let v = X(rs1);
   match decode(imm @ rs1 @ 0b000 @ rd @ 0b0010011) {
     Some(instr) => {
       execute(instr);
-      not_bool(X(rd) == v + sail_sign_extend(imm, sizeof(xlen)))
+      X(rd) == v + sail_sign_extend(imm, sizeof(xlen))
     },
-    _ => true
+    _ => false
   }
 }
diff --git a/test/smt/rv_add_1.unsat.sail b/test/smt/rv_add_1.unsat.sail
index d3b784e8..9621240d 100644
--- a/test/smt/rv_add_1.unsat.sail
+++ b/test/smt/rv_add_1.unsat.sail
@@ -143,13 +143,14 @@ function clause execute (ITYPE (imm, rs1, rd, RISCV_ADDI)) =
 
 function clause decode _ = None()
 
-function check_sat(imm:  bits(12), rs1: regbits, rd: regbits) -> bool = {
+$property
+function prop(imm:  bits(12), rs1: regbits, rd: regbits) -> bool = {
   let v = X(rs1);
   match decode(imm @ rs1 @ 0b000 @ rd @ 0b0010011) {
     Some(instr) => {
       execute(instr);
-      not_bool(X(rd) == v + sail_sign_extend(imm, sizeof(xlen)) | rd == 0)
+      X(rd) == v + sail_sign_extend(imm, sizeof(xlen)) | rd == 0
     },
-    _ => true
+    _ => false
   }
 }
diff --git a/test/smt/rv_add_decode.unsat.sail b/test/smt/rv_add_decode.unsat.sail
index d5952e09..01653c6f 100644
--- a/test/smt/rv_add_decode.unsat.sail
+++ b/test/smt/rv_add_decode.unsat.sail
@@ -17,9 +17,10 @@ function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0
 
 function clause decode _ = None()
 
-function check_sat(imm:  bits(12), rs1: regbits, rd: regbits) -> bool = {
+$property
+function prop(imm:  bits(12), rs1: regbits, rd: regbits) -> bool = {
   match decode(imm @ rs1 @ 0b000 @ rd @ 0b0010011) {
-    Some(ITYPE(_)) => false,
-    _ => true
+    Some(ITYPE(_)) => true,
+    _ => false
   }
 }
\ No newline at end of file
diff --git a/test/smt/rv_reg_rw.unsat.sail b/test/smt/rv_reg_rw.unsat.sail
index 5bf419a9..485f45c7 100644
--- a/test/smt/rv_reg_rw.unsat.sail
+++ b/test/smt/rv_reg_rw.unsat.sail
@@ -128,7 +128,8 @@ scattered union ast
 
 union clause ast = ITYPE : (bits(12), regbits, regbits, iop)
 
-function check_sat(r: regbits, v: xlenbits) -> bool = {
+$property
+function prop(r: regbits, v: xlenbits) -> bool = {
   X(r) = v;
-  not_bool(X(r) == v | r == 0)
+  X(r) == v | r == 0
 }
diff --git a/test/smt/shift_or_concat.unsat.sail b/test/smt/shift_or_concat.unsat.sail
index 4e562889..1cb8f11a 100644
--- a/test/smt/shift_or_concat.unsat.sail
+++ b/test/smt/shift_or_concat.unsat.sail
@@ -5,10 +5,11 @@ $include <prelude.sail>
 register R1 : bits(32)
 register R2 : bits(32)
 
-function check_sat((): unit) -> bool = {
+$property
+function prop((): unit) -> bool = {
   let x = sail_zero_extend(R1, 64);
   let x = sail_shiftleft(x, 32);
   let y = or_vec(x, sail_zero_extend(R2, 64));
   let z = R1 @ R2;
-  not_bool(y == z)
+  y == z
 }
\ No newline at end of file
diff --git a/test/smt/shift_or_concat128.unsat.sail b/test/smt/shift_or_concat128.unsat.sail
index 9cb0a0b8..36eab646 100644
--- a/test/smt/shift_or_concat128.unsat.sail
+++ b/test/smt/shift_or_concat128.unsat.sail
@@ -5,10 +5,11 @@ $include <prelude.sail>
 register R1 : bits(128)
 register R2 : bits(128)
 
-function check_sat((): unit) -> bool = {
+$property
+function prop((): unit) -> bool = {
   let x = sail_zero_extend(R1, 256);
   let x = sail_shiftleft(x, 128);
   let y = or_vec(x, sail_zero_extend(R2, 256));
   let z = R1 @ R2;
-  not_bool(y == z)
+  y == z
 }
\ No newline at end of file
diff --git a/test/smt/shift_or_concat4.unsat.sail b/test/smt/shift_or_concat4.unsat.sail
index b8510151..7bc983f5 100644
--- a/test/smt/shift_or_concat4.unsat.sail
+++ b/test/smt/shift_or_concat4.unsat.sail
@@ -5,10 +5,11 @@ $include <prelude.sail>
 register R1 : bits(4)
 register R2 : bits(4)
 
-function check_sat((): unit) -> bool = {
+$property
+function prop((): unit) -> bool = {
   let x = sail_zero_extend(R1, 8);
   let x = sail_shiftleft(x, 4);
   let y = or_vec(x, sail_zero_extend(R2, 8));
   let z = R1 @ R2;
-  not_bool(y == z)
+  y == z
 }
\ No newline at end of file
diff --git a/test/smt/shift_or_concat4_2.unsat.sail b/test/smt/shift_or_concat4_2.unsat.sail
index 2c730cbd..43a1b198 100644
--- a/test/smt/shift_or_concat4_2.unsat.sail
+++ b/test/smt/shift_or_concat4_2.unsat.sail
@@ -5,11 +5,12 @@ $include <prelude.sail>
 register R1 : bits(4)
 register R2 : bits(4)
 
-function check_sat((): unit) -> bool = {
+$property
+function prop((): unit) -> bool = {
   let w = 4;
   let x = sail_zero_extend(R1, 8);
   let x = sail_shiftleft(x, w);
   let y = or_vec(x, sail_zero_extend(R2, 8));
   let z = R1 @ R2;
-  not_bool(y == z)
+  y == z
 }
\ No newline at end of file
diff --git a/test/smt/shift_or_concat_1.sat.sail b/test/smt/shift_or_concat_1.sat.sail
index 88107c50..505753b2 100644
--- a/test/smt/shift_or_concat_1.sat.sail
+++ b/test/smt/shift_or_concat_1.sat.sail
@@ -5,10 +5,11 @@ $include <prelude.sail>
 register R1 : bits(32)
 register R2 : bits(32)
 
-function check_sat((): unit) -> bool = {
+$property
+function prop((): unit) -> bool = {
   let x = sail_zero_extend(R1, 64);
   let x = sail_shiftleft(x, 31);
   let y = or_vec(x, sail_zero_extend(R2, 64));
   let z = R1 @ R2;
-  not_bool(y == z)
+  y == z
 }
\ No newline at end of file
diff --git a/test/smt/shift_or_concat_2.sat.sail b/test/smt/shift_or_concat_2.sat.sail
index f7fd1f4c..8929834b 100644
--- a/test/smt/shift_or_concat_2.sat.sail
+++ b/test/smt/shift_or_concat_2.sat.sail
@@ -5,10 +5,11 @@ $include <prelude.sail>
 register R1 : bits(32)
 register R2 : bits(32)
 
-function check_sat((): unit) -> bool = {
+$property
+function prop((): unit) -> bool = {
   let x = sail_zero_extend(R1, 64);
   let x = sail_shiftleft(x, 33);
   let y = or_vec(x, sail_zero_extend(R2, 64));
   let z = R1 @ R2;
-  not_bool(y == z)
+  y == z
 }
\ No newline at end of file
diff --git a/test/smt/shiftr_zero_1.sat.sail b/test/smt/shiftr_zero_1.sat.sail
index 9eb75c69..04dd74c4 100644
--- a/test/smt/shiftr_zero_1.sat.sail
+++ b/test/smt/shiftr_zero_1.sat.sail
@@ -4,7 +4,8 @@ $include <prelude.sail>
 
 register R : bits(64)
 
-function check_sat((): unit) -> bool = {
+$property
+function prop((): unit) -> bool = {
   let x = sail_shiftright(R, 63);
-  not_bool(x == 0x0000_0000_0000_0000)
+  x == 0x0000_0000_0000_0000
 }
\ No newline at end of file
diff --git a/test/smt/shiftr_zero_1.unsat.sail b/test/smt/shiftr_zero_1.unsat.sail
index bcf60bb8..e43787d9 100644
--- a/test/smt/shiftr_zero_1.unsat.sail
+++ b/test/smt/shiftr_zero_1.unsat.sail
@@ -4,7 +4,8 @@ $include <prelude.sail>
 
 register R : bits(64)
 
-function check_sat((): unit) -> bool = {
+$property
+function prop((): unit) -> bool = {
   let x = sail_shiftright(R, 64);
-  not_bool(x == 0x0000_0000_0000_0000)
+  x == 0x0000_0000_0000_0000
 }
\ No newline at end of file
diff --git a/test/smt/sign_extend.unsat.sail b/test/smt/sign_extend.unsat.sail
index 835c2ce9..91f9d192 100644
--- a/test/smt/sign_extend.unsat.sail
+++ b/test/smt/sign_extend.unsat.sail
@@ -2,12 +2,13 @@ default Order dec
 
 $include <prelude.sail>
 
-function check_sat(xs: bits(16)) -> bool = {
+$property
+function prop(xs: bits(16)) -> bool = {
   var p: bool = false;
   if xs[15] == bitzero then {
     p = 0x0000 @ xs == sail_sign_extend(xs, 32);
   } else {
     p = 0xFFFF @ xs == sail_sign_extend(xs, 32);
   };
-  not_bool(p)
+  p
 }
\ No newline at end of file
diff --git a/test/smt/sign_extend_2.unsat.sail b/test/smt/sign_extend_2.unsat.sail
index 9c5b4437..75ec3836 100644
--- a/test/smt/sign_extend_2.unsat.sail
+++ b/test/smt/sign_extend_2.unsat.sail
@@ -2,12 +2,13 @@ default Order dec
 
 $include <prelude.sail>
 
-function check_sat(xs: bits(16)) -> bool = {
+$property
+function prop(xs: bits(16)) -> bool = {
   var p: bool = true;
   if xs[15] == bitzero then {
     p = 0x0000 @ xs == sail_sign_extend(xs, 32);
   } else {
     p = 0xFFFF @ xs == sail_sign_extend(xs, 32);
   };
-  not_bool(p)
+  p
 }
\ No newline at end of file
diff --git a/test/smt/trivial.sat.sail b/test/smt/trivial.sat.sail
index 8b8d67ce..0f802d54 100644
--- a/test/smt/trivial.sat.sail
+++ b/test/smt/trivial.sat.sail
@@ -2,6 +2,7 @@ default Order dec
 
 $include <flow.sail>
 
-function check_sat((): unit) -> bool = {
-  true
+$property
+function prop((): unit) -> bool = {
+  false
 }
\ No newline at end of file
diff --git a/test/smt/trivial.unsat.sail b/test/smt/trivial.unsat.sail
index 2237a21f..a6c32ed1 100644
--- a/test/smt/trivial.unsat.sail
+++ b/test/smt/trivial.unsat.sail
@@ -2,6 +2,7 @@ default Order dec
 
 $include <flow.sail>
 
-function check_sat((): unit) -> bool = {
-  false
+$property
+function prop((): unit) -> bool = {
+  true
 }
\ No newline at end of file
diff --git a/test/smt/trivial_funcall.sat.sail b/test/smt/trivial_funcall.sat.sail
index 48166c12..09fa5381 100644
--- a/test/smt/trivial_funcall.sat.sail
+++ b/test/smt/trivial_funcall.sat.sail
@@ -2,8 +2,9 @@ default Order dec
 
 $include <flow.sail>
 
-function f((): unit) -> bool = true
+function f((): unit) -> bool = false
 
-function check_sat((): unit) -> bool = {
+$property
+function prop((): unit) -> bool = {
   f()
 }
\ No newline at end of file
diff --git a/test/smt/trivial_return.sat.sail b/test/smt/trivial_return.sat.sail
index 4cfd709a..180606cd 100644
--- a/test/smt/trivial_return.sat.sail
+++ b/test/smt/trivial_return.sat.sail
@@ -2,7 +2,8 @@ default Order dec
 
 $include <flow.sail>
 
-function check_sat((): unit) -> bool = {
-  return true;
-  false
+$property
+function prop((): unit) -> bool = {
+  return false;
+  true
 }
\ No newline at end of file
diff --git a/test/smt/trivial_return.unsat.sail b/test/smt/trivial_return.unsat.sail
index 261955a4..507e3116 100644
--- a/test/smt/trivial_return.unsat.sail
+++ b/test/smt/trivial_return.unsat.sail
@@ -2,7 +2,8 @@ default Order dec
 
 $include <flow.sail>
 
-function check_sat((): unit) -> bool = {
-  return false;
-  return true
+$property
+function prop((): unit) -> bool = {
+  return true;
+  return false
 }
\ No newline at end of file
diff --git a/test/smt/update_access.unsat.sail b/test/smt/update_access.unsat.sail
index 26411ff0..38a25d99 100644
--- a/test/smt/update_access.unsat.sail
+++ b/test/smt/update_access.unsat.sail
@@ -2,11 +2,12 @@ default Order dec
 
 $include <vector_dec.sail>
 
-function check_sat(xs: bits(65), x: bit) -> bool = {
+$property
+function prop(xs: bits(65), x: bit) -> bool = {
   ys = xs;
   ys[63] = x;
   ys[64] = x;
   ys[42] = x;
   ys[0] = x;
-  not_bool(ys[64] == x & ys[63] == x & ys[42] == x & ys[0] == x)
+  ys[64] == x & ys[63] == x & ys[42] == x & ys[0] == x
 }
\ No newline at end of file
diff --git a/test/smt/zeros_1.sat.sail b/test/smt/zeros_1.sat.sail
index 4a813dcc..476b5ba4 100644
--- a/test/smt/zeros_1.sat.sail
+++ b/test/smt/zeros_1.sat.sail
@@ -2,6 +2,7 @@ default Order dec
 
 $include <vector_dec.sail>
 
-function check_sat((): unit) -> bool = {
-  0x00 == sail_zeros(8)
+$property
+function prop((): unit) -> bool = {
+  0x00 != sail_zeros(8)
 }
\ No newline at end of file
diff --git a/test/smt/zeros_1.unsat.sail b/test/smt/zeros_1.unsat.sail
index ade7cd23..02499efe 100644
--- a/test/smt/zeros_1.unsat.sail
+++ b/test/smt/zeros_1.unsat.sail
@@ -2,6 +2,7 @@ default Order dec
 
 $include <vector_dec.sail>
 
-function check_sat((): unit) -> bool = {
-  0x1 == sail_zeros(4)
-}
\ No newline at end of file
+$property
+function prop((): unit) -> bool = {
+  0x1 != sail_zeros(4)
+}
diff --git a/test/smt/zeros_2.sat.sail b/test/smt/zeros_2.sat.sail
index 5cea2e99..1d61c9a2 100644
--- a/test/smt/zeros_2.sat.sail
+++ b/test/smt/zeros_2.sat.sail
@@ -2,6 +2,7 @@ default Order dec
 
 $include <vector_dec.sail>
 
-function check_sat((): unit) -> bool = {
-  0x0000_0000_0000_0000 == sail_zeros(64)
+$property
+function prop((): unit) -> bool = {
+  0x0000_0000_0000_0000 != sail_zeros(64)
 }
\ No newline at end of file
diff --git a/test/smt/zeros_2.unsat.sail b/test/smt/zeros_2.unsat.sail
index 855c46b4..0d5aad20 100644
--- a/test/smt/zeros_2.unsat.sail
+++ b/test/smt/zeros_2.unsat.sail
@@ -2,6 +2,7 @@ default Order dec
 
 $include <vector_dec.sail>
 
-function check_sat((): unit) -> bool = {
-  0b1 == sail_zeros(1)
+$property
+function prop((): unit) -> bool = {
+  0b1 != sail_zeros(1)
 }
\ No newline at end of file
diff --git a/test/smt/zeros_3.sat.sail b/test/smt/zeros_3.sat.sail
index 3da36e1f..243ceac2 100644
--- a/test/smt/zeros_3.sat.sail
+++ b/test/smt/zeros_3.sat.sail
@@ -2,6 +2,7 @@ default Order dec
 
 $include <vector_dec.sail>
 
-function check_sat((): unit) -> bool = {
-  0x0000_0000_0000_0000_0 == sail_zeros(68)
+$property
+function prop((): unit) -> bool = {
+  not_bool(0x0000_0000_0000_0000_0 == sail_zeros(68))
 }
\ No newline at end of file
diff --git a/test/smt/zeros_3.unsat.sail b/test/smt/zeros_3.unsat.sail
index 145ab386..0c271660 100644
--- a/test/smt/zeros_3.unsat.sail
+++ b/test/smt/zeros_3.unsat.sail
@@ -2,6 +2,7 @@ default Order dec
 
 $include <vector_dec.sail>
 
-function check_sat((): unit) -> bool = {
-  0x0000_0000_0000_0000_1 == sail_zeros(68)
+$property
+function prop((): unit) -> bool = {
+  0x0000_0000_0000_0000_1 != sail_zeros(68)
 }
\ No newline at end of file
diff --git a/test/smt/zeros_4.unsat.sail b/test/smt/zeros_4.unsat.sail
index 416430fc..c02e034d 100644
--- a/test/smt/zeros_4.unsat.sail
+++ b/test/smt/zeros_4.unsat.sail
@@ -2,6 +2,7 @@ default Order dec
 
 $include <vector_dec.sail>
 
-function check_sat((): unit) -> bool = {
-  0x1000_0000_0000_0000_0 == sail_zeros(68)
+$property
+function prop((): unit) -> bool = {
+  0x1000_0000_0000_0000_0 != sail_zeros(68)
 }
\ No newline at end of file