2 files changed, 36 insertions, 1 deletions
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index c03b8934..086d4d11 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -178,7 +178,9 @@ let rec smt_ctyp ctx = function
      | Some regs -> Bitvec (required_width (Big_int.of_int (List.length regs)))
      | _ -> failwith ("No registers with ctyp: " ^ string_of_ctyp ctyp)
      end
-  | ctyp -> failwith ("Unhandled ctyp: " ^ string_of_ctyp ctyp)
+  | CT_list _ -> raise (Reporting.err_todo ctx.pragma_l "Lists not yet supported in SMT generation")
+  | CT_poly ->
+     Reporting.unreachable ctx.pragma_l __POS__ "Found polymorphic type in SMT property"
 
 (* We often need to create a SMT bitvector of a length sz with integer
    value x. [bvpint sz x] does this for positive integers, and [bvint sz x]
diff --git a/test/smt/real.unsat.sail b/test/smt/real.unsat.sail
new file mode 100644
index 00000000..035ee562
--- /dev/null
+++ b/test/smt/real.unsat.sail
@@ -0,0 +1,33 @@
+default Order dec
+
+$include <prelude.sail>
+$include <real.sail>
+
+$property
+val prop : (real, real, real) -> bool effect {escape}
+
+function prop(x, y, z) = {
+  assert(x * y == y * x);
+  assert(x * (y * z) == (x * y) * z);
+  assert(x - x == 0.0);
+  assert(x * 0.0 == 0.0);
+  assert(x * 1.0 == x);
+
+  if not_bool(x == 0.0) then {
+    assert(x * (y / x) == y)
+  };
+
+  // Comparisons
+  assert(x <= x);
+  assert(x >= x);
+  if x > y then {
+    assert(y < x)
+  };
+  if x < y & y < z then {
+    assert(x < z)
+  };
+  if x <= y & y <= x then {
+    assert(x == y)
+  };
+  true
+}
+\ No newline at end of file